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