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