---

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


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

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

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
2.  n:partial(\mBbbZ{})  {}\mrightarrow{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  (n)\mdownarrow{}\} 
\mvdash{}  False


By

---

Latex:
RenameVar  `h'  (-1)

---

Home Index