---

Step * 1 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))
3. ∀n:ℕ. ff = ff ⇐⇒ ∀n@0:ℕ. (λi.n <z i) n@0 = ff
⊢ False
BY
{ (D -1 THEN (D -2 THENA Auto) THEN Reduce (-1) THEN (InstHyp [⌜n + 1⌝] (-1)⋅ THENA 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
4. ∀n@0:ℕ. n <z n@0 = ff
5. n <z n + 1 = 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))
3.  \mforall{}n:\mBbbN{}.  ff  =  ff  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n@0:\mBbbN{}.  (\mlambda{}i.n  <z  i)  n@0  =  ff
\mvdash{}  False


By

---

Latex:
(D  -1  THEN  (D  -2  THENA  Auto)  THEN  Reduce  (-1)  THEN  (InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index