---

Step * 1 of Lemma no-excluded-middle-using-partial


1. ∀P:ℙ. (P ∨ (¬P))
⊢ False
BY
{ Assert ⌜n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} ⌝⋅ }

1
.....assertion..... 
1. ∀P:ℙ. (P ∨ (¬P))
⊢ n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 

2
1. ∀P:ℙ. (P ∨ (¬P))
2. n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}n:partial(\mBbbZ{})  {}\mrightarrow{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  (n)\mdownarrow{}\}  \mkleeneclose{}\mcdot{}

---

Home Index