---

Step * 1 1 of Lemma not-LPO


1. ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))
2. ∀f:ℕ ⟶ ℕ. ∃k:ℕ. (0 < k ⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
3. F : f:(ℕ ⟶ ℕ) ⟶ ℕ
4. ∀f:ℕ ⟶ ℕ. (0 < F f ⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
5. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F (λn.0)) = (F g) ∈ ℕ)))
6. n : ℕ
7. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F (λn.0)) = (F g) ∈ ℕ))
⊢ False
BY
{ ((InstHyp [⌜λn.0⌝] 4⋅ THENA Auto) THEN (RepeatFor 2 (D -1) THENA (Reduce 0 THEN Auto))) }

1
1. ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))
2. ∀f:ℕ ⟶ ℕ. ∃k:ℕ. (0 < k ⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
3. F : f:(ℕ ⟶ ℕ) ⟶ ℕ
4. ∀f:ℕ ⟶ ℕ. (0 < F f ⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
5. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F (λn.0)) = (F g) ∈ ℕ)))
6. n : ℕ
7. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F (λn.0)) = (F g) ∈ ℕ))
8. 0 < F (λn.0) ⇒ (∀n:ℕ. (((λn.0) n) = 0 ∈ ℤ))
9. 0 < F (λn.0)
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}n:\mBbbN{}.  ((f  n)  =  0))  \mvee{}  (\mneg{}(\mforall{}n:\mBbbN{}.  ((f  n)  =  0))))
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}k:\mBbbN{}.  (0  <  k  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  ((f  n)  =  0))
3.  F  :  f:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (0  <  F  f  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  ((f  n)  =  0))
5.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (((\mlambda{}n.0)  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.0))  =  (F  g))))
6.  n  :  \mBbbN{}
7.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (((\mlambda{}n.0)  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.0))  =  (F  g)))
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}n.0\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  (RepeatFor  2  (D  -1)  THENA  (Reduce  0  THEN  Auto)))

---

Home Index