---

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


1. weak-continuity(𝔹;𝔹)
2. ∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff)
⊢ False
BY
{ ((Assert ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. f i = g i) ⇒ (∀n:ℕ. f n = ff ⇐⇒ ∀n:ℕ. g n = ff))) BY
          (RenameVar `p' (-1)
           THEN (With ⌜λf.isl(p f)⌝ (D 1)⋅ THENA (Auto THEN GenConclTerm ⌜p f⌝⋅ THEN Auto))
           THEN Reduce (-1)
           THEN (RepeatFor 5 (ParallelLast') THENA Auto)
           THEN MoveToConcl (-1)
           THEN (GenConclTerm ⌜p f⌝⋅ THENA Auto)
           THEN Thin (-1)
           THEN D -1
           THEN (GenConclTerm ⌜p g⌝⋅ THENA Auto)
           THEN Thin (-1)
           THEN D -1
           THEN Reduce 0
           THEN Auto))
   THEN RepeatFor 2 (Thin 1)
   ) }

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

---

Latex:

---

Latex:

1.  weak-continuity(\mBbbB{};\mBbbB{})
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Dec(\mforall{}n:\mBbbN{}.  f  n  =  ff)
\mvdash{}  False


By

---

Latex:
((Assert  \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)))  BY
                (RenameVar  `p'  (-1)
                  THEN  (With  \mkleeneopen{}\mlambda{}f.isl(p  f)\mkleeneclose{}  (D  1)\mcdot{}  THENA  (Auto  THEN  GenConclTerm  \mkleeneopen{}p  f\mkleeneclose{}\mcdot{}  THEN  Auto))
                  THEN  Reduce  (-1)
                  THEN  (RepeatFor  5  (ParallelLast')  THENA  Auto)
                  THEN  MoveToConcl  (-1)
                  THEN  (GenConclTerm  \mkleeneopen{}p  f\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  Thin  (-1)
                  THEN  D  -1
                  THEN  (GenConclTerm  \mkleeneopen{}p  g\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  Thin  (-1)
                  THEN  D  -1
                  THEN  Reduce  0
                  THEN  Auto))
  THEN  RepeatFor  2  (Thin  1)
  )

---

Home Index