---

Step * of Lemma not-LPO

¬(∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ)))))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∀f:ℕ ⟶ ℕ. ∃k:ℕ. (0 < k ⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ)) BY
               (ParallelLast THEN (D -1 THENL [D 0 With ⌜1⌝ ; D 0 With ⌜0⌝ ]) THEN Auto))
   THEN (Skolemize (-1) `F' THENA 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 ∈ ℤ))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}n:\mBbbN{}.  ((f  n)  =  0))  \mvee{}  (\mneg{}(\mforall{}n:\mBbbN{}.  ((f  n)  =  0)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}k:\mBbbN{}.  (0  <  k  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  ((f  n)  =  0))  BY
                          (ParallelLast  THEN  (D  -1  THENL  [D  0  With  \mkleeneopen{}1\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}0\mkleeneclose{}  ])  THEN  Auto))
  THEN  (Skolemize  (-1)  `F'  THENA  Auto))

---

Home Index