Nuprl Definition : limited-omniscience

The limited principle of omniscience (LPO) is simple, classically true, 
proposition that is not true in intuitionistic mathematics.
It contradicts even weak form of Brouwer's continutity principle.
Nuprl satisfies strong versions of continuity 
(see rules--proved true in the Nuprl-in-Coq model--
StrongContinuity2 and weak continuity rule Continuity).
Therfore we can prove the negation of LPO:
Error :no-weak-limited-omniscience  

LPO ==  ∀f:ℕ ⟶ 𝔹((∀n:ℕff) ∨ (∃n:ℕtt))

Definitions occuring in Statement :  nat: bfalse: ff btrue: tt bool: 𝔹 all: x:A. B[x] exists: x:A. B[x] or: P ∨ Q apply: a function: x:A ⟶ B[x] equal: t ∈ T
Definitions occuring in definition :  function: x:A ⟶ B[x] or: P ∨ Q all: x:A. B[x] bfalse: ff exists: x:A. B[x] nat: equal: t ∈ T bool: 𝔹 apply: a btrue: tt
FDL editor aliases :  limited-omniscience

LPO  ==    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}n:\mBbbN{}.  f  n  =  ff)  \mvee{}  (\mexists{}n:\mBbbN{}.  f  n  =  tt))

Date html generated: 2018_07_29-AM-09_29_07
Last ObjectModification: 2015_09_23-AM-07_36_58

Theory : basic

Home Index