Nuprl Definition : limited-omniscience
The limited principle of omniscience (LPO) is a simple, classically true,
proposition that is not true in intuitionistic mathematics.
It contradicts even a 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
no-limited-omniscience.⋅
LPO == ∀f:ℕ ⟶ 𝔹. ((∀n:ℕ. f n = ff) ∨ (∃n:ℕ. f 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: f a,
function: x:A ⟶ B[x],
equal: s = 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: s = t ∈ T,
bool: 𝔹,
apply: f a,
btrue: tt
FDL editor aliases :
limited-omniscience
Latex:
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