---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
UseWitness  \mkleeneopen{}\mlambda{}n.isl(magic  (n)\mdownarrow{})\mkleeneclose{}\mcdot{}

---

Home Index