---

Step * 1 1 of Lemma not-choice-baire-to-nat


1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P[t]) ⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
2. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
3. ⇃(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
⊢ False
BY
{ Assert ⌜⇃(False)⌝⋅ }

1
.....assertion..... 
1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P[t]) ⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
2. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
3. ⇃(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
⊢ ⇃(False)

2
1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P[t]) ⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
2. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((t f) = (t g) ∈ ℕ)))
3. ⇃(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
4. ⇃(False)
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  (\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(P[t])  \mLeftarrow{}{}\mRightarrow{}  \00D9(\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t]))
2.  \mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((t  f)  =  (t  g))))
\mLeftarrow{}{}\mRightarrow{}  \00D9(\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((t  f)  =  (t  g))))
3.  \00D9(\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}\00D9(False)\mkleeneclose{}\mcdot{}

---

Home Index