Comment: about Ramsey
The following definitions and lemmas are based on Coquand's article
"A direct proof of Ramsey's Theorem".
The original article may have used the list type for finite sequences,
but to make this theory more compatible with our formuation of
bar induction, we use ⌜n:ℕ × (ℕn ⟶ T)⌝ to represent finite sequences
of type T.⋅
Definition: predicate-shift
A_x == λn,s. (A (n + 1) seq-append(1;n;seq-single(x);s))
Lemma: predicate-shift_wf
∀[T:Type]. ∀[X:𝕌']. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ X]. ∀[x:T]. (A_x ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ X)
Lemma: second-countable-choice
∀[X:𝕌']. ∀[R:ℕ ⟶ (n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X) ⟶ ℙ'].
((∀n:ℕ. ∃A:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. R[n;A]) ⇒ (∃B:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. ∀n:ℕ. R[n;B_n]))
Definition: predicate-or-shift
A[x] == λn,s. ((A n s) ∨ (A_x n s))
Lemma: predicate-or-shift_wf
∀[T:Type]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[x:T]. (A[x] ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ)
Definition: nary-rel
n-aryRel(T) == (ℕn ⟶ T) ⟶ ℙ
Lemma: nary-rel_wf
∀[T:Type]. ∀[n:ℕ]. (n-aryRel(T) ∈ 𝕌')
Definition: nary-rel-predicate
[[R]] == λm,s. ((n ≤ m) ∧ (R s))
Lemma: nary-rel-predicate_wf
∀[T:Type]. ∀[n:ℕ]. ∀[R:n-aryRel(T)]. ([[R]] ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ)
Definition: tree-secures
tree-secures(T;A;p)==r let iszero,f = p in if iszero then ∀s:ℕ0 ⟶ T. (A 0 s) else ∀x:T. tree-secures(T;A[x];f x) fi
Lemma: tree-secures_wf
∀[T:Type]. ∀[p:wfd-tree(T)]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. (tree-secures(T;A;p) ∈ ℙ)
Lemma: tree-secures_functionality
∀T:Type. ∀p:wfd-tree(T).
∀[A,B:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].
((∀n:ℕ. ∀s:ℕn ⟶ T. ((A n s) ⇒ (B n s))) ⇒ tree-secures(T;A;p) ⇒ tree-secures(T;B;p))
Lemma: trivial-tree-secures
∀T:Type. ∀p:wfd-tree(T). ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ((A 0 (λx.⊥)) ⇒ tree-secures(T;A;p))
Definition: tree-tensor
tree-tensor(n;p;q) ==
fix((λtree-tensor,n,p,q. let pzero,f = p
in if (n =z 0) then if pzero then q else Wsup(ff;λx.(tree-tensor 0 (f x) q)) fi
if pzero then p
else let qzero,g = q
in if qzero
then q
else Wsup(ff;λx.(tree-tensor (n - 1) (tree-tensor n (f x) q)
(tree-tensor n p (g x))))
fi
fi ))
n
p
q
Lemma: tree-tensor_wf
∀[T:Type]. ∀[n:ℕ]. ∀[p,q:wfd-tree(T)]. (tree-tensor(n;p;q) ∈ wfd-tree(T))
Definition: almost-full
almost-full(T;n;R) == ∃p:wfd-tree(T). tree-secures(T;[[R]];p)
Lemma: almost-full_wf
∀[T:Type]. ∀[n:ℕ]. ∀[R:n-aryRel(T)]. (almost-full(T;n;R) ∈ ℙ)
Definition: almost_full
almost_full(T;n;R) == ∀f:ℕ ⟶ T. ∃s:ℕn ⟶ ℕ. (strictly-increasing-seq(n;s) ∧ (R (f o s)))
Lemma: almost_full_wf
∀[T:Type]. ∀[n:ℕ]. ∀[R:n-aryRel(T)]. (almost_full(T;n;R) ∈ ℙ)
Lemma: almost_full0
∀[T:Type]. ∀[R:0-aryRel(T)]. ((R (λi.⊥)) ⇒ almost_full(T;0;R))
Lemma: Veldman-Coquand
∀X:Type. ∀n:ℕ. ∀p,q:wfd-tree(X).
∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
(tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;p;q)))
Lemma: Veldman-Ramsey
Ramsey's theorem -
infinite version has a constructive version here⋅
∀T:Type. ∀n:ℕ. ∀[R,S:n-aryRel(T)]. (almost-full(T;n;R) ⇒ almost-full(T;n;S) ⇒ almost-full(T;n;R ∧ S))
Comment: alternate fan and bar doc
This directory has Joan Moscovakis's proof that FAN implies WKL! .
We use "alternate" definitions of everything where finite sequences
are given by an ⌜n ∈ ℕ⌝ and a ⌜s ∈ ℕn ⟶ T⌝.
(This turns out to be nicer than using ⌜T List⌝.)
The key lemmas are fan-bar-sep where she proves a separation principle,
and alt-bar-sep-wkl! where this separation pinciple is used to prove
WLK! .⋅
Definition: altbar
bar(X) == ∀f:ℕ ⟶ T. ∃n:ℕ. (↑(X n f))
Lemma: altbar_wf
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (bar(X) ∈ ℙ)
Definition: altubar
uniformBar(X) == ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (↑(X n f))
Lemma: altubar_wf
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (uniformBar(X) ∈ ℙ)
Definition: altfan
This is an alternate statement of the fan theorem for "detachable" bars
where we use the type n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹 for the "set" of nodes.
Since we are using 𝔹 (boolean) instead of ⌜ℙ⌝, the decidablity is built in.
Also, the use of ⌜n ∈ ℕ⌝ and ⌜ℕn ⟶ T⌝ to represent finite sequences
turns out to be nicer than using ⌜T List⌝.⋅
Fan(T) == ∀X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. (bar(X) ⇒ uniformBar(X))
Lemma: altfan_wf
∀[T:Type]. (Fan(T) ∈ ℙ')
Definition: altunbounded
Unbounded(A) == ∀n:ℕ. ∃s:ℕn ⟶ T. (↑(A n s))
Lemma: altunbounded_wf
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (Unbounded(X) ∈ ℙ)
Definition: alttree
Tree(A) == ∀n:ℕ. ∀s:ℕn ⟶ T. ((↑(A n s)) ⇒ (∀i:ℕn. (↑(A i s))))
Lemma: alttree_wf
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (Tree(X) ∈ ℙ)
Definition: altjbar
jbar(X;Y) == ∀f:ℕ ⟶ T. ∀g:ℕ ⟶ S. ((∃n:ℕ. (↑(X n f))) ∨ (∃n:ℕ. (↑(Y n g))))
Lemma: altjbar_wf
∀[T,S:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. ∀[Y:n:ℕ ⟶ (ℕn ⟶ S) ⟶ 𝔹]. (jbar(X;Y) ∈ ℙ)
Definition: altbarsep
BarSep(T;S) == ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. ∀B:n:ℕ ⟶ (ℕn ⟶ S) ⟶ 𝔹. (jbar(A;B) ⇒ (bar(A) ∨ bar(B)))
Lemma: altbarsep_wf
∀[T,S:Type]. (BarSep(T;S) ∈ ℙ)
Definition: altneg
¬(A) == λn,s. (¬b(A n s))
Lemma: altneg_wf
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (¬(X) ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
Lemma: altneg-altneg
∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (¬(¬(X)) = X ∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹))
Definition: altpath
IsPath(A;f) == ∀n:ℕ. (↑(A n f))
Lemma: altpath_wf
∀[T:Type]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. ∀[f:ℕ ⟶ T]. (IsPath(A;f) ∈ ℙ)
Definition: alt-one-path
AtMostOnePath(A) == ∀g,h:ℕ ⟶ T. ∀n:ℕ. ((¬((g n) = (h n) ∈ T)) ⇒ (∃m:ℕ. (¬((↑(A m g)) ∧ (↑(A m h))))))
Lemma: alt-one-path_wf
∀[T:Type]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹]. (AtMostOnePath(A) ∈ ℙ)
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 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)]))
Lemma: alt-wkl!_wf
∀[T:Type]. (WKL!(T) ∈ ℙ)
Lemma: fan-bar-sep
∀[T:Type]. (Fan(T) ⇒ (∃size:ℕ. T ~ ℕsize) ⇒ BarSep(T;T))
Lemma: fan-bar-not-unbounded
∀[T:Type]. ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. (bar(A) ⇒ (¬(Tree(¬(A)) ∧ Unbounded(¬(A))))) supposing ¬¬Fan(T)
Lemma: complement-unbounded-tree
∀[T:Type]. ∀A:{A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} . (¬bar(¬(A))) supposing ¬¬Fan(T)
Definition: seq+
s.t == λi.if i <z n then s i else t fi
Lemma: seq+_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[t:T]. (s.t ∈ ℕn + 1 ⟶ T)
Definition: seq-append
seq-append(n;s;s') == λi.if i <z n then s i else s' (i - n) fi
Lemma: seq-append_wf
∀[T:Type]. ∀[n,k:ℕ]. ∀[s:ℕn ⟶ T]. ∀[s':ℕk ⟶ T]. (seq-append(n;s;s') ∈ ℕn + k ⟶ T)
Lemma: alt-bar-sep-wkl!
∀[T:Type]
((∃size:ℕ. T ~ ℕsize)
⇒ BarSep(T;T)
⇒ (∀A:{A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} . (¬bar(¬(A))))
⇒ WKL!(T))
Lemma: fan-wkl!
∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan(T) ⇒ WKL!(T))
Definition: dec-predicate
Decidable(X) == ∀t:T. Dec(X t)
Lemma: dec-predicate_wf
∀[T:Type]. ∀[X:T ⟶ ℙ]. (Decidable(X) ∈ ℙ)
Definition: R-closed
R-closed(T;x.X[x];a,b.R[a; b]) == ∀a,b:T. (R[a; b] ⇒ X[a] ⇒ X[b])
Lemma: R-closed_wf
∀[T:Type]. ∀[X:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. (R-closed(T;x.X[x];a,b.R[a;b]) ∈ ℙ)
Definition: predicate-not
¬(A) == λx.(¬(A x))
Lemma: predicate-not_wf
∀[T:Type]. ∀[A:T ⟶ Type]. (¬(A) ∈ T ⟶ ℙ)
Lemma: decidable-predicate-not
∀[T:Type]. ∀[A:T ⟶ ℙ].
((Decidable(A) ⇒ Decidable(¬(A))) ∧ ((Decidable(¬(A)) ∧ (∀t:T. ((¬¬(A t)) ⇒ (A t)))) ⇒ Decidable(A)))
Definition: predicate-and
predicate-and(A;B) == λp.let x,y = p in (A x) ∧ (B y)
Lemma: predicate-and_wf
∀[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ]. (predicate-and(A;B) ∈ (T × S) ⟶ ℙ)
Lemma: decidable-predicate-and
∀[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ].
((∃t:T. (A t)) ⇒ (∃s:S. (B s)) ⇒ (∀p:T × S. Dec(predicate-and(A;B) p) ⇐⇒ (∀x:T. Dec(A x)) ∧ (∀y:S. Dec(B y))))
Definition: predicate-or
predicate-or(A;B) == λp.let x,y = p in (A x) ∨ (B y)
Lemma: predicate-or_wf
∀[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ]. (predicate-or(A;B) ∈ (T × S) ⟶ ℙ)
Lemma: decidable-predicate-or
∀[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ].
((∃t:T. (¬(A t))) ⇒ (∃s:S. (¬(B s))) ⇒ (∀p:T × S. Dec(predicate-or(A;B) p) ⇐⇒ (∀x:T. Dec(A x)) ∧ (∀y:S. Dec(B y))))
Definition: tbar
tbar(T;X) == ∀f:ℕ ⟶ T. ∃n:ℕ. (X map(f;upto(n)))
Lemma: tbar_wf
∀[T:Type]. ∀[X:(T List) ⟶ ℙ]. (tbar(T;X) ∈ ℙ)
Definition: jbar
jbar(T;S;X;Y) == ∀f:ℕ ⟶ T. ∀g:ℕ ⟶ S. ((∃n:ℕ. (X map(f;upto(n)))) ∨ (∃n:ℕ. (Y map(g;upto(n)))))
Lemma: jbar_wf
∀[T,S:Type]. ∀[X:(T List) ⟶ ℙ]. ∀[Y:(S List) ⟶ ℙ]. (jbar(T;S;X;Y) ∈ ℙ)
Definition: ubar
ubar(T;X) == ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (X map(f;upto(n)))
Lemma: ubar_wf
∀[T:Type]. ∀[X:(T List) ⟶ ℙ]. (ubar(T;X) ∈ ℙ)
Definition: dbar
dbar(T;X) == Decidable(X) ∧ tbar(T;X)
Lemma: dbar_wf
∀[T:Type]. ∀[X:(T List) ⟶ ℙ]. (dbar(T;X) ∈ ℙ)
Definition: dfan
Fan_d(T) == ∀X:(T List) ⟶ ℙ. (dbar(T;X) ⇒ ubar(T;X))
Lemma: dfan_wf
∀[T:Type]. (Fan_d(T) ∈ ℙ')
Definition: bar-separation
BarSep(T;S) ==
∀A:(T List) ⟶ ℙ. ∀B:(S List) ⟶ ℙ. (Decidable(A) ⇒ Decidable(B) ⇒ jbar(T;S;A;B) ⇒ (tbar(T;A) ∨ tbar(S;B)))
Lemma: bar-separation_wf
∀[T,S:Type]. (BarSep(T;S) ∈ ℙ')
Lemma: fan-implies-bar-sep
∀[T:Type]. (Fan_d(T) ⇒ (∃size:ℕ. T ~ ℕsize) ⇒ BarSep(T;T))
Definition: is-path
is-path(A;f) == ∀n:ℕ. (A map(f;upto(n)))
Lemma: is-path_wf
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. ∀[f:ℕ ⟶ T]. (is-path(A;f) ∈ ℙ)
Definition: eff-unique-path
eff-unique-path(T;A) ==
∀g,h:ℕ ⟶ T. ∀n:ℕ. ((¬((g n) = (h n) ∈ T)) ⇒ (∃m:ℕ. (¬((A map(g;upto(m))) ∧ (A map(h;upto(m)))))))
Lemma: eff-unique-path_wf
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. (eff-unique-path(T;A) ∈ ℙ)
Definition: down-closed
down-closed(T;X) == R-closed(T List;s.X s;bs,as.as ≤ bs)
Lemma: down-closed_wf
∀[T:Type]. ∀[X:(T List) ⟶ ℙ]. (down-closed(T;X) ∈ ℙ)
Definition: upwd-closure
upwd-closure(T;A) == λas.∃bs:T List. (bs ≤ as ∧ (A bs))
Lemma: upwd-closure_wf
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. (upwd-closure(T;A) ∈ (T List) ⟶ ℙ)
Lemma: decidable__upwd-closure
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. (Decidable(A) ⇒ (∀as:T List. Dec(upwd-closure(T;A) as)))
Definition: tree-big
tree-big(T;A;n) == ∀as:T List. ((||as|| = n ∈ ℤ) ⇒ (A as))
Lemma: tree-big_wf
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. ∀[n:ℕ]. (tree-big(T;A;n) ∈ ℙ)
Lemma: decidable__tree-big
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. ((∃k:ℕ. T ~ ℕk) ⇒ Decidable(A) ⇒ (∀n:ℕ. Dec(tree-big(T;A;n))))
Lemma: tree-big-monotone
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;A);a) ⇒ tree-big(T;upwd-closure(T;A);b))
Lemma: tree-big-least
∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
((∃k:ℕ. T ~ ℕk)
⇒ Decidable(A)
⇒ (¬(A []))
⇒ (∀n:ℕ
(tree-big(T;upwd-closure(T;A);n)
⇒ (∃k:ℕn. ((¬tree-big(T;upwd-closure(T;A);k)) ∧ tree-big(T;upwd-closure(T;A);k + 1))))))
Lemma: not-tree-big
∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
((∃k:ℕ. T ~ ℕk)
⇒ Decidable(A)
⇒ (∀n:ℕ. ((¬tree-big(T;upwd-closure(T;A);n)) ⇒ (∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;A) as)))))))
Definition: unbounded-list-predicate
Unbounded(A) == ∀n:ℕ. ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (A as))
Lemma: unbounded-list-predicate_wf
∀[T:Type]. ∀[A:(T List) ⟶ ℙ]. (Unbounded(A) ∈ ℙ)
Lemma: fan-implies-barred-not-unbounded
∀[T:Type]. (Fan_d(T) ⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))))
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)]))
Lemma: twkl!_wf
∀[T:Type]. (WKL!(T) ∈ ℙ')
Lemma: bar-separation-implies-twkl!
∀[T:Type]
((∃size:ℕ. T ~ ℕsize)
⇒ BarSep(T;T)
⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A))))))
⇒ WKL!(T))
Lemma: dfan-implies-twkl!
∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan_d(T) ⇒ WKL!(T))
Lemma: twkl!-implies-dfan
∀T:Type. ((∃k:ℕ. T ~ ℕk) ⇒ WKL!(T) ⇒ Fan_d(T))
Lemma: dfan-iff-twkl!
∀T:Type. ((∃k:ℕ. T ~ ℕk) ⇒ (Fan_d(T) ⇐⇒ WKL!(T)))
Definition: tree-bars
(p|A) == fix((λtree-bars,A,p. let iszero,f = p in if iszero then A 0 (λx.x) else ∀x:T. (tree-bars A_x (f x)) fi )) A p
Lemma: tree-bars_wf
∀[T:Type]. ∀[p:wfd-tree(T)]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ((p|A) ∈ ℙ)
Lemma: Coquand-fan-theorem
∀[T:Type]
(finite-type(T)
⇒ (∀p:wfd-tree(T). ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ T. ((A n s) ⇒ (∀m:{n...}. ∀t:ℕm ⟶ T. ((t = s ∈ (ℕn ⟶ T)) ⇒ (A m t)))))
⇒ (p|A)
⇒ (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T. (A m as)))))
Definition: fan
Fan ==
∀A:(𝔹 List) ⟶ ℙ
((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
Lemma: fan_wf
Fan ∈ ℙ'
Definition: has-no-path
has-no-path(A) == ∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (¬(A map(f;upto(n))))
Lemma: has-no-path_wf
∀[A:(𝔹 List) ⟶ ℙ]. (has-no-path(A) ∈ ℙ)
Definition: eff-unique
eff-unique(A) == ∀g,h:ℕ ⟶ 𝔹. ∀n:ℕ. ((¬g n = h n) ⇒ (∃m:ℕ. (¬((A map(g;upto(m))) ∧ (A map(h;upto(m)))))))
Lemma: eff-unique_wf
∀A:(𝔹 List) ⟶ ℙ. (eff-unique(A) ∈ ℙ)
Definition: infinite-tree
infinite-tree(A) == (∀as,bs:𝔹 List. (as ≤ bs ⇒ (A bs) ⇒ (A as))) ∧ (∀n:ℕ. ∃as:𝔹 List. ((||as|| = n ∈ ℤ) ∧ (A as)))
Lemma: infinite-tree_wf
∀A:(𝔹 List) ⟶ ℙ. (infinite-tree(A) ∈ ℙ)
Definition: wkl!
WKL! ==
∀A:{A:(𝔹 List) ⟶ ℙ| infinite-tree(A)} . ((∀as:𝔹 List. Dec(A as)) ⇒ eff-unique(A) ⇒ (∃f:ℕ ⟶ 𝔹 [is-path(A;f)]))
Lemma: wkl!_wf
WKL! ∈ ℙ'
Lemma: fan-iff-dfan-bool
Fan ⇐⇒ Fan
Lemma: wkl!-iff-twkl!-bool
WKL! ⇐⇒ WKL!(𝔹)
Lemma: fan-iff-wkl!
Fan ⇐⇒ WKL!
Definition: nwkl!
nWKL! == ∀A:(𝔹 List) ⟶ ℙ. ((∀as:𝔹 List. Dec(A as)) ⇒ infinite-tree(A) ⇒ eff-unique(A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
Lemma: nwkl!_wf
nWKL! ∈ ℙ'
Lemma: nwkl!-iff-twkl!-bool
nWKL! ⇐⇒ WKL!(𝔹)
Lemma: nwkl!-implies-fan
nWKL! ⇒ Fan
Definition: PFan
PFan{i:l}() ==
∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
⇒ (∀bc,bc':(𝔹 × 𝔹) List. (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
⇒ (∃k:ℕ
∀gh:ℕ ⟶ (𝔹 × 𝔹)
((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
Lemma: PFan_wf
PFan{i:l}() ∈ ℙ'
Lemma: fan-implies-PFan
Fan ⇒ PFan{i:l}()
Lemma: fan-implies-nwkl!-using-PFan
Fan ⇒ nWKL!
Lemma: fan-iff-nwkl!
Fan ⇐⇒ nWKL!
Lemma: wkl!-iff-nwkl!
WKL! ⇐⇒ nWKL!
Definition: unsquashed-WCP
unsquashed-WCP ==
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a,b:ℕ ⟶ ℕ. ((∀i:ℕM a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
Lemma: unsquashed-WCP_wf
unsquashed-WCP ∈ ℙ
Definition: base-CP
base-CP() ==
∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base
∃M:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ. ∀a,b:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕM a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
Lemma: base-CP_wf
base-CP() ∈ ℙ
Lemma: Escardo-Xu
¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ)))
Lemma: unsquashed-weak-continuity-false
¬unsquashed-WCP
Lemma: unsquashed-weak-continuity-false2
¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ)))
Lemma: unsquashed-weak-continuity-base-false
¬base-CP()
Lemma: Troelstra-lemma
¬(∀g:ℕ ⟶ ℕ. ∃n:ℕ. ∀f:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ (∀x:ℕ. ((g x) = 0 ∈ ℕ)) ⇒ (∀x:ℕ. ((f x) = 0 ∈ ℕ))))
Definition: AC_1_0
AC_1_0{i:l}() == ∀R:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ. ((∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. (R f n))) ⇒ (↓∃F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. (R f (F f))))
Lemma: AC_1_0_wf
AC_1_0{i:l}() ∈ ℙ'
Home
Index