---

Step * of Lemma unsquashed-continuity-false-troelstra

¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ)))
BY
{ ((D 0 THENA Auto)
   THEN (Assert ⌜∀a:ℕ ⟶ ℕ. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))⌝⋅
         THENA ((UnivCD THENA Auto) THEN BHyp (-3) THEN Auto)
         )
   THEN (InstHyp [⌜0s⌝] (-1)⋅ THENA Auto)
   THEN (Skolemize (-1) `Phi' THENA Auto)) }

1
1. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a:ℕ ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
2. ∀a:ℕ ⟶ ℕ. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ.  ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
3. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((0s = b ∈ (ℕn ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
4. Phi : F:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℕ
5. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀b:ℕ ⟶ ℕ.  ((0s = b ∈ (ℕPhi F ⟶ ℕ)) ⇒ ((F 0s) = (F b) ∈ ℕ))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  b)  {}\mRightarrow{}  ((F  a)  =  (F  b))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.    \mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  b)  {}\mRightarrow{}  ((F  a)  =  (F  b)))\mkleeneclose{}\mcdot{}
              THENA  ((UnivCD  THENA  Auto)  THEN  BHyp  (-3)  THEN  Auto)
              )
  THEN  (InstHyp  [\mkleeneopen{}0s\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (Skolemize  (-1)  `Phi'  THENA  Auto))

---

Home Index