---

Step * of Lemma afcs-contradicts-kuroda

(↓∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a)))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀m:ℕ. (¬¬(A m))) ⇒ (¬¬(∀m:ℕ. (A m))))))
BY
{ ((D 0 THENA At ℙ' Auto⋅) THEN (UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN Unsquash) }

1
1. ∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a))
2. ∀A:ℕ ⟶ ℙ. ((∀m:ℕ. (¬¬(A m))) ⇒ (¬¬(∀m:ℕ. (A m))))
⊢ False

---

Latex:

---

Latex:
(\mdownarrow{}\mexists{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (is-absolutely-free\{i:l\}(a)  \mwedge{}  init0(a)  \mwedge{}  increasing-sequence(a)))
{}\mRightarrow{}  (\mneg{}(\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}m:\mBbbN{}.  (\mneg{}\mneg{}(A  m)))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mforall{}m:\mBbbN{}.  (A  m))))))


By

---

Latex:
((D  0  THENA  At  \mBbbP{}'  Auto\mcdot{})  THEN  (UnivCD  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  Unsquash)

---

Home Index