---

Step * 1 1 1 of Lemma DNS-iff-not-not-GMP


1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
3. ¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))@i
⊢ False
BY
{ Assert ⌜¬(∃n:ℕ. (¬A[n]))⌝⋅ }

1
.....assertion..... 
1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
3. ¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))@i
⊢ ¬(∃n:ℕ. (¬A[n]))

2
1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
3. ¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))@i
4. ¬(∃n:ℕ. (¬A[n]))
⊢ False

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  (\mforall{}i:\mBbbN{}.  (\mneg{}\mneg{}A[i]))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mforall{}i:\mBbbN{}.  A[i]))@i
3.  \mneg{}((\mneg{}(\mforall{}i:\mBbbN{}.  A[i]))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (\mneg{}A[n])))@i
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}A[n]))\mkleeneclose{}\mcdot{}

---

Home Index