---

Step * 1 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)))
4. magic : ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓))
⊢ False
BY
{ (D -2 THEN UseWitness ⌜magic⌝⋅) }

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

---

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)))
4.  magic  :  \mforall{}t:Base.  \00D9((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))
\mvdash{}  False


By

---

Latex:
(D  -2  THEN  UseWitness  \mkleeneopen{}magic\mkleeneclose{}\mcdot{})

---

Home Index