---

Step * 1 1 1 of Lemma no-weak-limited-omniscience


1. n : ℕ
2. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. ff = g i) ⇒ (∀n:ℕ. ff = ff ⇐⇒ ∀n:ℕ. g n = ff))
⊢ False
BY
{ (InstHyp [⌜λi.n <z i⌝] (-1)⋅ THENA (Auto THEN Reduce 0 THEN Auto)) }

1
1. n : ℕ
2. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. ff = g i) ⇒ (∀n:ℕ. ff = ff ⇐⇒ ∀n:ℕ. g n = ff))
3. ∀n:ℕ. ff = ff ⇐⇒ ∀n@0:ℕ. (λi.n <z i) n@0 = ff
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}i:\mBbbN{}n.  ff  =  g  i)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  ff  =  ff  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  g  n  =  ff))
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}i.n  <z  i\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  Reduce  0  THEN  Auto))

---

Home Index