---

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

¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t]) ⇐⇒ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
BY
{ ((D 0 THENA Auto)
   THEN (InstHyp [⌜λ2F.∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))⌝] (-1)⋅
         THENA Auto
         )
   THEN InstLemma `strong-continuity2-implies-weak-skolem` []
   THEN (Assert ⌜∀F:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))⌝⋅
         THENA ((D 0 THENA Auto)
                THEN (InstHyp [⌜F⌝] (-2)⋅ THENA Auto)
                THEN MoveToConcl (-1)
                THEN BLemma `quotient-implies-squash`
                THEN Auto)
         )
   THEN Thin (-2)) }

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) ∈ ℕ))
3. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  (\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}P[t])  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t]))


By

---

Latex:
((D  0  THENA  Auto)
  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
              )
  THEN  InstLemma  `strong-continuity2-implies-weak-skolem`  []
  THEN  (Assert  \mkleeneopen{}\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))\mkleeneclose{}\mcdot{}
              THENA  ((D  0  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}F\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  BLemma  `quotient-implies-squash`
                            THEN  Auto)
              )
  THEN  Thin  (-2))

---

Home Index