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

[jkingdon]

This is a bit counterintuitive to me, but certain kinds of functions cannot even be shown to exist in iset.mm. Exercise 11.6(ii) of [HoTT] can be translated into our notation as:

ncflpo.f $e |- ( ph -> F : RR --> NN ) $.
ncflpo.0 $e |- ( ph -> ( F ` 0 ) = 0 ) $.
ncflpo.rp $e |- ( ( ph /\ x e. RR+ ) -> ( F ` x ) =/= 0 ) $.
ncflpo $p |- ( ph -> _om e. Omni ) $.

Proving this would be a nice companion to https://us.metamath.org/ileuni/trilpo.html .

Perhaps relatedly, does A. x e. RR A. y e. RR DECID x =//= y imply _om e. Omni ? Answer: yes, see https://us.metamath.org/ileuni/trilpo.html and https://us.metamath.org/ileuni/triap.html Does A. x e. RR A. y e. RR DECID x =/= y ? _Answer: no, it implies _om e. WOmni as described in https://github.com/metamath/set.mm/issues/4041_

[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.

[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

[jkingdon]

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.

I have formalized this part at #4060 .

[jkingdon]

I think I got it: Let P:ω→2 be a property. Define the number x:=∑nPn2−n. You can decide whether the integer f(x) is zero or not. But this amounts to P being everywhere zero or not.

I'm having trouble following this. The last sentence seems to be about WLPO rather than LPO (as in https://us.metamath.org/ileuni/redcwlpo.html ).

Perhaps relatedly, I also don't quite see the steps after "integer f(x) is zero or not". I see how those two cases get us -. 0 < x or -. x = 0. But I don't see the steps between there and either analytic LPO or regular LPO.

As a matter of how to set up the problem, we could either try to deal with _om e. Omni directly or it would also suffice if we could show the converse of #4060 :

( E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\
          A. x e. RR+ ( f ` x ) =/= 0 ) )
  -> A. x e. RR DECID x =//= 0 )

which would combine with https://us.metamath.org/ileuni/trilpo.html and triap for the result as originally stated.

[benjub]

@jkingdon : you're right: unless I was thinking of something else at the time, I am only proving WLPO. In more details:

Let $f \colon \mathbb{R} \to \mathbb{N}$ be such that $f(0)=0$ and $(x > 0 \to f(x) \neq 0)$. Let $P \colon \mathbb{N} \to 2$ be a property. Define the real number $x \coloneqq \sum_{n\geq 0} P_n 2^{-n}$. It is decidable whether the integer $f(x)$ is zero or not, that is, $f(x) \neq 0 \vee f(x) = 0$. By using the contrapositives of each of the two hypotheses on $f$ to each disjunct, we obtain $x \neq 0 \vee \neg x > 0$. If $x \neq 0$, then $\neg \forall n \in \mathbb{N} P_n = 0$. If $\neg x > 0$, then $\neg \exists n \in \mathbb{N} P_n = 1$, or equivalently $\forall n \in \mathbb{N} P_n = 0$. Therefore, we have proved $\text{DECID } \forall n \in \mathbb{N} P_n = 0$. Since $P$ was any property, we have proved that $\mathbb{N}$ is weakly omniscient.

[jkingdon]

unless I was thinking of something else at the time, I am only proving WLPO. In more details:

A formalization of this proof is at https://github.com/metamath/set.mm/pull/4100

[benjub]

@jkingdon : So, should the exercise from HOTT be corrected to conclude WLPO (what we proved) instead of LPO ? By the other results, if the exercise were correct in concluding LPO, then we would have that analytic WLPO implies LPO, which I haven't seen claimed anywhere (though I couldn't for now rule it out).

[jkingdon]

@jkingdon : So, should the exercise from HOTT be corrected to conclude WLPO (what we proved) instead of LPO ? By the other results, if the exercise were correct in concluding LPO, then we would have that analytic WLPO implies LPO, which I haven't seen claimed anywhere (though I couldn't for now rule it out).

Yeah, I've been meaning to make an issue on the HoTT Book site, so thanks for the nudge. Now up at https://github.com/HoTT/book/issues/1162 . As I note there, I'm not really sure exactly what the book should say but I think our results are (probably) good enough to show that it shouldn't say what it says now.