---

Step * of Lemma Escardo-Xu

¬(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ)))
BY
{ (D 0 THEN Auto) }

1
1. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}i:\mBbbN{}k.  ((g  i)  =  0))  {}\mRightarrow{}  ((F  (\mlambda{}i.0))  =  (F  g))))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index