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