Nuprl Definition : twkl!
WKL!(T) ==
∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
(Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
Definitions occuring in Statement :
unbounded-list-predicate: Unbounded(A),
down-closed: down-closed(T;X),
eff-unique-path: eff-unique-path(T;A),
is-path: is-path(A;f),
dec-predicate: Decidable(X),
list: T List,
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
prop: ℙ,
and: P ∧ Q,
down-closed: down-closed(T;X),
unbounded-list-predicate: Unbounded(A),
dec-predicate: Decidable(X),
list: T List,
implies: P ⇒ Q,
eff-unique-path: eff-unique-path(T;A),
sq_exists: ∃x:{A| B[x]},
function: x:A ⟶ B[x],
nat: ℕ,
is-path: is-path(A;f)
FDL editor aliases :
twkl!
Latex:
WKL!(T) ==
\mforall{}A:\{A:(T List) {}\mrightarrow{} \mBbbP{}| down-closed(T;A) \mwedge{} Unbounded(A)\}
(Decidable(A) {}\mRightarrow{} eff-unique-path(T;A) {}\mRightarrow{} (\mexists{}f:\{\mBbbN{} {}\mrightarrow{} T| is-path(A;f)\}))
Date html generated:
2016_05_14-PM-04_10_28
Last ObjectModification:
2015_09_22-PM-06_02_20
Theory : fan-theorem
Home
Index