---

Step * 1 1 1 of Lemma not-d-CCC-nat


1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
3. ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ)))
⊢ False
BY
{ (InstLemma `not-LPO` [] THEN D -1) }

1
1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
3. ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ)))
⊢ ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))

---

Latex:

---

Latex:

1.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  (g  n))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  (\muparrow{}(R  n  m))))
2.  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  ((\mexists{}l:\mBbbN{}n.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}m.  ((h  l)  =  0)))
3.  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mexists{}l:\mBbbN{}.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}.  ((h  l)  =  0)))
\mvdash{}  False


By

---

Latex:
(InstLemma  `not-LPO`  []  THEN  D  -1)

---

Home Index