---

Step * of Lemma no-uniform-double-negation-elim

¬(∀[P:ℙ]. ((¬¬P) ⇒ P))
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `double-negation-iff-xmiddle` [⌜False⌝]⋅ THENA Auto)
   THEN Fold `not` (-1)
   THEN (D -1 THEN Thin (-1))
   THEN D -1) }

1
.....antecedent..... 
1. ∀[P:ℙ]. ((¬¬P) ⇒ P)@i'
⊢ ∀[P:ℙ]. ((¬¬P) ⇒ (P ∨ False))

2
1. ∀[P:ℙ]. ((¬¬P) ⇒ P)@i'
2. ∀[P:ℙ]. (P ∨ (¬P))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}[P:\mBbbP{}].  ((\mneg{}\mneg{}P)  {}\mRightarrow{}  P))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `double-negation-iff-xmiddle`  [\mkleeneopen{}False\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `not`  (-1)
  THEN  (D  -1  THEN  Thin  (-1))
  THEN  D  -1)

---

Home Index