---

Step * of Lemma no-excluded-middle-quot-true1

¬(∀P:ℙ. ⇃(P ∨ (¬P)))
BY
{ ((D 0 THENA Auto)
   THEN (Assert EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.∀x:Base. (↓True)) BY
               (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN ((InstLemma not-has-value-decidable-quot [⌜λ2f g.∀x:Base. (↓True)⌝]⋅ THENA Complete (Auto)) THENA Auto)) }

1
1. ∀P:ℙ. ⇃(P ∨ (¬P))
2. EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.∀x:Base. (↓True))
3. ¬(f,g:∀x:Base. ((x)↓ ∨ (¬(x)↓))//(∀x:Base. (↓True)))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mneg{}P)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.\mforall{}x:Base.  (\mdownarrow{}True))  BY
                          (RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  ((InstLemma  not-has-value-decidable-quot  [\mkleeneopen{}\mlambda{}\msubtwo{}f  g.\mforall{}x:Base.  (\mdownarrow{}True)\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto))
              THENA  Auto
              ))

---

Home Index