---

Step * 1 of Lemma Escardo-Xu


1. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))
⊢ False
BY
{ ((Skolemize 1 `M' THENA Auto) THEN Thin 1) }

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

---

Latex:

---

Latex:

1.  \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)))
\mvdash{}  False


By

---

Latex:
((Skolemize  1  `M'  THENA  Auto)  THEN  Thin  1)

---

Home Index