---

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


1. ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. f i = g i) ⇒ (∀n:ℕ. f n = ff ⇐⇒ ∀n:ℕ. g n = ff)))
⊢ False
BY
{ ((With ⌜λn.ff⌝ (D 1)⋅ THENA Auto) THEN SqExRepD THEN Reduce (-1)) }

1
1. n : ℕ
2. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. ff = g i) ⇒ (∀n:ℕ. ff = ff ⇐⇒ ∀n:ℕ. g n = ff))
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}n.ff\mkleeneclose{}  (D  1)\mcdot{}  THENA  Auto)  THEN  SqExRepD  THEN  Reduce  (-1))

---

Home Index