Step
*
1
of Lemma
monotone-bar-induction8
1. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
2. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n]))
⇒ ⇃(Q[n;s]))
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. ⇃(Q[m;f]))
4. ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f])) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
⊢ ⇃(⇃(Q[0;λx.⊥]))
BY
{ Assert ⌜(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f]))
∧ ((M n f) = (inl k) ∈ (ℕ?))
∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
⇒ ⇃(Q[0;λx.⊥])⌝⋅ }
1
.....assertion.....
1. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
2. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n]))
⇒ ⇃(Q[n;s]))
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. ⇃(Q[m;f]))
4. ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f])) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
⊢ (∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f])) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
⇒ ⇃(Q[0;λx.⊥])
2
1. Q : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ ℙ
2. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ((∀m:ℕ. ⇃(Q[n + 1;s.m@n]))
⇒ ⇃(Q[n;s]))
3. bar : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀m:{n...}. ⇃(Q[m;f]))
4. ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f])) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
5. (∃M:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
∀f:ℕ ⟶ ℕ
∃n:ℕ
∃k:ℕn
((∀m:{k...}. ⇃(Q[m;f])) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f))
⇒ ((M m f) = (inl k) ∈ (ℕ?))))))
⇒ ⇃(Q[0;λx.⊥])
⊢ ⇃(⇃(Q[0;λx.⊥]))
Latex:
Latex:
1. Q : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}
2. \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. ((\mforall{}m:\mBbbN{}. \00D9(Q[n + 1;s.m@n])) {}\mRightarrow{} \00D9(Q[n;s]))
3. bar : \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. \00D9(Q[m;f]))
4. \00D9(\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} (\mBbbN{}n?)
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\mexists{}n:\mBbbN{}
\mexists{}k:\mBbbN{}n
((\mforall{}m:\{k...\}. \00D9(Q[m;f]))
\mwedge{} ((M n f) = (inl k))
\mwedge{} (\mforall{}m:\mBbbN{}. ((\muparrow{}isl(M m f)) {}\mRightarrow{} ((M m f) = (inl k))))))
\mvdash{} \00D9(\00D9(Q[0;\mlambda{}x.\mbot{}]))
By
Latex:
Assert \mkleeneopen{}(\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} (\mBbbN{}n?)
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\mexists{}n:\mBbbN{}
\mexists{}k:\mBbbN{}n
((\mforall{}m:\{k...\}. \00D9(Q[m;f]))
\mwedge{} ((M n f) = (inl k))
\mwedge{} (\mforall{}m:\mBbbN{}. ((\muparrow{}isl(M m f)) {}\mRightarrow{} ((M m f) = (inl k))))))
{}\mRightarrow{} \00D9(Q[0;\mlambda{}x.\mbot{}])\mkleeneclose{}\mcdot{}
Home
Index