---

Step * of Lemma afcs-contradicts-markov

(↓∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a)))
⇒ (¬(∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n)))) ⇒ (¬¬(∃n:ℕ. (A n))) ⇒ (∃n:ℕ. (A n)))))
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:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n)))) ⇒ (¬¬(∃n:ℕ. (A n))) ⇒ (∃n:ℕ. (A n)))
⊢ 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{}n:\mBbbN{}.  ((A  n)  \mvee{}  (\mneg{}(A  n))))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (A  n)))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (A  n)))))


By

---

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

---

Home Index