---

Step * of Lemma Troelstra-lemma

¬(∀g:ℕ ⟶ ℕ. ∃n:ℕ. ∀f:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ (∀x:ℕ. ((g x) = 0 ∈ ℕ)) ⇒ (∀x:ℕ. ((f x) = 0 ∈ ℕ))))
BY
{ ((D 0 THENA Auto) THEN (InstHyp [⌜λx.0⌝] (-1)⋅ THENA Auto) THEN ExRepD THEN Thin (1)) }

1
1. n : ℕ
2. ∀f:ℕ ⟶ ℕ. ((f = (λx.0) ∈ (ℕn ⟶ ℕ)) ⇒ (∀x:ℕ. (((λx.0) x) = 0 ∈ ℕ)) ⇒ (∀x:ℕ. ((f x) = 0 ∈ ℕ)))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}.  ((g  x)  =  0))  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}.  ((f  x)  =  0))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}x.0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  Thin  (1))

---

Home Index