---

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

¬ChoicePrinciple((ℕ ⟶ ℕ) ⟶ ℕ)
BY
{ ((D 0 THENA Auto)
   THEN Unfold `choice-principle` (-1)
   THEN (InstHyp [⌜λ2F.∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))⌝] (-1)⋅
         THENA Auto
         )) }

1
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) ∈ ℕ)))
⊢ False

---

Latex:

---

Latex:
\mneg{}ChoicePrinciple((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `choice-principle`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}F.\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))\mkleeneclose{}]  (-1)\mcdot{}
              THENA  Auto
              ))

---

Home Index