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