---

Step * 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 ∈ ℤ))
⊢ False
BY
{ ((InstLemma `weak-continuity-nat-nat` [⌜F⌝;⌜λn.0⌝]⋅ THENA Auto)
   THEN (FLemma `squash-from-quotient` [-1] THENA Auto)
   THEN RepeatFor 2 (D -1)) }

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) ∈ ℕ))
⊢ 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))
\mvdash{}  False


By

---

Latex:
((InstLemma  `weak-continuity-nat-nat`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}\mlambda{}n.0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FLemma  `squash-from-quotient`  [-1]  THENA  Auto)
  THEN  RepeatFor  2  (D  -1))

---

Home Index