---

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


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
BY
{ ((Assert ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓)) BY Auto) THEN RenameVar `magic' (-1)) }

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)))
4. magic : ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓))
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mneg{}P))
2.  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.\mforall{}x:Base.  (\mdownarrow{}True))
3.  \mneg{}(f,g:\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))//(\mforall{}x:Base.  (\mdownarrow{}True)))
\mvdash{}  False


By

---

Latex:
((Assert  \mforall{}t:Base.  \00D9((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))  BY  Auto)  THEN  RenameVar  `magic'  (-1))

---

Home Index