---

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

.....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) ∈ ℕ)))
⊢ (∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))) ⇒ False
BY
{ (Thin (-1)
   THEN (D 0 THENA Auto)
   THEN (Assert ⌜¬unsquashed-WCP⌝⋅ THENA Auto)
   THEN D (-1)
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌜F⌝] (-2)⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜M⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}  (\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))))  {}\mRightarrow{}  False


By

---

Latex:
(Thin  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mneg{}unsquashed-WCP\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}F\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}M\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index