---

Step * of Lemma gen-continuity-is-false

¬(∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ.  ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g)))))
BY
{ ((D 0 THENA Auto)
   THEN (InstHyp [⌜λf.∀n:ℕ. ∃m:{n...}. ((f m) = 0 ∈ ℤ)⌝;⌜0s⌝] 1⋅
         THENA (Auto THEN Reduce 0 THEN Auto THEN D 0 With ⌜n⌝  THEN Auto)
         )
   ) }

1
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ.  ((P f) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
2. ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((0s = g ∈ (ℕk ⟶ ℕ)) ⇒ ((λf.∀n:ℕ. ∃m:{n...}. ((f m) = 0 ∈ ℤ)) g)))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((P  f)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  (P  g)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}f.\mforall{}n:\mBbbN{}.  \mexists{}m:\{n...\}.  ((f  m)  =  0)\mkleeneclose{};\mkleeneopen{}0s\mkleeneclose{}]  1\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  Auto  THEN  D  0  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto)
              )
  )

---

Home Index