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 s) ∨ (A_x 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 in if iszero then ∀s:ℕ0 ⟶ T. (A 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 s)  (B 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 x.⊥))  tree-secures(T;A;p))

Definition: tree-tensor
tree-tensor(n;p;q) ==
  fix((λtree-tensor,n,p,q. let pzero,f 
                           in if (n =z 0) then if pzero then else Wsup(ff;λx.(tree-tensor (f x) q)) fi 
                              if pzero then p
                              else let qzero,g 
                                   in if qzero
                                      then q
                                      else Wsup(ff;λx.(tree-tensor (n 1) (tree-tensor (f x) q) 
                                                       (tree-tensor (g x))))
                              fi )) 

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 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 s) ∨ ([[R]] s));p)
     tree-secures(X;λm,s. ((B s) ∨ ([[S]] s));q)
     tree-secures(X;λm,s. (((A s) ∨ (B s)) ∨ (([[R]] s) ∧ ([[S]] s)));tree-tensor(n;p;q)))

Lemma: Veldman-Ramsey
Ramsey's theorem 
     infinite version has 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 ⌜List⌝.)

The key lemmas are fan-bar-sep where she proves separation principle,
and alt-bar-sep-wkl! where this separation pinciple is used to prove
WLK! .⋅

Definition: altbar
bar(X) ==  ∀f:ℕ ⟶ T. ∃n:ℕ(↑(X f))

Lemma: altbar_wf
[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹].  (bar(X) ∈ ℙ)

Definition: altubar
uniformBar(X) ==  ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (↑(X 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 ⌜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 s))

Lemma: altunbounded_wf
[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹].  (Unbounded(X) ∈ ℙ)

Definition: alttree
Tree(A) ==  ∀n:ℕ. ∀s:ℕn ⟶ T.  ((↑(A s))  (∀i:ℕn. (↑(A s))))

Lemma: alttree_wf
[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹].  (Tree(X) ∈ ℙ)

Definition: altjbar
jbar(X;Y) ==  ∀f:ℕ ⟶ T. ∀g:ℕ ⟶ S.  ((∃n:ℕ(↑(X f))) ∨ (∃n:ℕ(↑(Y 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 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 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 g)) ∧ (↑(A 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 of type ⌜n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹⌝ to represent the "set" of nodes.
Tree(A) says that is "downward closed".
Unbounded(A) says that 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 set-type).

The "uniquness" assumption is AtMostOnePath(A), and the conclusion
is that there is path.

The theorem fan-wkl! says that for 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:ℕ ⟶ [IsPath(A;f)]))

Lemma: alt-wkl!_wf
[T:Type]. (WKL!(T) ∈ ℙ)

Lemma: fan-bar-sep
[T:Type]. (Fan(T)  (∃size:ℕ~ ℕ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 <then else fi 

Lemma: seq+_wf
[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[t:T].  (s.t ∈ ℕ1 ⟶ T)

Definition: seq-append
seq-append(n;s;s') ==  λi.if i <then else s' (i n) fi 

Lemma: seq-append_wf
[T:Type]. ∀[n,k:ℕ]. ∀[s:ℕn ⟶ T]. ∀[s':ℕk ⟶ T].  (seq-append(n;s;s') ∈ ℕk ⟶ T)

Lemma: alt-bar-sep-wkl!
  ((∃size:ℕ~ ℕsize)
   (∀A:{A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹Tree(A) ∧ Unbounded(A)} bar(¬(A))))

Lemma: fan-wkl!
[T:Type]. ((∃size:ℕ~ ℕ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 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 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:ℕ~ ℕ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, ≤ 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:ℕ~ ℕ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:ℕ~ ℕk)
   (A []))
         (∃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:ℕ~ ℕk)
   (∀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:ℕ ⟶ [is-path(A;f)]))

Lemma: twkl!_wf
[T:Type]. (WKL!(T) ∈ ℙ')

Lemma: bar-separation-implies-twkl!
  ((∃size:ℕ~ ℕsize)
   (∀A:(T List) ⟶ ℙ(dbar(T;A)  (down-closed(T;¬(A)) ∧ Unbounded(¬(A))))))

Lemma: dfan-implies-twkl!
[T:Type]. ((∃size:ℕ~ ℕsize)  Fan_d(T)  WKL!(T))

Lemma: twkl!-implies-dfan
T:Type. ((∃k:ℕ~ ℕk)  WKL!(T)  Fan_d(T))

Lemma: dfan-iff-twkl!
T:Type. ((∃k:ℕ~ ℕk)  (Fan_d(T) ⇐⇒ WKL!(T)))

Definition: tree-bars
(p|A) ==  fix((λtree-bars,A,p. let iszero,f in if iszero then x.x) else ∀x:T. (tree-bars A_x (f x)) fi )) p

Lemma: tree-bars_wf
[T:Type]. ∀[p:wfd-tree(T)]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ].  ((p|A) ∈ ℙ)

Lemma: Coquand-fan-theorem
   (∀p:wfd-tree(T). ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ.
        ((∀n:ℕ. ∀s:ℕn ⟶ T.  ((A s)  (∀m:{n...}. ∀t:ℕm ⟶ T.  ((t s ∈ (ℕn ⟶ T))  (A t)))))
         (∃N:ℕ. ∀m:{N...}. ∀as:ℕm ⟶ T.  (A 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:ℕ.  ((¬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))))))
         ∀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:ℕ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:ℕ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

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

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 n)))  (↓∃F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ(R (F f))))

Lemma: AC_1_0_wf
AC_1_0{i:l}() ∈ ℙ'

Home Index