Existence of a certain non-constant function implies the limited principle of omnisience

[jkingdon]

Existence of a certain non-constant function implies the limited principle of omnisience

[jkingdon]

Perhaps relatedly, does A. x e. RR A. y e. RR DECID x =//= y imply _om e. Omni ?

I just now noticed this is already proven - https://us.metamath.org/ileuni/triap.html plus https://us.metamath.org/ileuni/trilpo.html

[benjub]

If A. x e. RR DECID x =//= 0, then you can construct a function as in the hypothesis of ncflop: take it to be 1 if x is apart from zero.

[benjub]

I think I got it: Let $P \colon \omega \to 2$ be a property. Define the number $x := \sum_n P_n 2^{-n}$. You can decide whether the integer $f(x)$ is zero or not. But this amounts to P being everywhere zero or not.

[digama0]

Does A. x e. RR A. y e. RR DECID x =/= y ?

This one also follows similar to @benjub 's first answer: take f(x) to be 1 if x != 0. Then f(0) = 0 (because -. ( 0 =/= 0 )) and f(x) =/= 0 if x > 0 because this implies x != 0.