---

Step * 1 1 1 2 of Lemma not-decidable-zero-sequence


1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
2. n : ℕ
3. y : ¬((λx.0) = (λx.0) ∈ (ℕ ⟶ ℕ))
4. (G (λx.0)) = (inr y ) ∈ (((λx.0) = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬((λx.0) = (λx.0) ∈ (ℕ ⟶ ℕ))))
⊢ (∀g:ℕ ⟶ ℕ
     (((λx.0) = g ∈ (ℕn ⟶ ℕ))
     ⇒ (case inr y  of inl(x) => 0 | inr(x) => 1 = case G g of inl(x) => 0 | inr(x) => 1 ∈ ℕ)))
⇒ False
BY
{ (D (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((s  =  (\mlambda{}x.0))  \mvee{}  (\mneg{}(s  =  (\mlambda{}x.0))))
2.  n  :  \mBbbN{}
3.  y  :  \mneg{}((\mlambda{}x.0)  =  (\mlambda{}x.0))
4.  (G  (\mlambda{}x.0))  =  (inr  y  )
\mvdash{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          (((\mlambda{}x.0)  =  g)
          {}\mRightarrow{}  (case  inr  y    of  inl(x)  =>  0  |  inr(x)  =>  1  =  case  G  g  of  inl(x)  =>  0  |  inr(x)  =>  1)))
{}\mRightarrow{}  False


By

---

Latex:
(D  (-2)  THEN  Auto)

---

Home Index