Open jkingdon opened 4 weeks ago
This is one of the usual constructive principles between nothing and excluded middle (excluded middle is known as the principle of omniscience because of https://us.metamath.org/ileuni/exmidomni.html ).
We can define/prove:
A e. LOmni <-> ∀𝑓 ∈ (2o ↑𝑚 𝐴) ∀g ∈ (2o ↑𝑚 𝐴) ( -. 1o e. ( ran f i^i ran g ) -> ( -. 1o e. ran f \/ -. 1o e. ran g ) )
LOmni
NN e. LOmni <-> A. f e. ( { 0 , 1 } ^m NN ) ( E* n e. NN ( f ` n ) = 1 -> A. n e. NN ( f ` ( 2 x. n ) ) = 0 \/ A. n e. NN ( f ` ( ( 2 x. n ) + 1 ) ) = 0 )
A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) -> _om e. LOmni
A e. Omni -> A e. LOmni
This is one of the usual constructive principles between nothing and excluded middle (excluded middle is known as the principle of omniscience because of https://us.metamath.org/ileuni/exmidomni.html ).
We can define/prove:
A e. LOmni <-> ∀𝑓 ∈ (2o ↑𝑚 𝐴) ∀g ∈ (2o ↑𝑚 𝐴) ( -. 1o e. ( ran f i^i ran g ) -> ( -. 1o e. ran f \/ -. 1o e. ran g ) )(see "Stated set-theoretically, the lesser limited principle of omniscience for A" at https://ncatlab.org/nlab/show/principle+of+omniscience#the_lesser_limited_principle_of_omniscience ).LOmniNN e. LOmni <-> A. f e. ( { 0 , 1 } ^m NN ) ( E* n e. NN ( f ` n ) = 1 -> A. n e. NN ( f ` ( 2 x. n ) ) = 0 \/ A. n e. NN ( f ` ( ( 2 x. n ) + 1 ) ) = 0 ). This is from https://awswan.github.io/teaching/intuitionisticlogic/lecturenotes/section3.pdf or https://plato.stanford.edu/entries/mathematics-constructive/ (search for "LLPO")A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) -> _om e. LOmnias described at https://ncatlab.org/nlab/show/principle+of+omniscience#analyticA e. Omni -> A e. LOmni(mentioned at https://ncatlab.org/nlab/show/principle+of+omniscience#analytic at least for A = ω but I suppose maybe true for any A)