Lemma: decidable-finite-cantor
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ((∀x,y:T. Dec(R[x;y])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T. Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])))
Lemma: simple-decidable-finite-cantor
∀[T:Type]. ∀[R:T ⟶ ℙ]. ((∀x:T. Dec(R[x])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T. Dec(∃f:ℕn ⟶ 𝔹. R[F f])))
Definition: finite-cantor-decider
finite-cantor-decider(dcdr;n;F) ==
case primrec(n;λs,t. if dcdr (F (λi.s[i])) (F (λi.t[i])) then inl <λi.s[i], λi.t[i]> else inr (λ%8.Ax) fi ;
λi,x,s,t. case x (s @ [tt]) (t @ [ff])
of inl(fg) =>
inl fg
| inr(_) =>
case x (s @ [ff]) (t @ [tt])
of inl(fg) =>
inl fg
| inr(_) =>
case x (s @ [ff]) (t @ [ff])
of inl(fg) =>
inl fg
| inr(_) =>
case x (s @ [tt]) (t @ [tt]) of inl(fg) => inl fg | inr(_) => inr (λ_.Ax) )
[]
[]
of inl(fg) =>
inl let f,g = fg
in <f, g, case dcdr (F f) (F g) of inl(x) => x | inr(_) => Ax>
| inr(_) =>
inr (λ_.Ax)
Lemma: decidable-finite-cantor-ext
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ((∀x,y:T. Dec(R[x;y])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T. Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])))
Lemma: finite-cantor-decider_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀dcdr:∀x,y:T. Dec(R[x;y]). ∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.
(finite-cantor-decider(dcdr;n;F) ∈ Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g]))
Lemma: decidable-finite-cantor-to-int
∀[R:ℤ ⟶ ℤ ⟶ ℙ]. ((∀x,y:ℤ. Dec(R[x;y])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ ℤ. Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])))
Definition: simple-finite-cantor-decider
FiniteCantorDecide(dcdr;n;F) ==
case primrec(n;λs.if dcdr (F (λi.s[i])) then inl (λi.s[i]) else inr (λ%6.Ax) fi ;λi,x,s. case x (s @ [tt])
of inl(f) =>
inl f
| inr(_) =>
case x (s @ [ff])
of inl(f) =>
inl f
| inr(_) =>
inr (λ_.Ax) )
[]
of inl(f) =>
inl <f, case dcdr (F f) of inl(x) => x | inr(_) => Ax>
| inr(_) =>
inr (λ_.Ax)
Lemma: simple-decidable-finite-cantor-ext
∀[T:Type]. ∀[R:T ⟶ ℙ]. ((∀x:T. Dec(R[x])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T. Dec(∃f:ℕn ⟶ 𝔹. R[F f])))
Lemma: simple-finite-cantor-decider_wf
∀[T:Type]. ∀[R:T ⟶ ℙ]. ∀[dcdr:∀x:T. Dec(R[x])]. ∀[n:ℕ]. ∀[F:(ℕn ⟶ 𝔹) ⟶ T].
(FiniteCantorDecide(dcdr;n;F) ∈ Dec(∃f:ℕn ⟶ 𝔹. R[F f]))
Definition: strong-continuity-test
strong-continuity-test(M;n;f;b) == primrec(n;b;λi,r. if isl(M i f) then inr Ax else r fi )
Lemma: strong-continuity-test_wf
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕ?]. (strong-continuity-test(M;n;f;b) ∈ ℕ?)
Lemma: strong-continuity-test-unroll
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f,b:Top].
(strong-continuity-test(M;n;f;b) ~ if (n =z 0) then b
if isl(M (n - 1) f) then inr Ax
else strong-continuity-test(M;n - 1;f;b)
fi )
Lemma: strong-continuity-test-prop1
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕ?].
((↑isl(strong-continuity-test(M;n;f;b)))
⇒ ((↑isl(b)) ∧ (∀i:ℕ. (i < n ⇒ (↑isr(M i f)))) ∧ (strong-continuity-test(M;n;f;b) = b ∈ (ℕ?))))
Lemma: strong-continuity-test-prop2
∀[T:Type]
∀M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?). ∀n:ℕ. ∀f:ℕn ⟶ T. ∀b:ℕ?.
((↑isl(b))
⇒ (↑isr(strong-continuity-test(M;n;f;b)))
⇒ (∃m:ℕ. (m < n ∧ (↑isl(strong-continuity-test(M;m;f;M m f))))))
Lemma: strong-continuity-test-prop3
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n,m:ℕ]. ∀[f:ℕ ⟶ T].
((↑isl(strong-continuity-test(M;n;f;M n f))) ⇒ (↑isl(strong-continuity-test(M;m;f;M m f))) ⇒ (n = m ∈ ℤ))
Definition: bound-domain
bound-domain(f;n;e) == λx.if (x) < (0) then ⊥ else if (x) < (n) then f x else (exception(e; x))
Definition: bsc-body
bsc-body(F;M;f) ==
(∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer))
Lemma: bsc-body_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))]. ∀[f:ℕ ⟶ T]. (bsc-body(F;M;f) ∈ ℙ)
Definition: basic-strong-continuity
basic-strong-continuity(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ)) [(∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer))))]
Lemma: basic-strong-continuity_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (basic-strong-continuity(T;F) ∈ ℙ)
Definition: sq-basic-strong-continuity
sq-basic-strong-continuity(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ)) [(∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer))))]
Lemma: sq-basic-strong-continuity_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (sq-basic-strong-continuity(T;F) ∈ ℙ)
Definition: strong-continuity2
strong-continuity2(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
∀f:ℕ ⟶ T. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f)))
Lemma: strong-continuity2_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity2(T;F) ∈ ℙ)
Lemma: basic-implies-strong-continuity2
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (basic-strong-continuity(T;F) ⇒ strong-continuity2(T;F))
Lemma: basic-implies-strong-continuity2-ext
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (basic-strong-continuity(T;F) ⇒ strong-continuity2(T;F))
Definition: strong-continuity3
strong-continuity3(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
Lemma: strong-continuity3_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity3(T;F) ∈ ℙ)
Lemma: strong-continuity3_functionality_surject
∀[T,S:Type].
∀g:T ⟶ S. (Surj(T;S;g) ⇒ (∀F:(ℕ ⟶ S) ⟶ ℕ. (strong-continuity3(T;λf.(F (g o f))) ⇒ strong-continuity3(S;F))))
Lemma: strong-continuity3_functionality
∀[T,S:Type]. ∀e:T ~ S. ∀F:(ℕ ⟶ S) ⟶ ℕ. (strong-continuity3(T;λf.(F ((fst(e)) o f))) ⇒ strong-continuity3(S;F))
Lemma: strong-continuity2-implies-3
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity2(T;F) ⇒ strong-continuity3(T;F))
Lemma: strong-continuity2-iff-3
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity2(T;F) ⇐⇒ strong-continuity3(T;F))
Lemma: strong-continuity2_functionality_surject
∀[T,S:Type].
∀g:T ⟶ S. (Surj(T;S;g) ⇒ (∀F:(ℕ ⟶ S) ⟶ ℕ. (strong-continuity2(T;λf.(F (g o f))) ⇒ strong-continuity2(S;F))))
Lemma: strong-continuity2_biject_retract
∀[T,S,U:Type].
∀r:ℕ ⟶ U
((U ⊆r ℕ)
⇒ (∀x:U. ((r x) = x ∈ U))
⇒ (∀g:S ⟶ U
(Bij(S;U;g)
⇒ (∀F:(ℕ ⟶ T) ⟶ S
(strong-continuity2(T;g o F)
⇒ (∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))))))))
Lemma: strong-continuity2_biject_retract-ext
∀[T,S,U:Type].
∀r:ℕ ⟶ U
((U ⊆r ℕ)
⇒ (∀x:U. ((r x) = x ∈ U))
⇒ (∀g:S ⟶ U
(Bij(S;U;g)
⇒ (∀F:(ℕ ⟶ T) ⟶ S
(strong-continuity2(T;g o F)
⇒ (∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))))))))
Lemma: strong-continuity2_biject
∀[T,S:Type].
∀g:S ⟶ ℕ
(Bij(S;ℕ;g)
⇒ (∀F:(ℕ ⟶ T) ⟶ S
(strong-continuity2(T;g o F)
⇒ (∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))))))
Definition: strong-continuity4
strong-continuity4(T;F) ==
∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)
∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl (F f)) ∈ (ℕ?)))))
Lemma: strong-continuity4_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity4(T;F) ∈ ℙ)
Lemma: strong-continuity3-implies-4
∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. (strong-continuity3(T;F) ⇒ strong-continuity4(T;F))
Definition: weak-continuity-skolem
weak-continuity-skolem(T;F) == ∃M:(ℕ ⟶ T) ⟶ ℕ. ∀f,g:ℕ ⟶ T. ((f = g ∈ (ℕM f ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ))
Lemma: weak-continuity-skolem_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (weak-continuity-skolem(T;F) ∈ ℙ)
Lemma: weak-continuity-skolem_functionality
∀[T,S:Type].
∀e:T ~ S. ∀F:(ℕ ⟶ S) ⟶ ℕ. (weak-continuity-skolem(T;λf.(F ((fst(e)) o f))) ⇒ weak-continuity-skolem(S;F))
Lemma: strong-continuity2-weak-skolem
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (strong-continuity2(T;F) ⇒ weak-continuity-skolem(T;F))
Definition: Kleene-M
Kleene-M(F) == λn,f. ν(e.F bound-domain(f;n;e)?e:x.<x, x>)
Lemma: Kleene-M_wf
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (Kleene-M(F) ∈ ⇃(basic-strong-continuity(T;F)))
Definition: KleeneSearch
KleeneSearch(M;f;n) == eval x = M n f in if x is an integer then n else KleeneSearch(M;f;imax(fst(x);n + 1))
Lemma: KleeneSearch_wf
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[M:⇃(basic-strong-continuity(T;F))]. ∀[f:ℕ ⟶ T]. ∀[start:ℕ].
(KleeneSearch(M;f;start) ∈ ⇃({m:ℕ| (start ≤ m) ∧ (∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ)))} ))
Definition: KleeneM
KleeneM(F;f) == KleeneSearch(Kleene-M(F);f;1)
Lemma: KleeneM_wf
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[f:ℕ ⟶ T].
(KleeneM(F;f) ∈ ⇃({m:ℕ+| ∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ))} ))
Lemma: weak-continuity-skolem-truncated
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(weak-continuity-skolem(T;F))
Lemma: weak-continuity-truncated
∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]
∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(∀f:ℕ ⟶ T. ∃n:ℕ. ∀g:ℕ ⟶ T. ((f = g ∈ (ℕn ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: strong-continuity2-half-squash
∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
Lemma: strong-continuity2-half-squash-ext
∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
Lemma: strong-continuity3-half-squash
∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity3(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
Lemma: strong-continuity3-half-squash-surject
∀[B:Type]. ((∃g:ℕ ⟶ B. Surj(ℕ;B;g)) ⇒ (∀F:(ℕ ⟶ B) ⟶ ℕ. ⇃(strong-continuity3(B;F))))
Lemma: strong-continuity2-half-squash-surject-biject
∀[T,S,U:Type].
((U ⊆r ℕ)
⇒ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U))
⇒ (∃g:ℕ ⟶ T. Surj(ℕ;T;g))
⇒ (∃h:S ⟶ U. Bij(S;U;h))
⇒ (∀F:(ℕ ⟶ T) ⟶ S
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f))))))
Lemma: strong-continuity2-half-squash-surject-biject-ext
∀[T,S,U:Type].
((U ⊆r ℕ)
⇒ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U))
⇒ (∃g:ℕ ⟶ T. Surj(ℕ;T;g))
⇒ (∃h:S ⟶ U. Bij(S;U;h))
⇒ (∀F:(ℕ ⟶ T) ⟶ S
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f))))))
Lemma: strong-continuity3-half-squash-equipollent
∀[T:Type]. ∀[B:Type]. (T ~ B ⇒ (∀F:(ℕ ⟶ B) ⟶ ℕ. ⇃(strong-continuity3(B;F)))) supposing (T ⊆r ℕ) ∧ (↓T)
Lemma: strong-continuity2-no-inner-squash
∀F:(ℕ ⟶ ℕ) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f))))
Lemma: strong-continuity2-no-inner-squash-unique
∀F:(ℕ ⟶ ℕ) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ)))))
Lemma: strong-continuity2-no-inner-squash-unique-bool
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ)))))
Lemma: strong-continuity-implies1
∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]
(↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ. ((↓∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f))))
Lemma: strong-continuity-implies2
∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]
(↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))))
Lemma: strong-continuity-implies3
∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]
(↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl (F f)) ∈ (ℕ?)))))))
Lemma: strong-continuity-implies4
∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]
(↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl (F f)) ∈ (ℕ?))))))
Definition: seq-cont
seq-cont(T;F) ==
∀f:ℕ ⟶ T. ∀g:ℕ ⟶ ℕ ⟶ T.
((∀k:ℕ. ∃n:ℕ. ∀m:{n...}. ((g m) = f ∈ (ℕk ⟶ T))) ⇒ ⇃(∃n:ℕ. ∀m:{n...}. ((F (g m)) = (F f) ∈ ℕ)))
Lemma: seq-cont_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (seq-cont(T;F) ∈ ℙ)
Lemma: seq-cont-nat
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. seq-cont(ℕ;F)
Definition: unsquashed-seq-cont
unsquashed-seq-cont(T;F) ==
∀f:ℕ ⟶ T. ∀g:ℕ ⟶ ℕ ⟶ T.
((∀k:ℕ. ∃n:ℕ. ∀m:{n...}. ((g m) = f ∈ (ℕk ⟶ T))) ⇒ (∃n:ℕ. ∀m:{n...}. ((F (g m)) = (F f) ∈ ℕ)))
Lemma: unsquashed-seq-cont_wf
∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. (unsquashed-seq-cont(T;F) ∈ ℙ)
Lemma: strong-continuity2-implies-weak-skolem
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: strong-continuity2-implies-weak-skolem2
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕM f ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: strong-continuity2-implies-weak
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: weak-continuity-equipollent
∀T:Type. (T ~ ℕ ⇒ (∀F:(ℕ ⟶ T) ⟶ ℕ. ∀f:ℕ ⟶ T. ⇃(∃n:ℕ. ∀g:ℕ ⟶ T. ((f = g ∈ (ℕn ⟶ T)) ⇒ ((F f) = (F g) ∈ ℕ)))))
Lemma: weak-continuity-nat-int
∀F:(ℕ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ ⟶ ℤ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. ((f = g ∈ (ℕn ⟶ ℤ)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: weak-continuity-nat-nat
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: not-LPO
¬(∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ)))))
Lemma: weak-continuity-principle-nat-int
∀F:(ℕ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ ⟶ ℤ. ∀G:n:ℕ ⟶ {g:ℕ ⟶ ℤ| f = g ∈ (ℕn ⟶ ℤ)} . ∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)
Lemma: weak-continuity-principle-nat-nat
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. ∀G:n:ℕ ⟶ {g:ℕ ⟶ ℕ| f = g ∈ (ℕn ⟶ ℕ)} . ∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)
Lemma: weak-continuity-principle-nat+-int-bool
∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . ∃n:ℕ+. F f = F (G n)
Lemma: weak-continuity-principle-nat+-int-bool-ext
∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . ∃n:ℕ+. F f = F (G n)
Lemma: weak-continuity-principle-nat+-int-bool-double
∀F,H:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . ∃n:ℕ+. (F f = F (G n) ∧ H f = H (G n))
Lemma: weak-continuity-principle-nat+-int-bool-double-ext
∀F,H:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . ∃n:ℕ+. (F f = F (G n) ∧ H f = H (G n))
Lemma: weak-continuity-principle-nat+-int-nat
∀F:(ℕ+ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . ∃n:ℕ+. ((F f) = (F (G n)) ∈ ℕ)
Definition: WCP
WCP(F;f;G) == mu(λn.F f =b F (G (n + 1))) + 1
Lemma: WCP_wf
∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} . (WCP(F;f;G) ∈ {n:ℕ+| F f = F (G n)} )
Definition: WCPD
WCPD(F;H;f;G) == mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1
Lemma: WCPD_wf
∀F,H:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .
(WCPD(F;H;f;G) ∈ {n:ℕ+| F f = F (G n) ∧ H f = H (G n)} )
Lemma: weak-continuity-nat-int-bool
∀F:(ℕ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ ⟶ ℤ. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℤ. ((f = g ∈ (ℕn ⟶ ℤ)) ⇒ F f = F g))
Definition: pseudo-bounded
pseudo-bounded(S) == ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
Lemma: pseudo-bounded_wf
∀[S:Type]. pseudo-bounded(S) ∈ ℙ supposing S ⊆r ℕ
Lemma: pseudo-bounded-not-unbounded
∀[S:{S:Type| S ⊆r ℕ} ]. (pseudo-bounded(S) ⇒ (¬(∀B:ℕ. ∃n:{B...}. (n ∈ S))))
Lemma: pseudo-bounded-is-bounded
∀[S:{S:Type| S ⊆r ℕ} ]. ∀m:S. (pseudo-bounded(S) ⇒ ⇃(∃B:ℕ. ∀n:S. (n ≤ B)))
Lemma: weak-Markov-principle-alt
∀a,b:ℕ ⟶ ℕ. ((∀c:ℕ ⟶ ℕ. ((¬(a = c ∈ (ℕ ⟶ ℕ))) ∨ (¬(b = c ∈ (ℕ ⟶ ℕ))))) ⇒ (∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))))
Lemma: weak-Markov-principle
∀a,b:ℕ ⟶ ℕ.
((∀c:ℕ ⟶ ℕ. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬((b n) = (c n) ∈ ℤ))))))
⇒ (∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))))
Definition: nat-star
ℕ* == {s:ℕ ⟶ ℕ| ∀i,j:ℕ. (0 < s i ⇒ 0 < s j ⇒ (i = j ∈ ℤ))}
Lemma: nat-star_wf
ℕ* ∈ Type
Definition: nat-star-retract
nat-star-retract(s) == λn.if (∃i∈upto(n).0 <z s i)_b then 0 else s n fi
Lemma: nat-star-retract_wf
∀[s:ℕ ⟶ ℕ]. (nat-star-retract(s) ∈ ℕ*)
Lemma: nat-star-retract-id
∀[s:ℕ*]. (nat-star-retract(s) = s ∈ ℕ*)
Lemma: nat-star-retract-property
∀s:ℕ ⟶ ℕ. (∃n:ℕ. 0 < s n ⇐⇒ ∃n:ℕ. 0 < nat-star-retract(s) n)
Definition: nat-star-0
0 == λn.0
Lemma: nat-star-0_wf
0 ∈ ℕ*
Lemma: weak-Markov-principle2
∀a:ℕ*. ((∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))) ⇒ (∃n:ℕ. 0 < a n))
Lemma: weak-Markov-principle2-alt
∀a:ℕ*. ((∀c:ℕ*. ((¬(a = c ∈ ℕ*)) ∨ (¬(0 = c ∈ ℕ*)))) ⇒ (∃n:ℕ. 0 < a n))
Lemma: strong-continuity2-no-inner-squash-cantor
∀F:(ℕ ⟶ ℕ2) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ2) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ2. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f))))
Lemma: strong-continuity2-no-inner-squash-cantor2
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f))))
Lemma: strong-continuity2-no-inner-squash-cantor3
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ2
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ2?)
∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ2?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ2?) supposing ↑isl(M n f))))
Lemma: strong-continuity2-no-inner-squash-cantor4
∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (𝔹?)
∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (𝔹?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (𝔹?) supposing ↑isl(M n f))))
Lemma: strong-continuity2-no-inner-squash-cantor5
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℤ?)
∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℤ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℤ?) supposing ↑isl(M n f))))
Definition: int2nat
int2nat(i) == eval j = i in if (j) < (0) then (2 * ((-j) - 1)) + 1 else (2 * j)
Lemma: int2nat_wf
∀[i:ℤ]. (int2nat(i) ∈ ℕ)
Definition: nat2int
nat2int(m) == if m rem 2=0 then m ÷ 2 else (-((m ÷ 2) + 1))
Lemma: nat2int_wf
∀[n:ℕ]. (nat2int(n) ∈ ℤ)
Lemma: int2nat2int
∀[i:ℤ]. (nat2int(int2nat(i)) = i ∈ ℤ)
Lemma: strong-continuity2-implies-weak-skolem-cantor
∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕM f ⟶ 𝔹)) ⇒ F f = F g))
Lemma: strong-continuity2-implies-weak-skolem-cantor-nat
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕM f ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: general-uniform-continuity-from-fan
∀[B:ℕ ⟶ Type]
⇃(∀i:ℕ. ∀K:B[i] ⟶ ℕ. (∃Bnd:ℕ [(∀t:B[i]. ((K t) ≤ Bnd))]))
⇒ (∀[T:Type]
∀F:(i:ℕ ⟶ B[i]) ⟶ T
(⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ B[i]) ⟶ (T?) [(∀f:i:ℕ ⟶ B[i]
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
⇒ ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ B[i]. ((f = g ∈ (i:ℕn ⟶ B[i])) ⇒ ((F f) = (F g) ∈ T)))))
supposing ∀i:ℕ. B[i]
Lemma: general-uniform-continuity-from-fan-ext
∀[B:ℕ ⟶ Type]
⇃(∀i:ℕ. ∀K:B[i] ⟶ ℕ. (∃Bnd:ℕ [(∀t:B[i]. ((K t) ≤ Bnd))]))
⇒ (∀[T:Type]
∀F:(i:ℕ ⟶ B[i]) ⟶ T
(⇃(∃M:n:ℕ ⟶ (i:ℕn ⟶ B[i]) ⟶ (T?) [(∀f:i:ℕ ⟶ B[i]
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
⇒ ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ B[i]. ((f = g ∈ (i:ℕn ⟶ B[i])) ⇒ ((F f) = (F g) ∈ T)))))
supposing ∀i:ℕ. B[i]
Lemma: uniform-continuity-from-fan
∀[T:Type]
∀F:(ℕ ⟶ 𝔹) ⟶ T
(⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
⇒ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
Lemma: uniform-continuity-from-fan2
∀[T:Type]
((∃U:Type. ((U ⊆r ℕ) ∧ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U)) ∧ (∃h:T ⟶ U. Bij(T;U;h))))
⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ T. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T)))))
Lemma: uniform-continuity-from-fan3
∀[T:Type]
((∃P:ℕ ⟶ ℙ. ∃a:ℕ. (P[a] ∧ (∀n:ℕ. Dec(P[n])) ∧ (∃h:T ⟶ {n:ℕ| P[n]} . Bij(T;{n:ℕ| P[n]} ;h))))
⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ T. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T)))))
Definition: ucont
ucont(F;M) == eval K = FAN(λn,s. if M n s then tt else inr (λx.Ax) fi ) in <K - 1, λ_,_,_. Ax>
Lemma: uniform-continuity-from-fan-ext
∀[T:Type]
∀F:(ℕ ⟶ 𝔹) ⟶ T
(⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (T?) supposing ↑isl(M n f))))])
⇒ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
Lemma: ucont_wf
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[M:⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))
∧ (∀n:ℕ
(M n f) = (inl (F f)) ∈ (T?)
supposing ↑isl(M n f))))])].
(ucont(F;M) ∈ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))))
Lemma: strong-continuity2-implies-uniform-continuity
∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ F f = F g))
Lemma: strong-continuity2-implies-uniform-continuity-ext
∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ F f = F g))
Lemma: strong-continuity2-implies-uniform-continuity-nat
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: strong-continuity2-implies-uniform-continuity-nat-ext
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
Lemma: general-cantor-to-int-uniform-continuity-half-squashed
∀B:ℕ ⟶ ℕ+. ∀F:(i:ℕ ⟶ ℕB[i]) ⟶ ℤ. ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i]. ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
Lemma: strong-continuity2-implies-uniform-continuity-int
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ)))
Lemma: strong-continuity2-implies-uniform-continuity-int-ext
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ)))
Lemma: prop-truncation-implies
∀T:Type. ((∀a,b:T. (a = b ∈ T)) ⇒ ⇃(T) ⇒ T)
Lemma: prop-truncation-quot
∀T:Type. (⇃(⇃(T)) ⇒ ⇃(T))
Lemma: implies-prop-truncation
∀T:Type. (T ⇒ ⇃(T))
Definition: ext2Cantor
ext2Cantor(n;f;d) == λx.if x <z n then f x else d fi
Lemma: ext2Cantor_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ 𝔹]. ∀[d:𝔹]. (ext2Cantor(n;f;d) ∈ ℕ ⟶ 𝔹)
Lemma: eq_ext2Cantor
∀n:ℕ. ∀s:ℕn ⟶ 𝔹. ∀d1,d2:𝔹. (ext2Cantor(n;s;d1) = ext2Cantor(n;s;d2) ∈ (ℕn ⟶ 𝔹))
Lemma: fan+weak-continuity-implies-uniform-continuity
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
Definition: uniform-continuity-pi
ucA(T;F;n) == ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ T))
Lemma: uniform-continuity-pi_wf
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[n:ℕ]. (ucA(T;F;n) ∈ Type)
Definition: extl2Cantor
extl2Cantor(s;b) == λx.if x <z ||s|| then s[x] else b fi
Lemma: extl2Cantor_wf
∀[s:𝔹 List]. ∀[b:𝔹]. (extl2Cantor(s;b) ∈ ℕ ⟶ 𝔹)
Lemma: ext2Cantor_eq
∀[s:𝔹 List]. ∀[d:𝔹]. (ext2Cantor(||s||;λx.s[x];d) = extl2Cantor(s;d) ∈ (ℕ ⟶ 𝔹))
Lemma: fun2listCantor
∀n:ℕ. ∀f:ℕn ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))
Definition: uniform-continuity-pi2
ucB(T;F;n) == ∀s:ℕn ⟶ 𝔹. ((F ext2Cantor(n;s;tt)) = (F ext2Cantor(n;s;ff)) ∈ T)
Lemma: uniform-continuity-pi2_wf
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[n:ℕ]. (ucB(T;F;n) ∈ Type)
Lemma: decidable__bool
Dec(𝔹)
Lemma: uniform-continuity-pi2-dec
∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ∀n:ℕ. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ Dec(ucB(T;F;n)))
Lemma: uniform-continuity-pi2-dec-ext
∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ∀n:ℕ. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ Dec(ucB(T;F;n)))
Lemma: uniform-continuity-pi-dec
∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ∀n:ℕ. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ ucA(T;F;n) ⇒ (∀m:ℕ. (m < n ⇒ Dec(ucA(T;F;m)))))
Definition: uniform-continuity-pi-pi
ucpB(T;F;n) == ucA(T;F;n) × (∀i:ℕ. (ucA(T;F;i) ⇒ (n ≤ i)))
Lemma: uniform-continuity-pi-pi_wf
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[n:ℕ]. (ucpB(T;F;n) ∈ Type)
Lemma: uniform-continuity-pi-pi-prop
∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[n,m:ℕ]. (n = m ∈ ℕ) supposing (ucpB(T;F;m) and ucpB(T;F;n))
Definition: uniform-continuity-pi-search
uniform-continuity-pi-search(
G;
n;x)
==r if n ≤z x then n
if isl(G x) then x
else uniform-continuity-pi-search(
G;
n;x + 1)
fi
Lemma: uniform-continuity-pi-search_wf
∀[n:ℕ]. ∀[G:∀m:ℕn. (Top + Top)]. ∀[x:ℕ]. (uniform-continuity-pi-search(G;n;x) ∈ ℕ)
Lemma: uniform-continuity-pi-search-prop1
∀[n:ℕ]. ∀[P:ℕ ⟶ ℙ]. ∀[G:∀m:ℕn. Dec(P[m])]. ∀[x:ℕ].
(uniform-continuity-pi-search(G;n;x) ∈ {k:{x..n + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m]))} ) supposing ((x ≤ n) and (∃n:{x..\000Cn + 1-}. P[n]))
Lemma: uniform-continuity-pi-search-prop2
∀[n:ℕ]. ∀[P:ℕ ⟶ ℙ]. ∀[G:∀m:ℕn. Dec(P[m])]. ∀[x:ℕ].
(uniform-continuity-pi-search(
G;
n;x) ∈ {k:{x..n + 1-}| P[k] ∧ (∀m:{x..k-}. (¬P[m])) ∧ (∀m:{x..n + 1-}. (P[m] ⇒ (k ≤ m)))} ) supposing
((x ≤ n) and
(∃n:{x..n + 1-}. P[n]))
Lemma: uniform-continuity-pi-pi-prop2
∀T:Type. ∀F:(ℕ ⟶ 𝔹) ⟶ T. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∃n:ℕ. ucpB(T;F;n) ⇐⇒ ∃n:ℕ. ucA(T;F;n)))
Lemma: strong-continuity2-implies-uniform-continuity2
∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹. ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ F f = F g)
Lemma: strong-continuity2-implies-uniform-continuity2-int
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ))
Lemma: strong-continuity2-implies-uniform-continuity2-nat
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ))
Lemma: general-cantor-to-int-uniform-continuity
∀B:ℕ ⟶ ℕ+. ∀F:(k:ℕ ⟶ ℕB[k]) ⟶ ℤ. ∃n:ℕ. ∀f,g:k:ℕ ⟶ ℕB[k]. ((f = g ∈ (k:ℕn ⟶ ℕB[k])) ⇒ ((F f) = (F g) ∈ ℤ))
Lemma: cantor-to-int-uniform-continuity
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ))
Lemma: cantor-to-int-bounded
∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)
Lemma: bounded-type-cantor
Bounded(ℕ ⟶ 𝔹)
Lemma: cantor-to-general-cantor
∀B:ℕ ⟶ ℕ+
∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
(Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹. ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))
Lemma: general-cantor-to-int-bounded
∀B:ℕ ⟶ ℕ+. ∀F:(n:ℕ ⟶ ℕB[n]) ⟶ ℤ. ∃bnd:ℕ. ∀f:n:ℕ ⟶ ℕB[n]. (|F f| ≤ bnd)
Lemma: decidable-cantor-to-int
∀[R:ℤ ⟶ ℤ ⟶ ℙ]. ((∀x,y:ℤ. Dec(R[x;y])) ⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. Dec(∃f,g:ℕ ⟶ 𝔹. R[F f;F g])))
Lemma: decidable-cantor-to-int-ext
∀[R:ℤ ⟶ ℤ ⟶ ℙ]. ((∀x,y:ℤ. Dec(R[x;y])) ⇒ (∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. Dec(∃f,g:ℕ ⟶ 𝔹. R[F f;F g])))
Definition: ext2Baire
ext2Baire(n;f;d) == λx.if x <z n then f x else d fi
Lemma: ext2Baire_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. ∀[d:ℕ]. (ext2Baire(n;f;d) ∈ ℕ ⟶ ℕ)
Lemma: weak-continuity-implies-strong1
(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))))
⇒ (∀F:(ℕ ⟶ ℕ) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
∀f:ℕ ⟶ ℕ
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f)))))
Lemma: weak-continuity-implies-strong-cantor
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ
∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
∀f:ℕ ⟶ 𝔹. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (ℕ?) supposing ↑isl(M n f)))
Lemma: weak-continuity-implies-strong-cantor-unique
∀F:(ℕ ⟶ 𝔹) ⟶ ℕ
∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
Lemma: strong-continuity2-no-inner-squash-bound
∀F:(ℕ ⟶ ℕ) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ. (F f < n ∧ ((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl (F f)) ∈ (ℕ?))))))
Definition: strong-continuity-test-bound
strong-continuity-test-bound(M;n;f;b) ==
primrec(n;inr Ax ;λi,r. if i <z b then inr Ax if (i =z b) then inl b if isl(M i f) then inr Ax else r fi )
Lemma: strong-continuity-test-bound_wf
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕn]. (strong-continuity-test-bound(M;n;f;b) ∈ ℕn?)
Lemma: strong-continuity-test-bound-unroll
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f,b:Top].
(strong-continuity-test-bound(M;n;f;b) ~ if (n =z 0) then inr Ax
if n - 1 <z b then inr Ax
if (n - 1 =z b) then inl b
if isl(M (n - 1) f) then inr Ax
else strong-continuity-test-bound(M;n - 1;f;b)
fi )
Lemma: strong-continuity-test-bound-prop1
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕn].
((↑isl(strong-continuity-test-bound(M;n;f;b))) ⇒ (strong-continuity-test-bound(M;n;f;b) = (inl b) ∈ (ℕn?)))
Lemma: strong-continuity-test-bound-prop2
∀[T:Type]. ∀[M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕn?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[b:ℕn].
((↑isl(strong-continuity-test-bound(M;n;f;b))) ⇒ (∀i:ℕ. (b < i ⇒ i < n ⇒ (↑isr(M i f)))))
Lemma: strong-continuity-test-bound-prop3
∀[M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)]. ∀[n,m:ℕ]. ∀[f:ℕ ⟶ ℕ]. ∀[b:ℕn].
(b < m
⇒ (↑isl(M n f))
⇒ (↑isl(M m f))
⇒ (↑isl(strong-continuity-test-bound(M;n;f;b)))
⇒ (↑isl(strong-continuity-test-bound(M;m;f;b)))
⇒ (m = n ∈ ℕ))
Lemma: strong-continuity-test-bound-prop4
∀M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?). ∀n:ℕ. ∀f:ℕn ⟶ ℕ. ∀b:ℕn.
((↑isr(strong-continuity-test-bound(M;n;f;b)))
⇒ (∃m:ℕ. (b < m ∧ m < n ∧ (↑isl(M m f)) ∧ (↑isl(strong-continuity-test-bound(M;m;f;b))))))
Lemma: strong-continuity2-no-inner-squash-unique-bound
∀F:(ℕ ⟶ ℕ) ⟶ ℕ
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ. ∃n:ℕ. (F f < n ∧ ((M n f) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ)))))
Lemma: monotone-bar-induction1
∀[B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ].
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (∀m:ℕ. B[n + 1;s.m@n])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (↓Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. (↓Q[n + 1;s.m@n])) ⇒ (↓Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ∃m:ℕ. B[m;alpha])
⇒ (↓Q[0;λx.⊥]))
Lemma: monotone-bar-induction2
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (∀m:ℕ. B[n + 1;s.m@n])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ∃m:ℕ. B[m;alpha])
⇒ ⇃(Q[0;λx.⊥]))
Lemma: strong-continuity-implies1-sp
∀[F:(ℕ ⟶ ℕ) ⟶ ℕ]. (↓∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?). ∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. ((M n f) = (inl (F f)) ∈ (ℕ?))))
Definition: strong-continuity-test-sp
strong-continuity-test-sp(M;n;f;k) ==
primrec(n;inl k;λi,r. case M i f of inl(m) => if (m =z k) then inr Ax else r fi | inr(x) => r)
Lemma: strong-continuity-test-sp_wf
∀[M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)]. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. ∀[k:ℕ]. (strong-continuity-test-sp(M;n;f;k) ∈ ℕ?)
Lemma: quot-implies-squash
∀P:ℙ. (⇃(P) ⇒ (↓P))
Lemma: all-quotient-dependent
∀T:Type
(canonicalizable(T)
⇒ (∀S:T ⟶ ℙ. ∀E:t:T ⟶ S[t] ⟶ S[t] ⟶ ℙ.
((∀t:T. EquivRel(S t;a,b.E[t;a;b]))
⇒ (∀t:T. (x,y:S[t]//E[t;x;y]) ⇐⇒ f,g:∀t:T. S[t]//dep-fun-equiv(T;t,x,y.↓E[t;x;y];f;g)))))
Lemma: all-quotient
∀T:Type
(canonicalizable(T)
⇒ (∀S:Type. ∀E:S ⟶ S ⟶ ℙ.
(EquivRel(S;a,b.E[a;b]) ⇒ (∀t:T. (x,y:S//E[x;y]) ⇐⇒ f,g:∀t:T. S//fun-equiv(T;a,b.↓E[a;b];f;g)))))
Lemma: all-quotient-true
∀T:Type. (⇃(canonicalizable(T)) ⇒ (∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))))
Lemma: all-quotient-true2
∀T:Type. ((T ⊆r Base) ⇒ (∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))))
Lemma: all-quotient-true3
∀T:Type. (canonicalizable(T) ⇒ (∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))))
Definition: choice-principle
If P is a family of propositions (i.e. types) indexed by type T,
then for each t:T, P[t] is a type.
The type ∀t:T. P[t] is by definition the dependent function type
t:T ⟶ P[t]
One way to say that a type A is inhabited is the "truncation"
or "half squash" ⇃(A) which is the quotient A//True.
The choice principle for T says that every P[t] is inhabited
if and only if the function type t:T ⟶ P[t] is inhabited.
We prove that ChoicePrinciple(T) ⇐⇒ ⇃(canonicalizable(T))
(see choice-iff-canonicalizable).
Therefore we can prove ChoicePrinciple(ℕ) and ChoicePrinciple(ℕ ⟶ ℕ)
but we can also prove ¬ChoicePrinciple((ℕ ⟶ ℕ) ⟶ ℕ)
(see not-choice-baire-to-nat).
So the choice principle is true for type 0 and type 1 but false for type 2.⋅
ChoicePrinciple(T) == ∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))
Lemma: choice-principle_wf
∀[T:Type]. (ChoicePrinciple(T) ∈ 𝕌')
Lemma: choice-iff-canonicalizable
∀T:Type. (ChoicePrinciple(T) ⇐⇒ ⇃(canonicalizable(T)))
Definition: truth
Truth == P,Q:ℙ//(P ⇐⇒ Q)
Lemma: truth_wf
Truth ∈ 𝕌'
Lemma: axiom-choice-quot
∀T:Type
(⇃(canonicalizable(T)) ⇒ (∀X:Type. ∀P:T ⟶ X ⟶ ℙ. ((∀f:T. ⇃(∃m:X. (P f m))) ⇒ ⇃(∃F:T ⟶ X. ∀f:T. (P f (F f))))))
Lemma: axiom-choice-quot-alt-proof
∀T:Type
(⇃(canonicalizable(T)) ⇒ (∀X:Type. ∀P:T ⟶ X ⟶ ℙ. ((∀f:T. ⇃(∃m:X. (P f m))) ⇒ ⇃(∃F:T ⟶ X. ∀f:T. (P f (F f))))))
Lemma: axiom-choice-C0
∀P:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃m:ℕ. (P m f))) ⇒ ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (P (F f) f)))
Lemma: axiom-choice-0X-quot
∀B:{B:Type| B ⊆r Base} . ∀X:Type. ∀P:B ⟶ X ⟶ ℙ. ((∀n:B. ⇃(∃m:X. (P n m))) ⇒ ⇃(∃f:B ⟶ X. ∀n:B. (P n (f n))))
Lemma: axiom-choice-1X-quot
∀X:Type. ∀P:(ℕ ⟶ ℕ) ⟶ X ⟶ ℙ. ((∀f:ℕ ⟶ ℕ. ⇃(∃m:X. (P f m))) ⇒ ⇃(∃F:(ℕ ⟶ ℕ) ⟶ X. ∀f:ℕ ⟶ ℕ. (P f (F f))))
Lemma: axiom-choice-00-quot
∀P:ℕ ⟶ ℕ ⟶ ℙ. ((∀n:ℕ. ⇃(∃m:ℕ. (P n m))) ⇒ ⇃(∃f:ℕ ⟶ ℕ. ∀n:ℕ. (P n (f n))))
Lemma: choice-nat
ChoicePrinciple(ℕ)
Lemma: choice-baire
ChoicePrinciple(ℕ ⟶ ℕ)
Lemma: not-choice-baire-to-nat
¬ChoicePrinciple((ℕ ⟶ ℕ) ⟶ ℕ)
Lemma: not-choice-baire-to-nat-ssq
¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t]) ⇐⇒ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
Lemma: not-canonicalizable-baire-to-nat
¬⇃(canonicalizable((ℕ ⟶ ℕ) ⟶ ℕ))
Lemma: not-canonicalizable-implies-subtype-base
¬(∀[T:Type]. (canonicalizable(T) ⇒ (T ⊆r Base)))
Lemma: notAC20
∀T:Type
(⇃T
⇒ (¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃∃m:T. (P n m)) ⇒ ⇃∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))))
Lemma: notAC20-ssq
∀T:Type
((↓T)
⇒ (¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m))) ⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n)))))))
Lemma: strong-continuity-rel
∀P:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ. ∀F:∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n)).
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
Lemma: weak-continuity-rel
∀P:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
((∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n,k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g n)))))
Lemma: weak-continuity-rel-fun
∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ((∀f:ℕ ⟶ ℕ. ⇃(P f)) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
Lemma: strong-continuity-rel-unique
∀P:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ. ∀F:∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n)).
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ)))))
Lemma: strong-continuity-rel-unique-pair
∀P:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ. ∀F:∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n)).
⇃(∃M:n:ℕ ⟶ s:(ℕn ⟶ ℕ) ⟶ (k:ℕn × (P ext2Baire(n;s;0) k)?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
∃p:P ext2Baire(n;f;0) k
(((M n f) = (inl <k, p>) ∈ (k:ℕn × (P ext2Baire(n;f;0) k)?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ)))))
Lemma: seq-adjoin-is-seq-add
∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. ∀[m:ℕ]. (s.m@n = s++m ∈ (ℕn + 1 ⟶ ℕ))
Lemma: seq-append0-left
∀[t:Top]. ∀[m:ℕ]. ∀[f:ℕm ⟶ ℕ]. (seq-append(0;m;t;f) = f ∈ (ℕm ⟶ ℕ))
Lemma: seq-append-bar
∀k:ℕ. ∀s:ℕk ⟶ ℕ. ∀x:ℕ. ∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:{n...}. Q[m + k;seq-append(k;m;s;f)])
⇒ (∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:{n...}. Q[m + k;seq-append(k + 1;m;s.x@k;f)]))
Lemma: monotone-bar-induction3
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (∀m:ℕ. B[n + 1;s.m@n])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃m:ℕ. B[m;alpha]))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction3-2
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (∀m:ℕ. B[n + 1;s.m@n])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃m:ℕ. B[m;alpha]))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction4
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ
⇃(∃n:ℕ. (B[n;alpha] ∧ (∀m:{n...}. ∀s:ℕm ⟶ ℕ. ((alpha = s ∈ (ℕm ⟶ ℕ)) ⇒ B[m;s] ⇒ (∀k:ℕ. B[m + 1;s.k@m]))))))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction5
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (B[n;alpha] ∧ (∀m:{n...}. (B[m;alpha] ⇒ B[m + 1;alpha])))))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction6
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (B[n;alpha] ∧ (∀m:{n...}. B[m;alpha]))))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction7
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (B[n;alpha] ∧ (∀m:{n...}. (B[m;alpha] ∧ ⇃(Q[m;alpha]))))))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction8
∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. ⇃(Q[m;f])))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction8-2
∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s])) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f])) ⇒ ⇃(Q[0;λx.⊥]))
Definition: rep-seq-from
rep-seq-from(s;n;f) == λx.if (x) < (n) then s x else (f x)
Lemma: rep-seq-from_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[f:ℕ ⟶ T]. (rep-seq-from(s;n;f) ∈ ℕ ⟶ T)
Lemma: rep-seq-from-0
∀[T:Type]. ∀[s:ℕ0 ⟶ T]. ∀[f:ℕ ⟶ T]. (rep-seq-from(s;0;f) = f ∈ (ℕ ⟶ T))
Lemma: rep-seq-from-prop1
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[f:ℕ ⟶ T]. ∀[m:{n...}]. (rep-seq-from(s;m;f) = s ∈ (ℕn ⟶ T))
Lemma: rep-seq-from-prop2
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[f:ℕ ⟶ T]. ∀[m:ℕ]. (rep-seq-from(s.f m@m;m + 1;f) = rep-seq-from(s;m;f) ∈ (ℕn ⟶ T))
Lemma: rep-seq-from-prop3
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ T]. ∀[f:ℕ ⟶ T]. (rep-seq-from(s.f n@n;n + 1;f) = rep-seq-from(s;n;f) ∈ (ℕ ⟶ T))
Lemma: unsquashed-monotone-bar-induction8-false
¬(∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s])) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. Q[m;f])) ⇒ Q[0;λx.⊥]))
Lemma: unsquashed-monotone-bar-induction8-false3
¬(∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. B[m;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ Q[0;λx.⊥]))
Lemma: unsquashed-BIM-implies-unsquashed-weak-continuity-old
(∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. Q[n;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (B[n;s] ⇒ B[n + 1;s.m@n]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ Q[0;λx.⊥]))
⇒ (∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ)))
Lemma: unsquashed-BIM-implies-unsquashed-weak-continuity
(∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (B[n;s] ⇒ B[n + 1;s.m@n]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ Q[0;λx.⊥]))
⇒ (∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((∀i:ℕn. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ)))
Lemma: unsquashed-monotone-bar-induction3-false
¬(∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (B[n;s] ⇒ B[n + 1;s.m@n]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ Q[0;λx.⊥]))
Lemma: unsquashed-BIM-false
¬(∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;f]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ. (B[n;s] ⇒ B[n + 1;s.m@n]))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]))
⇒ Q[0;λx.⊥]))
Lemma: seq-add-same
∀[f:ℕ ⟶ ℕ]. ∀[n:ℕ]. (f.f n@n = f ∈ (ℕ ⟶ ℕ))
Lemma: monotone-bar-induction8-implies-3
(∀Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. ⇃(Q[m;f])))
⇒ ⇃(Q[0;λx.⊥])))
⇒ (∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ.
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ (∀m:ℕ. B[n + 1;s.m@n])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n])) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:ℕ ⟶ ℕ. ⇃(∃m:ℕ. B[m;alpha]))
⇒ ⇃(Q[0;λx.⊥])))
Lemma: not-decidable-zero-sequence
¬(∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ)))))
Lemma: not-excluded-middle-thru-continuity
¬(∀P:ℙ. (P ∨ (¬P)))
Lemma: extended-fan-theorem
∀C:ℕ ⟶ (ℕ ⟶ 𝔹) ⟶ ℙ
((∀a:ℕ ⟶ 𝔹. ∃n:ℕ. (C n a)) ⇒ ⇃(∃m:ℕ. ∀a:ℕ ⟶ 𝔹. ∃n:ℕ. ∀b:ℕ ⟶ 𝔹. ((a = b ∈ (ℕm ⟶ 𝔹)) ⇒ (C n b))))
Lemma: extended-fan-theorem2
∀C:ℕ ⟶ (ℕ ⟶ 𝔹) ⟶ ℙ. ∀F:∀a:ℕ ⟶ 𝔹. ∃n:ℕ. (C n a). ⇃(∃m:ℕ. ∀a,b:ℕ ⟶ 𝔹. ((a = b ∈ (ℕm ⟶ 𝔹)) ⇒ (C (fst((F a))) b)))
Definition: enum-fin-seq
enum-fin-seq(m) == primrec(m;[λx.tt];λi,r. (map(λs,x. if x=i then tt else (s x);r) @ map(λs,x. if x=i then ff else (s x\000C);r)))
Lemma: enum-fin-seq_wf
∀[m:ℕ]. (enum-fin-seq(m) ∈ ℕ ⟶ 𝔹 List(2^m))
Lemma: enum-fin-seq-true
∀m:ℕ. ((λx.tt) = enum-fin-seq(m)[0] ∈ (ℕ ⟶ 𝔹))
Definition: enum-fin-seq-max
enum-fin-seq-max(M;m) == imax-list(map(λs.(M s);enum-fin-seq(m)))
Lemma: enum-fin-seq-max_wf
∀[M:(ℕ ⟶ 𝔹) ⟶ ℕ]. ∀[m:ℕ]. (enum-fin-seq-max(M;m) ∈ ℕ)
Definition: enum-fin-seq-max2
enum-fin-seq-max2(M;m) == imax-list(map(λs.case M m s of inl(k) => k + 1 | inr(x) => 0;enum-fin-seq(m)))
Lemma: enum-fin-seq-max2_wf
∀[M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)]. ∀[m:ℕ]. (enum-fin-seq-max2(M;m) ∈ ℕ)
Definition: replace-seq-from
replace-seq-from(s;n;k) == λx.if (x) < (n) then s x else k
Lemma: replace-seq-from_wf
∀[T:Type]. ∀[s:ℕ ⟶ T]. ∀[n:ℕ]. ∀[k:T]. (replace-seq-from(s;n;k) ∈ ℕ ⟶ T)
Lemma: replace-seq-from-succ
∀T:Type. ∀f:ℕ ⟶ T. ∀m:ℕ. ∀k:T.
(0 < m ⇒ (replace-seq-from(f;m;k) = (λx.if x=m - 1 then f x else (replace-seq-from(f;m - 1;k) x)) ∈ (ℕ ⟶ T)))
Lemma: implies_l_member_append
∀T:Type. ∀l1,l2:T List. ∀v:T. (((v ∈ l1) ∨ (v ∈ l2)) ⇒ (v ∈ l1 @ l2))
Lemma: replace-seq-from-member-enum
∀f:ℕ ⟶ 𝔹. ∀m:ℕ. (replace-seq-from(f;m;tt) ∈ enum-fin-seq(m))
Lemma: imax-list-strict-ub
∀L:ℤ List. ∀a:ℤ. a < imax-list(L) ⇐⇒ (∃b∈L. a < b) supposing 0 < ||L||
Comment: Veldman-Bezem-Ramsey doc
The paper
"Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics"
by Veldman & Bezem uses bar induction on monotone bars to prove
a version of Ramsey's theorem.
We give a formalization of those results in Nuprl.⋅
Definition: strict-inc
StrictInc == {s:ℕ ⟶ ℕ| ∀j:ℕ. ∀i:ℕj. s i < s j}
Lemma: strict-inc_wf
StrictInc ∈ Type
Lemma: strict-inc-subtype
∀m:ℕ. (StrictInc ⊆r {s:ℕm ⟶ ℕ| strictly-increasing-seq(m;s)} )
Lemma: implies-strict-inc
∀[f:ℕ ⟶ ℕ]. f ∈ StrictInc supposing ∀i:ℕ. f i < f (i + 1)
Lemma: strict-inc-lower-bound
∀[f:StrictInc]. ∀[i:ℕ]. (i ≤ (f i))
Lemma: compose-strict-inc
∀s,f:StrictInc. (s o f ∈ StrictInc)
Definition: make-strict
make-strict(alpha) == λi.primrec(i;alpha 0;λi',v. if v <z alpha (i' + 1) then alpha (i' + 1) else v + 1 fi )
Lemma: make-strict_wf
∀[alpha:ℕ ⟶ ℕ]. (make-strict(alpha) ∈ StrictInc)
Lemma: make-strict-agrees
∀[alpha:ℕ ⟶ ℕ]. ∀[n:ℕ]. ∀[i:ℕn]. ((make-strict(alpha) i) = (alpha i) ∈ ℤ) supposing strictly-increasing-seq(n;alpha)
Lemma: monotone-bar-induction-strict
∀[B,Q:n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ].
((∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n]))))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ (↓Q[n;s])))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ (↓Q[n + 1;s.m@n]))) ⇒ (↓Q[n;s])))
⇒ (∀alpha:StrictInc. ∃m:ℕ. B[m;alpha])
⇒ (↓Q[0;λx.⊥]))
Lemma: monotone-bar-induction-strict2
∀B,Q:n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ.
((∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n]))))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ ⇃(Q[n + 1;s.m@n]))) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:StrictInc. ∃m:ℕ. B[m;alpha])
⇒ ⇃(Q[0;λx.⊥]))
Lemma: monotone-bar-induction-strict3
∀B,Q:n:ℕ ⟶ {s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} ⟶ ℙ.
((∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(B[n;s] ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ B[n + 1;s.m@n]))))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} . (B[n;s] ⇒ ⇃(Q[n;s])))
⇒ (∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
((∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ ⇃(Q[n + 1;s.m@n]))) ⇒ ⇃(Q[n;s])))
⇒ (∀alpha:StrictInc. ⇃(∃m:ℕ. B[m;alpha]))
⇒ ⇃(Q[0;λx.⊥]))
Lemma: not-not-Ramsey
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. (¬(∀s:StrictInc. ∃n:ℕ. (¬homogeneous(R;n;s))))
Lemma: unary-strong-almost-full-has-strict-inc
∀[A:ℕ ⟶ ℙ]. ((∀s:StrictInc. ∃n:ℕ. A[s n]) ⇒ (∃s:StrictInc. ∀n:ℕ. A[s n]))
Lemma: unary-almost-full-has-strict-inc
∀A:ℕ ⟶ ℙ. ((∀s:StrictInc. ⇃(∃n:ℕ. A[s n])) ⇒ ⇃(∃s:StrictInc. ∀n:ℕ. A[s n]))
Lemma: intuitionistic-pigeonhole1
∀[A,B:ℕ ⟶ ℙ].
((∀s:StrictInc. ∃n:ℕ. A[s n]) ⇒ (∀s:StrictInc. ∃n:ℕ. B[s n]) ⇒ (∀s:StrictInc. ∃n:ℕ. (A[s n] ∧ B[s n])))
Lemma: intuitionistic-pigeonhole
∀A,B:ℕ ⟶ ℙ.
((∀s:StrictInc. ⇃(∃n:ℕ. A[s n])) ⇒ (∀s:StrictInc. ⇃(∃n:ℕ. B[s n])) ⇒ (∀s:StrictInc. ⇃(∃n:ℕ. (A[s n] ∧ B[s n]))))
Definition: u-almost-full
u-almost-full(n.A[n]) == ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])
Lemma: u-almost-full_wf
∀[A:ℕ ⟶ ℙ]. (u-almost-full(n.A[n]) ∈ ℙ)
Lemma: u-almost-full-filter
∀A,B:ℕ ⟶ ℙ.
((u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]) ⇒ u-almost-full(n.A[n] ∧ B[n]))
∧ ((∀n:ℕ. (A[n] ⇒ B[n])) ⇒ u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]))
∧ u-almost-full(n.True))
Lemma: u-almost-full-finite-intersection
∀k:ℕ. ∀A:ℕk ⟶ ℕ ⟶ ℙ. ((∀i:ℕk. u-almost-full(n.A[i;n])) ⇒ u-almost-full(n.∀i:ℕk. A[i;n]))
Lemma: finite-Ramsey1
∀c:ℕ. ∀s:ℕc ⟶ ℕ.
∃N:ℕ+
∀g:ℕN ⟶ ℕN ⟶ ℕc. ∃i:ℕc. ∃f:ℕs i ⟶ ℕN. (Inj(ℕs i;ℕN;f) ∧ (∀a,b:ℕs i. (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))))
Lemma: finite-Ramsey
∀k,n:ℕ.
∃N:ℕ+
∀g:ℕN ⟶ ℕN ⟶ ℕk
∃f:ℕn ⟶ ℕN. (Inj(ℕn;ℕN;f) ∧ (∀a,b,c,d:ℕn. (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))))
Lemma: Ramsey-n-3
∀n:ℕ. ∃N:ℕ+. ∀g:ℕN ⟶ ℕN ⟶ ℕn. ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))
Definition: b-almost-full
A binary relation R on ℕ is almost full if every strictly increasing sequence s
must have a pair s(n), s(m) (with n < m) related by R.
But the n and m need not be an extensional property of s because we have
"squashed" the proposition ⌜∃n:ℕ. ∃m:{n + 1...}. R[s n; s m]⌝
using the quotient by //True.
This allows us to prove that relations are almost full using
bar induction on monotone bars, which relies on continuity -- which is
not extensional.
The key lemma used to prove the Intuitionistic Ramsey Theorem (Veldman & Bezem)
(See intuitionistic-Ramsey) is b-almost-full-intersection, which
uses monotone-bar-induction-strict3
That is a variant of bar induction on monotone bars, which follows from
bar induction on decidable bars and the strong continuity principle
-- two Brouwerian principles that we have proved to be true in Nuprl
using our Nuprl-in-Coq meta-theory.
⋅
b-almost-full(n,m.R[n; m]) == ∀s:StrictInc. ⇃(∃n:ℕ. ∃m:{n + 1...}. R[s n; s m])
Lemma: b-almost-full_wf
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. (b-almost-full(n,m.R[n;m]) ∈ ℙ)
Lemma: b-almost-full-intersection-lemma
∀R,T:ℕ ⟶ ℕ ⟶ ℙ.
(b-almost-full(n,m.R[n;m])
⇒ b-almost-full(n,m.T[n;m])
⇒ (∀s:StrictInc. ⇃(∃m:ℕ. ∃n,p:{m + 1...}. (R[s m;s n] ∧ T[s m;s p]))))
Lemma: better-not-not-Ramsey
∀[R:ℕ ⟶ ℕ ⟶ ℙ]. (¬(∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ. ((n < m ∧ R[s n;s m]) ∧ p < q ∧ (¬R[s p;s q])))))
Definition: baf-bar
baf-bar(n,m.R[n; m];n,m.T[n; m];l;a) ==
strictly-increasing-seq(l;a) ∧ (∃i:ℕl. ∃j,k:{i + 1..l-}. (R[a i; a j] ∧ T[a i; a k]))
Lemma: baf-bar_wf
∀[R,T:ℕ ⟶ ℕ ⟶ ℙ]. ∀[l:ℕ]. ∀[a:x:ℕl ⟶ ℕ]. (baf-bar(n,m.R[n;m];n,m.T[n;m];l;a) ∈ ℙ)
Lemma: baf-bar-monotone
∀R,T:ℕ ⟶ ℕ ⟶ ℙ. ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
(baf-bar(n,m.R[n;m];n,m.T[n;m];n;s)
⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ baf-bar(n,m.R[n;m];n,m.T[n;m];n + 1;s.m@n))))
Lemma: b-almost-full-intersection
This is the main technical lemma from Veldman & Bezem's proof
of the Intuitionistic Ramsey theorem.
We were able to closely follow their proof except that
before carrying out some of the reasoning steps we have to
"unsquash" some of the hypotheses.
The needed "unsquashing" is usually done using lemmas
implies-quotient-true or all-quotient-true
(making use of the fact that we can prove canonicalizable(StrictInc)).⋅
∀R,T:ℕ ⟶ ℕ ⟶ ℙ. (b-almost-full(n,m.R[n;m]) ⇒ b-almost-full(n,m.T[n;m]) ⇒ ⇃(∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m])))
Lemma: intuitionistic-Ramsey
∀R,T:ℕ ⟶ ℕ ⟶ ℙ. (b-almost-full(n,m.R[n;m]) ⇒ b-almost-full(n,m.T[n;m]) ⇒ b-almost-full(n,m.R[n;m] ∧ T[n;m]))
Lemma: b-almost-full-filter
∀A,B:ℕ ⟶ ℕ ⟶ ℙ.
((b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m]) ⇒ b-almost-full(n,m.A[n;m] ∧ B[n;m]))
∧ ((∀n,m:ℕ. (A[n;m] ⇒ B[n;m])) ⇒ b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m]))
∧ b-almost-full(n,m.True))
Lemma: general-fan-theorem-troelstra
∀X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ∃n:ℕ. X[n;f]) ⇒ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]))
Lemma: general-fan-theorem-troelstra-sq
∀X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])) ⇒ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]))
Lemma: general-fan-theorem-troelstra2
∀X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ∃n:ℕ. X[n;f]) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]))
Comment: Veldman's reverse AC doc
The "axiom of choice" ⌜(∀n:ℕ. ∃m:T. (A n m)) ⇒ (∃g:ℕ ⟶ T. ∀n:ℕ. (A n (g n)))⌝
follows from the definition of the quantifiers in type theory.
In "On the Constructive Contrapositions of Two Axioms of Countable Choice",
Veldman (1982) considered the contrapositive of the above:
⌜(∀g:ℕ ⟶ T. ∃n:ℕ. (R n (g n))) ⇒ (∃n:ℕ. ∀m:T. (R n m))⌝ (where R is ¬A).
In "The Contrapositive of Countable Choice for Inhabited Sets of Naturals",
Petrakis uses CCC(T) for ⌜∀R:ℕ ⟶ T ⟶ ℙ. ((∀g:ℕ ⟶ T. ∃n:ℕ. (R n (g n))) ⇒ (∃n:ℕ. ∀m:T. (R n m)))⌝
and dCCC(T) for ∀R:ℕ ⟶ T ⟶ 𝔹. ((∀g:ℕ ⟶ T. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:T. (↑(R n m))))
(i.e. where R is decidable).
Veldman proved (using the general Fan theorem) that CCC(T) is true for
finite types T and that CCC(ℕ) is false (even dCCC(ℕ) is false).
We prove those results here CCC-finite, not-d-CCC-nat.
Petrakis gives a simpler proof of dCCC(T) for finite T that does not use
any form of the fan theorem. We give an even simpler proof of that
here d-CCC-finite.
Petrakis studies the inhabited subtypes K ⊆r ℕ for which CCC(K),
so we define CCCNSet(K) == (K ⊆r ℕ) ∧ K ∧ CCC(K).
Petrakis's main result is that ⌜CCCNSet(K) ⇒ finite(K)⌝.
Combined with Veldman's result that ⌜finite(T) ⇒ CCC(T)⌝ we get
CCC(K) ⇐⇒ finite(K) for inhabited subtypes of ℕ
ccc-nset-iff-finite
⋅
Definition: contra-cc
CCC(T) == ∀R:ℕ ⟶ T ⟶ ℙ. ((∀g:ℕ ⟶ T. ∃n:ℕ. (R n (g n))) ⇒ (∃n:ℕ. ∀m:T. (R n m)))
Definition: contra-dcc
dCCC(T) == ∀R:ℕ ⟶ T ⟶ 𝔹. ((∀g:ℕ ⟶ T. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:T. (↑(R n m))))
Lemma: contra-dcc_wf
∀[T:Type]. (dCCC(T) ∈ ℙ)
Lemma: contra-cc_wf
∀[T:Type]. (CCC(T) ∈ ℙ')
Lemma: d-CCC-finite
∀[T:Type]. (finite(T) ⇒ dCCC(T))
Lemma: not-d-CCC-nat
¬dCCC(ℕ)
Lemma: CCC-bool
CCC(𝔹)
Lemma: d-CCC-surjection
∀[A,B:Type]. ((∃f:A ⟶ B. Surj(A;B;f)) ⇒ dCCC(A) ⇒ dCCC(B))
Lemma: not-d-CCC-infinite
∀[A:Type]. ((∃f:A ⟶ ℕ. Surj(A;ℕ;f)) ⇒ (¬dCCC(A)))
Lemma: not-CCC-infinite
∀[A:Type]. ((∃f:A ⟶ ℕ. Surj(A;ℕ;f)) ⇒ (¬CCC(A)))
Lemma: CCC-surjection
∀[A,B:Type]. ((∃f:A ⟶ B. Surj(A;B;f)) ⇒ CCC(A) ⇒ CCC(B))
Lemma: CCC-product
∀A,B:Type. (CCC(A) ⇒ CCC(B) ⇒ CCC(A × B))
Lemma: CCC-finite
∀[T:Type]. (finite(T) ⇒ CCC(T))
Lemma: CCC-nat2K-implies-CCC-K
∀[K:Type]. (CCC(ℕ ⟶ K) ⇒ CCC(K))
Definition: dccc-nset
dccc-nset(K) == (K ⊆r ℕ) ∧ K ∧ dCCC(K)
Lemma: dccc-nset_wf
∀[K:Type]. (dccc-nset(K) ∈ ℙ)
Definition: ccc-nset
CCCNSet(K) == (K ⊆r ℕ) ∧ K ∧ CCC(K)
Lemma: ccc-nset_wf
∀[K:Type]. (CCCNSet(K) ∈ ℙ')
Lemma: ccc-nset-minimum
∀K:Type. (CCCNSet(K) ⇒ (∃n:K. ∀m:K. (n ≤ m)))
Lemma: ccc-nset-remove1
∀K:Type. (CCCNSet(K) ⇒ (∀k0,k1:K. ((¬(k0 = k1 ∈ ℤ)) ⇒ CCCNSet({k:K| ¬(k = k0 ∈ ℤ)} ))))
Definition: weakly-decidable-nset
WD(K) == (K ⊆r ℕ) ∧ (∀m,k:K. ∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K))))
Lemma: weakly-decidable-nset_wf
∀[K:Type]. (WD(K) ∈ ℙ)
Lemma: ccc-nset-weakly-decidable
∀K:Type. (CCCNSet(K) ⇒ WD(K))
Definition: transparent-nset
Transparent(K) == (K ⊆r ℕ) ∧ (∀B:ℕ. ((∀k:K. (k ≤ B)) ∨ (∃k:K. B < k)))
Lemma: transparent-nset_wf
∀[K:Type]. (Transparent(K) ∈ ℙ)
Lemma: ccc-nset-transparent
∀K:Type. (CCCNSet(K) ⇒ Transparent(K))
Lemma: bounded-decidable-nset-finite
∀K:Type. ((K ⊆r ℕ) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))) ⇒ (∀B:ℕ. ((∀k:K. (k ≤ B)) ⇒ finite(K))))
Lemma: unbounded-decidable-nset-infinite
∀K:Type. ((K ⊆r ℕ) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))) ⇒ (∀B:ℕ. ∃k:K. B < k) ⇒ (∃f:K ⟶ ℕ. Surj(K;ℕ;f)))
Lemma: bounded-ccc-nset-decidable
∀K:Type. (CCCNSet(K) ⇒ (∀B:ℕ. ((∀k:K. (k ≤ B)) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))))))
Lemma: unbounded-ccc-nset-decidable
∀K:Type. (CCCNSet(K) ⇒ (∀B:ℕ. ∃k:K. B < k) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))))
Lemma: bounded-ccc-nset-finite
∀K:Type. (CCCNSet(K) ⇒ (∀B:ℕ. ((∀k:K. (k ≤ B)) ⇒ finite(K))))
Lemma: ccc-nset-not-not-finite
∀K:Type. (CCCNSet(K) ⇒ (¬¬finite(K)))
Lemma: CCC-omni
∀K:Type. (CCCNSet(K) ⇒ (∀P:K ⟶ ℙ. ((∀k:K. Dec(P[k])) ⇒ ((∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))))))
Lemma: CCC-omni-2
∀K:Type
(CCCNSet(K) ⇒ (∀P:K ⟶ K ⟶ ℙ. ((∀k,m:K. Dec(P[k;m])) ⇒ ((∃k:K. ∀m:K. P[k;m]) ∨ (∀k:K. (¬(∀m:K. P[k;m])))))))
Lemma: CCC-Sigma02-dns
∀K:Type. (CCCNSet(K) ⇒ (∀P:K ⟶ K ⟶ ℙ. ((∀k,m:K. Dec(P[k;m])) ⇒ (¬¬(∃k:K. ∀m:K. P[k;m])) ⇒ (∃k:K. ∀m:K. P[k;m]))))
Lemma: ccc-nset-iff-finite
∀K:Type. ((K ⊆r ℕ) ⇒ K ⇒ (CCC(K) ⇐⇒ finite(K)))
Definition: zero-seq
0s == λx.0
Lemma: zero-seq_wf
0s ∈ ℕ ⟶ ℕ
Definition: finite-nat-seq
finite-nat-seq() == n:ℕ × (ℕn ⟶ ℕ)
Lemma: finite-nat-seq_wf
finite-nat-seq() ∈ Type
Definition: mk-finite-nat-seq
f^(n) == <n, f>
Lemma: mk-finite-nat-seq_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. (f^(n) ∈ finite-nat-seq())
Definition: append-finite-nat-seq
f**g == let n,s = f in let m,r = g in λx.if (x) < (n) then s x else (r (x - n))^(n + m)
Lemma: append-finite-nat-seq_wf
∀[f,g:finite-nat-seq()]. (f**g ∈ finite-nat-seq())
Definition: neighbourhood-function-nat
K0(G) == (∀f:ℕ ⟶ ℕ. ∃n:ℕ. (↑isl(G f^(n)))) ∧ (∀f,g:finite-nat-seq(). ((↑isl(G f)) ⇒ ((G f) = (G f**g) ∈ (ℕ?))))
Lemma: neighbourhood-function-nat_wf
∀[G:finite-nat-seq() ⟶ (ℕ?)]. (K0(G) ∈ Type)
Definition: finite-nat-seq-to-list
finite-nat-seq-to-list(f) == let n,s = f in primrec(n;[];λi,r. (r @ [s i]))
Lemma: finite-nat-seq-to-list_wf
∀[f:finite-nat-seq()]. (finite-nat-seq-to-list(f) ∈ ℕ List)
Lemma: finite-nat-seq-to-list-prop1
∀[f:finite-nat-seq()]
((||finite-nat-seq-to-list(f)|| = (fst(f)) ∈ ℕ) ∧ (∀i:ℕfst(f). (finite-nat-seq-to-list(f)[i] = ((snd(f)) i) ∈ ℕ)))
Definition: ble
ble(n;m) == if n=m then tt else if (n) < (m) then tt else ff
Lemma: ble_wf
∀[n,m:ℤ]. (ble(n;m) ∈ 𝔹)
Lemma: assert-ble
∀[n:ℤ]. ∀[m:ℕ]. (↑ble(n;m) ⇐⇒ n ≤ m)
Definition: equal-upto-finite-nat-seq
equal-upto-finite-nat-seq(n;f;g) == primrec(n;tt;λi,b. (b ∧b (f i =z g i)))
Lemma: equal-upto-finite-nat-seq_wf
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℕ]. (equal-upto-finite-nat-seq(n;f;g) ∈ 𝔹)
Lemma: assert-equal-upto-finite-nat-seq
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℕ]. (↑equal-upto-finite-nat-seq(n;f;g) ⇐⇒ f = g ∈ (ℕn ⟶ ℕ))
Definition: init-seg-nat-seq
init-seg-nat-seq(f;g) == let n,s = f in let m,r = g in if ble(n;m) then equal-upto-finite-nat-seq(n;s;r) else ff fi
Lemma: init-seg-nat-seq_wf
∀[f,g:finite-nat-seq()]. (init-seg-nat-seq(f;g) ∈ 𝔹)
Lemma: append-empty-nat-seq
∀[f:finite-nat-seq()]. ∀[g:Top]. (f**g^(0) = f ∈ finite-nat-seq())
Lemma: assert-init-seg-nat-seq
∀f,g:finite-nat-seq(). (↑init-seg-nat-seq(f;g) ⇐⇒ ∃h:finite-nat-seq(). (g = f**h ∈ finite-nat-seq()))
Lemma: assert-init-seg-nat-seq2
∀f,g:finite-nat-seq(). (↑init-seg-nat-seq(f;g) ⇐⇒ ((fst(f)) ≤ (fst(g))) ∧ ((snd(f)) = (snd(g)) ∈ (ℕfst(f) ⟶ ℕ)))
Definition: phi-star
Phi* == λF.0s^(Phi F)
Lemma: phi-star_wf
∀[Phi:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ]. (Phi* ∈ ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ finite-nat-seq())
Lemma: append-finite-nat-seq-assoc
∀[f,g,h:finite-nat-seq()]. (f**g**h = f**g**h ∈ finite-nat-seq())
Lemma: extend-seq1-all-dec
∀n,n0:finite-nat-seq(). ∀beta:ℕ ⟶ ℕ.
Dec(∃x:ℕ. ((↑init-seg-nat-seq(n0**λi.x^(1);n)) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
Lemma: init-seg-nat-seq-append-implies-left
∀a,b,s:finite-nat-seq(). ((↑init-seg-nat-seq(a**b;s)) ⇒ (↑init-seg-nat-seq(a;s)))
Lemma: init-seg-nat-seq-append-implies-right
∀a,b,s:finite-nat-seq(). ((↑init-seg-nat-seq(s;a)) ⇒ (↑init-seg-nat-seq(s;a**b)))
Lemma: append-finite-nat-seq-1
∀n,a,b:finite-nat-seq(). ∀x:ℕ.
((↑init-seg-nat-seq(n**λi.x^(1);a**b)) ⇒ ((↑init-seg-nat-seq(a;n)) ∨ (↑init-seg-nat-seq(n**λi.x^(1);a))))
Lemma: dec-exists-int-seg
∀a,b:ℤ. ∀[F:{a..b-} ⟶ ℙ]. ((∀k:{a..b-}. Dec(F[k])) ⇒ Dec(∃k:{a..b-}. F[k]))
Definition: gamma-neighbourhood
gamma-neighbourhood(beta;n0) ==
λn.if init-seg-nat-seq(n;n0) then inr ⋅
if TERMOF{extend-seq1-all-dec:o, 1:l} n n0 beta then inl 1
else inl 0
fi
Lemma: gamma-neighbourhood_wf
∀[beta:ℕ ⟶ ℕ]. ∀[n0:finite-nat-seq()]. (gamma-neighbourhood(beta;n0) ∈ finite-nat-seq() ⟶ (ℕ?))
Lemma: gamma-neighbourhood-prop1
∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq().
((∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x))))
∧ (∀a,b:finite-nat-seq().
((↑isl(gamma-neighbourhood(beta;n0) a))
⇒ ((gamma-neighbourhood(beta;n0) a) = (gamma-neighbourhood(beta;n0) a**b) ∈ (ℕ?)))))
Lemma: gamma-neighbourhood-prop2
∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq(). ∀x:ℕ.
((¬((beta x) = 0 ∈ ℤ))
⇒ (∃x1:ℕx + 1
((¬((beta x1) = 0 ∈ ℤ))
∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))
∧ ((gamma-neighbourhood(beta;n0) n0**λx.x1^(1)) = (inl 1) ∈ (ℕ?))
∧ ((gamma-neighbourhood(beta;n0) n0**λx.(x1 + 1)^(1)) = (inl 0) ∈ (ℕ?)))))
Lemma: gamma-neighbourhood-prop3
∀beta:ℕ ⟶ ℕ. ∀n,m:ℕ.
(((beta 0) = 0 ∈ ℤ)
⇒ (↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m)))
⇒ (n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 0) ∈ (ℕ?))))
Definition: eq-seg-nat-seq
eq-seg-nat-seq(n;m) == init-seg-nat-seq(n;m) ∧b init-seg-nat-seq(m;n)
Lemma: eq-seg-nat-seq_wf
∀[n,m:finite-nat-seq()]. (eq-seg-nat-seq(n;m) ∈ 𝔹)
Lemma: assert-eq-seg-nat-seq
∀[n,m:finite-nat-seq()]. (↑eq-seg-nat-seq(n;m) ⇐⇒ n = m ∈ finite-nat-seq())
Definition: ext-finite-nat-seq
ext-finite-nat-seq(f;x) == let n,s = f in λk.if (k) < (n) then s k else x
Lemma: ext-finite-nat-seq_wf
∀[f:finite-nat-seq()]. ∀[x:ℕ]. (ext-finite-nat-seq(f;x) ∈ ℕ ⟶ ℕ)
Lemma: gamma-neighbourhood-prop4
∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq(). ∀x,n:ℕ.
((¬((beta x) = 0 ∈ ℤ))
⇒ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))
⇒ (↑isl(gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.x^(1);0)^(n)))
⇒ ((gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.x^(1);0)^(n)) = (inl 1) ∈ (ℕ?)))
Lemma: gamma-neighbourhood-prop5
∀beta:ℕ ⟶ ℕ. ∀n,m:ℕ.
((¬((beta 0) = 0 ∈ ℤ))
⇒ (↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m)))
⇒ (n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 1) ∈ (ℕ?))))
Lemma: gamma-neighbourhood-prop6
∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq(). ∀x,n:ℕ.
((¬((beta x) = 0 ∈ ℤ))
⇒ (↑isl(gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.(x + 1)^(1);0)^(n)))
⇒ ((gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.(x + 1)^(1);0)^(n)) = (inl 0) ∈ (ℕ?)))
Lemma: unsquashed-continuity-false-troelstra
¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ)))
Definition: spector-bar-rec
spector-bar-rec(Y;G;H;n;s)==r if Y n s ≤z n then G n s else H n s (λt.spector-bar-rec(Y;G;H;n + 1;s.t@n)) fi
Definition: decidable-bar-rec
decidable-bar-rec(dec;base;ind;n;s)
==r case dec n s of inl(r) => base n s r | inr(x) => ind n s (λt.decidable-bar-rec(dec;base;ind;n + 1;s.t@n))
Lemma: decidable-bar-rec_wf
∀[B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ]. ∀[bar:∀s:ℕ ⟶ ℕ. (↓∃n:ℕ. B[n;s])]. ∀[dec:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ∨ (¬B[n;s]))].
∀[base:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s])]. ∀[ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s])].
(decidable-bar-rec(dec;base;ind;0;seq-normalize(0;⊥)) ∈ Q[0;seq-normalize(0;⊥)])
Lemma: decidable-bar-rec_wf2
∀[B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ]. ∀[bar:∀s:ℕ ⟶ ℕ. (↓∃n:ℕ. B[n;s])]. ∀[dec:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ∨ (¬B[n;s]))].
∀[base:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s])]. ∀[ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s])]. ∀[n:ℕ].
∀[s:ℕn ⟶ ℕ].
(decidable-bar-rec(dec;base;ind;0;seq-normalize(0;⊥)) ∈ Q[0;seq-normalize(0;⊥)])
Lemma: decidable-bar-rec-equal-spector
∀[dec,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].
(decidable-bar-rec(dec;base;ind;n;s) ~ spector-bar-rec(λn,s. if dec n s then 0 else n + 1 fi ;λn,s. case dec n s
of inl(r) =>
base n s r
| inr(x) =>
⊥;ind;n;s))
Definition: howard-bar-rec
howard-bar-rec(M;mon;base;ind;n;s)
==r case M n s
of inl(x) =>
let k,p = x
in base n s (mon n k s p)
| inr(x) =>
ind n s (λt.howard-bar-rec(M;mon;base;ind;n + 1;s.t@n))
Lemma: howard-bar-rec_wf
∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ. ∀bar:∀s:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;s]). ∀mon:∀n:ℕ. ∀m:ℕn. ∀s:ℕn ⟶ ℕ. (B[m;s] ⇒ B[n;s]).
∀base:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]). ∀ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]).
⇃(Q[0;seq-normalize(0;⊥)])
Lemma: howard-bar-rec-equal-spector
∀[M,mon,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].
(howard-bar-rec(M;mon;base;ind;n;s) ~ spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
of inl(x) =>
let k,p = x
in base n s (mon n k s p)
| inr(x) =>
⊥;ind;n;s))
Lemma: howard-bar-rec-equal-decidable
∀[M,mon,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].
(howard-bar-rec(M;mon;base;ind;n;s) ~ decidable-bar-rec(M;λn,s,r. let k,p = r in base n s (mon n k s p);ind;n;s))
Lemma: gen-bar-rec
∀P:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. P[n + 1;s.m@n]) ⇒ P[n;s])) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. P[m;f])) ⇒ ⇃(P[0;λx.⊥]))
Lemma: gen-bar-ind-implies-monotone
(∀P:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
((∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. P[n + 1;s.m@n]) ⇒ P[n;s])) ⇒ (∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. P[m;f])) ⇒ ⇃(P[0;λx.⊥])))
⇒ (∀B,Q:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ. ∀bar:∀s:ℕ ⟶ ℕ. ⇃(∃n:ℕ. B[n;s]). ∀mon:∀n:ℕ. ∀m:ℕn. ∀s:ℕn ⟶ ℕ. (B[m;s] ⇒ B[n;s]).
∀base:∀n:ℕ. ∀s:ℕn ⟶ ℕ. (B[n;s] ⇒ Q[n;s]). ∀ind:∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. Q[n + 1;s.m@n]) ⇒ Q[n;s]).
⇃(Q[0;seq-normalize(0;⊥)]))
Definition: cons-nat-seq
cons-nat-seq(n;a) == λk.if k=0 then n else (a (k - 1))
Lemma: cons-nat-seq_wf
∀[n:ℕ]. ∀[a:ℕ ⟶ ℕ]. (cons-nat-seq(n;a) ∈ ℕ ⟶ ℕ)
Definition: shift-seq
shift-seq(c;a) == λn.(c cons-nat-seq(n;a))
Lemma: shift-seq_wf
∀[c:(ℕ ⟶ ℕ) ⟶ ℕ]. ∀[a:ℕ ⟶ ℕ]. (shift-seq(c;a) ∈ ℕ ⟶ ℕ)
Definition: squashed-continuity1-rel
squashed-continuity1-rel(A) ==
(∀a:ℕ ⟶ ℕ. ⇃(∃b:ℕ ⟶ ℕ. (A a b))) ⟶ ⇃(∃c:(ℕ ⟶ ℕ) ⟶ ℕ
((∀a:ℕ ⟶ ℕ
⇃(∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((c a) = (c b) ∈ ℕ))))
∧ (∀a:ℕ ⟶ ℕ. (A a shift-seq(c;a)))))
Lemma: squashed-continuity1-rel_wf
∀[A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ]. (squashed-continuity1-rel(A) ∈ ℙ)
Lemma: kripke's-schema-contradicts-squashed-continuity1-rel
(∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))) ⇒ (¬(∀A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ. squashed-continuity1-rel(A)))
Lemma: MP+KS-imply-LEM
(∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ (¬(∀n:ℕ. (¬P[n]))) ⇒ (∃n:ℕ. P[n])))
⇒ (∀A:ℙ. ∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))
⇒ (∀P:ℙ. (P ∨ (¬P)))
Lemma: MP+truncated-KS-imply-truncated-LEM
(∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ (¬(∀n:ℕ. (¬P[n]))) ⇒ (∃n:ℕ. P[n])))
⇒ (∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ))))
⇒ (∀P:ℙ. ⇃(P ∨ (¬P)))
Definition: increasing-sequence
increasing-sequence(a) == ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
Lemma: increasing-sequence_wf
∀[a:ℕ ⟶ ℕ]. (increasing-sequence(a) ∈ ℙ)
Lemma: increasing-sequence-prop1
∀a:ℕ ⟶ ℕ. (increasing-sequence(a) ⇒ (∀n,m:ℕ. ((n ≤ m) ⇒ ((a n) ≤ (a m)))))
Definition: min-increasing-sequence
min-increasing-sequence(a;n;k) ==
primrec(n;inr ⋅ ;λi,r. case r of inl(x) => inl x | inr(x) => if k ≤z a i then inl i else inr ⋅ fi )
Lemma: min-increasing-sequence_wf
∀[a:ℕ ⟶ ℕ]. ∀[n,k:ℕ]. (min-increasing-sequence(a;n;k) ∈ ℕ?)
Lemma: min-increasing-sequence-prop1
∀b:ℕ ⟶ ℕ. ∀n,x,k:ℕ. ((min-increasing-sequence(b;n;x) = (inl k) ∈ (ℕ?)) ⇒ (x ≤ (b k)))
Lemma: min-increasing-sequence-prop2
∀b,a:ℕ ⟶ ℕ. ∀n,x,k:ℕ.
((b = a ∈ (ℕx ⟶ ℕ))
⇒ increasing-sequence(a)
⇒ (min-increasing-sequence(b;n;(a x) + 1) = (inl k) ∈ (ℕ?))
⇒ (x ≤ k))
Definition: min-inc-seq
min-inc-seq(a;n;k) == case min-increasing-sequence(a;n;k) of inl(x) => x | inr(x) => n
Lemma: min-inc-seq_wf
∀[a:ℕ ⟶ ℕ]. ∀[n,k:ℕ]. (min-inc-seq(a;n;k) ∈ ℕ)
Definition: eq-finite-seqs
eq-finite-seqs(a;b;x) == primrec(x;tt;λi,r. (r ∧b (a i =z b i)))
Lemma: eq-finite-seqs_wf
∀[a,b:ℕ ⟶ ℕ]. ∀[x:ℕ]. (eq-finite-seqs(a;b;x) ∈ 𝔹)
Lemma: eq-finite-seqs-implies-eq-upto
∀a,b:ℕ ⟶ ℕ. ∀x:ℕ. ((↑eq-finite-seqs(a;b;x)) ⇒ (a = b ∈ (ℕx ⟶ ℕ)))
Lemma: eq-finite-seqs-iff-eq-upto
∀a,b:ℕ ⟶ ℕ. ∀x:ℕ. (↑eq-finite-seqs(a;b;x) ⇐⇒ a = b ∈ (ℕx ⟶ ℕ))
Definition: kripke2b-seq
kripke2b-seq(a;x;F) == λb.if eq-finite-seqs(a;b;x) then min-inc-seq(b;fst((F b));(a x) + 1) else 0 fi
Lemma: kripke2b-seq_wf
∀[a:ℕ ⟶ ℕ]. ∀[x:ℕ]. ∀[F:∀b:{b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} . ∃n:ℕ. ((b n) ≥ ((a x) + 1) )].
(kripke2b-seq(a;x;F) ∈ (ℕ ⟶ ℕ) ⟶ ℕ)
Definition: nat-pred
n-1 == if n=0 then 0 else (n - 1)
Lemma: nat-pred_wf
∀[n:ℕ]. (n-1 ∈ ℕ)
Definition: baire2cantor
baire2cantor(a) == λn.if (a n =z a n-1) then ff else tt fi
Lemma: baire2cantor_wf
∀[a:ℕ ⟶ ℕ]. (baire2cantor(a) ∈ ℕ ⟶ 𝔹)
Definition: cantor2baire-aux
cantor2baire-aux(a;n) == primrec(n;0;λm,r. if a (m + 1) then r + 1 else r fi )
Lemma: cantor2baire-aux_wf
∀[a:ℕ ⟶ 𝔹]. ∀[n:ℕ]. (cantor2baire-aux(a;n) ∈ ℕ)
Lemma: cantor2baire-aux+1
∀[a:ℕ ⟶ 𝔹]. ∀[n:ℕ].
(cantor2baire-aux(a;n + 1) ~ if a (n + 1) then cantor2baire-aux(a;n) + 1 else cantor2baire-aux(a;n) fi )
Lemma: nat-pred-as-sub
∀n:ℕ. (0 < n ⇒ (n-1 = (n - 1) ∈ ℕ))
Lemma: cantor2baire-aux-pos
∀[a:ℕ ⟶ 𝔹]. ∀[n:ℕ].
cantor2baire-aux(a;n) ~ if a n then cantor2baire-aux(a;n-1) + 1 else cantor2baire-aux(a;n-1) fi supposing 0 < n
Definition: cantor2baire
cantor2baire(a) == λn.cantor2baire-aux(a;n)
Lemma: cantor2baire_wf
∀[a:ℕ ⟶ 𝔹]. (cantor2baire(a) ∈ ℕ ⟶ ℕ)
Lemma: cantor2baire-is-increasing
∀a:ℕ ⟶ 𝔹. increasing-sequence(cantor2baire(a))
Definition: initF
initF(a) == a 0 = ff
Lemma: initF_wf
∀[a:ℕ ⟶ 𝔹]. (initF(a) ∈ ℙ)
Definition: init0
init0(a) == (a 0) = 0 ∈ ℕ
Lemma: init0_wf
∀[a:ℕ ⟶ ℕ]. (init0(a) ∈ ℙ)
Lemma: init0-cantor2baire
∀a:ℕ ⟶ 𝔹. init0(cantor2baire(a))
Lemma: cantor2baire2cantor
∀a:ℕ ⟶ 𝔹. (initF(a) ⇒ (baire2cantor(cantor2baire(a)) = a ∈ (ℕ ⟶ 𝔹)))
Lemma: baire2cantor2baire
∀a:ℕ ⟶ ℕ. (init0(a) ⇒ increasing-sequence(a) ⇒ (cantor2baire(baire2cantor(a)) = a ∈ (ℕ ⟶ ℕ)))
Definition: kripke2b-baire-seq
kripke2b-baire-seq(a;x;F) ==
λb.if eq-finite-seqs(a;cantor2baire(b);x)
then min-inc-seq(cantor2baire(b);fst((F cantor2baire(b)));(a x) + 1)
else 0
fi
Lemma: kripke2b-baire-seq_wf
∀[a:ℕ ⟶ ℕ]. ∀[x:ℕ]. ∀[F:∀b:{b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} . ∃n:ℕ. ((b n) ≥ ((a x) + 1) )].
(kripke2b-baire-seq(a;x;F) ∈ (ℕ ⟶ 𝔹) ⟶ ℕ)
Lemma: init0-implies-eq-upto1-zero-seq
∀a:ℕ ⟶ ℕ. (init0(a) ⇒ (a = 0s ∈ (ℕ1 ⟶ ℕ)))
Lemma: init0-zero-seq
init0(0s)
Lemma: increasing-zero-seq
increasing-sequence(0s)
Definition: change-from1
change-from1(a) == λn.if n=0 then ff else if a 1=a 0 then tt else ff
Lemma: change-from1_wf
∀[a:ℕ ⟶ ℕ]. (change-from1(a) ∈ ℕ ⟶ 𝔹)
Definition: baire-diff-from
baire-diff-from(a;k) == λn.if k ≤z n then if a k=a k-1 then (a k-1) + 1 else (a k-1) else a n fi
Lemma: baire-diff-from_wf
∀[a:ℕ ⟶ ℕ]. ∀[k:ℕ]. (baire-diff-from(a;k) ∈ ℕ ⟶ ℕ)
Lemma: eq-upto-baire-diff-from
∀[a:ℕ ⟶ ℕ]. ∀[n:ℕ]. (a = baire-diff-from(a;n) ∈ (ℕn ⟶ ℕ))
Lemma: init0-baire-diff-from
∀a:ℕ ⟶ ℕ. ∀n:ℕ. (0 < n ⇒ init0(a) ⇒ init0(baire-diff-from(a;n)))
Lemma: increasing-baire-diff-from
∀a:ℕ ⟶ ℕ. ∀n:ℕ. (increasing-sequence(a) ⇒ increasing-sequence(baire-diff-from(a;n)))
Lemma: implies-eq-upto-baire2cantor
∀a,b:ℕ ⟶ ℕ. ∀n:ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ (baire2cantor(a) = baire2cantor(b) ∈ (ℕn ⟶ 𝔹)))
Lemma: baire-diff-from-diff
∀a:ℕ ⟶ ℕ. ∀n:ℕ. (¬((a n) = (baire-diff-from(a;n) n) ∈ ℕ))
Definition: baire_eq_from
baire_eq_from(a;k) == λn.if n <z k then a n else a k fi
Lemma: baire_eq_from_wf
∀[a:ℕ ⟶ ℕ]. ∀[k:ℕ]. (baire_eq_from(a;k) ∈ ℕ ⟶ ℕ)
Lemma: increasing-baire-eq-from
∀a:ℕ ⟶ ℕ. ∀k:ℕ. (increasing-sequence(a) ⇒ increasing-sequence(baire_eq_from(a;k)))
Lemma: eq-upto-baire-eq-from
∀a:ℕ ⟶ ℕ. ∀p,n:ℕ. ((p ≤ n) ⇒ (a = baire_eq_from(a;n) ∈ (ℕp ⟶ ℕ)))
Lemma: init0-baire-eq-from
∀a:ℕ ⟶ ℕ. ∀n:ℕ. (init0(a) ⇒ init0(baire_eq_from(a;n)))
Definition: is-absolutely-free
is-absolutely-free{i:l}(f) == ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
Lemma: is-absolutely-free_wf
∀[a:ℕ ⟶ ℕ]. (is-absolutely-free{i:l}(a) ∈ ℙ')
Lemma: old-Kripke2a
(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
⇒ (∀a:{a:ℕ ⟶ ℕ| increasing-sequence(a)} . ∀m:ℕ. (¬¬(∃n:ℕ. ((a n) ≥ m ))))
Lemma: Kripke2a
∀a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ⇒ increasing-sequence(a) ⇒ (∀m:ℕ. (¬¬(∃n:ℕ. ((a n) ≥ m )))))
Lemma: Kripke2b
∀a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ⇒ init0(a) ⇒ increasing-sequence(a) ⇒ (¬(∀m:ℕ. ∃n:ℕ. ((a n) ≥ m ))))
Lemma: gen-continuity-contradicts-kuroda
(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀m:ℕ. (¬¬(A m))) ⇒ (¬¬(∀m:ℕ. (A m))))))
Lemma: afcs-contradicts-kuroda
(↓∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a)))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀m:ℕ. (¬¬(A m))) ⇒ (¬¬(∀m:ℕ. (A m))))))
Lemma: gen-continuity-contradicts-markov
(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n)))) ⇒ (¬¬(∃n:ℕ. (A n))) ⇒ (∃n:ℕ. (A n)))))
Lemma: gen-continuity-is-false
¬(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
Lemma: afcs-contradicts-markov
(↓∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a)))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n)))) ⇒ (¬¬(∃n:ℕ. (A n))) ⇒ (∃n:ℕ. (A n)))))
Definition: absolutelyfree
absolutelyfree{i:l}(T) ==
((T ⊆r (ℕ ⟶ ℕ)) ∧ (∀P:T ⟶ ℙ. ∀f:T. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:T. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))))
∧ (∀S:Type
((S ⊆r (ℕ ⟶ ℕ)) ⇒ (∀P:S ⟶ ℙ. ∀f:S. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:S. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))) ⇒ (S ⊆r T)))
Lemma: absolutelyfree_wf
∀[T:Type]. (absolutelyfree{i:l}(T) ∈ ℙ')
Lemma: absolutelyfree-subtype
∀[T:Type]. T ⊆r (ℕ ⟶ ℕ) supposing absolutelyfree{i:l}(T)
Lemma: absolutelyfree-unique
∀[T,S:Type]. (absolutelyfree{i:l}(T) ⇒ absolutelyfree{i:l}(S) ⇒ T ≡ S)
Definition: type2tree
type2tree(A;B;C) == W(C + A;d.case d of inl(n) => Void | inr(m) => B)
Lemma: type2tree_wf
∀[A,B,C:Type]. (type2tree(A;B;C) ∈ Type)
Definition: tree2fun
tree2fun(eq;w;g) ==
let d,f = w
in case d of inl(n) => n | inr(m) => eval x = g m in tree2fun(eq;f x;λi.if eq i m then x else g i fi )
Lemma: tree2fun_wf
∀[A,B,C:Type]. ∀[eq:EqDecider(A)]. ∀[w:type2tree(A;B;C)]. ∀[g:A ⟶ B]. (tree2fun(eq;w;g) ∈ C) supposing value-type(B)
Definition: fun2tree
fun2tree(M;p)
==r let n,br = p
in case M n br
of inl(x) =>
Wsup(inl x;λi.i)
| inr(_) =>
Wsup(inr n ;λi.fun2tree(M;<n + 1, λx.if (x =z n) then i else br x fi >))
Home
Index