Nuprl Definition : alt-wkl!
WKL! is the weak Konig lemma with uniqueness.
"weak" because is about decidable (aka "detachable") trees.
We use A of type ⌜n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹⌝ to represent the "set" of nodes.
Tree(A) says that A is "downward closed".
Unbounded(A) says that A has nodes of every height
(but we don't need the constructive witness for this, so the
assumptions ⌜Tree(A) ∧ Unbounded(A)⌝ can be put into a set-type).
The "uniquness" assumption is AtMostOnePath(A), and the conclusion
is that there is a path.
The theorem Error :fan-wkl! says that for a finite type T, Fan(T) ⇒ WKL!(T).
Since we can prove Fan(T), that means that WKL!(T) is true for finite types T.
⋅
WKL!(T) == ∀A:{A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} . (AtMostOnePath(A) ⇒ (∃f:ℕ ⟶ T [IsPath(A;f)]))
Definitions occuring in Statement :
alt-one-path: AtMostOnePath(A),
altpath: IsPath(A;f),
alttree: Tree(A),
altunbounded: Unbounded(A),
int_seg: {i..j-},
nat: ℕ,
bool: 𝔹,
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],
natural_number: $n
Definitions occuring in definition :
altpath: IsPath(A;f),
nat: ℕ,
function: x:A ⟶ B[x],
sq_exists: ∃x:A [B[x]],
alt-one-path: AtMostOnePath(A),
implies: P ⇒ Q,
altunbounded: Unbounded(A),
alttree: Tree(A),
and: P ∧ Q,
bool: 𝔹,
natural_number: $n,
int_seg: {i..j-},
set: {x:A| B[x]} ,
all: ∀x:A. B[x]
FDL editor aliases :
alt-wkl!
Latex:
WKL!(T) ==
\mforall{}A:\{A:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbB{}| Tree(A) \mwedge{} Unbounded(A)\}
(AtMostOnePath(A) {}\mRightarrow{} (\mexists{}f:\mBbbN{} {}\mrightarrow{} T [IsPath(A;f)]))
Date html generated:
2019_06_20-PM-02_46_29
Last ObjectModification:
2019_06_06-PM-10_09_17
Theory : fan-theorem
Home
Index