Nuprl Definition : wkl!
WKL! ==
∀A:{A:(𝔹 List) ⟶ ℙ| infinite-tree(A)} . ((∀as:𝔹 List. Dec(A as)) ⇒ eff-unique(A) ⇒ (∃f:{ℕ ⟶ 𝔹| is-path(A;f)}))
Definitions occuring in Statement :
infinite-tree: infinite-tree(A),
eff-unique: eff-unique(A),
is-path: is-path(A;f),
list: T List,
nat: ℕ,
bool: 𝔹,
decidable: Dec(P),
prop: ℙ,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
set: {x:A| B[x]} ,
prop: ℙ,
infinite-tree: infinite-tree(A),
all: ∀x:A. B[x],
list: T List,
decidable: Dec(P),
apply: f a,
implies: P ⇒ Q,
eff-unique: eff-unique(A),
sq_exists: ∃x:{A| B[x]},
function: x:A ⟶ B[x],
nat: ℕ,
bool: 𝔹,
is-path: is-path(A;f)
FDL editor aliases :
wkl!
Latex:
WKL! ==
\mforall{}A:\{A:(\mBbbB{} List) {}\mrightarrow{} \mBbbP{}| infinite-tree(A)\}
((\mforall{}as:\mBbbB{} List. Dec(A as)) {}\mRightarrow{} eff-unique(A) {}\mRightarrow{} (\mexists{}f:\{\mBbbN{} {}\mrightarrow{} \mBbbB{}| is-path(A;f)\}))
Date html generated:
2016_05_14-PM-04_12_41
Last ObjectModification:
2015_09_22-PM-06_02_24
Theory : fan-theorem
Home
Index