---

Step * 1 1 of Lemma unsquashed-weak-continuity-base-false


1. MC : Base
2. MC ∈ F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a@0,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a@0. ((a@0 i) = (b i) ∈ ℕ)) ⇒ ((F a@0) = (F b) ∈ ℕ))
⊢ False
BY
{ TACTIC:Assert ⌜∃M:Base
                  ((M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ)
                  ∧ (∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base.
                       ((∀i:ℕM F. ((a i) = 0 ∈ ℕ)) ⇒ ((F a) = (F (λx.0)) ∈ ℕ))))⌝⋅ }

1
.....assertion..... 
1. MC : Base
2. MC ∈ F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a@0,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a@0. ((a@0 i) = (b i) ∈ ℕ)) ⇒ ((F a@0) = (F b) ∈ ℕ))
⊢ ∃M:Base
   ((M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ)
   ∧ (∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕM F. ((a i) = 0 ∈ ℕ)) ⇒ ((F a) = (F (λx.0)) ∈ ℕ))))

2
1. MC : Base
2. MC ∈ F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a@0,b:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕMC F a@0. ((a@0 i) = (b i) ∈ ℕ)) ⇒ ((F a@0) = (F b) ∈ ℕ))
4. ∃M:Base
    ((M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ)
    ∧ (∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕM F. ((a i) = 0 ∈ ℕ)) ⇒ ((F a) = (F (λx.0)) ∈ ℕ))))
⊢ False

---

Latex:

---

Latex:

1.  MC  :  Base
2.  MC  \mmember{}  F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}
3.  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  \mforall{}a@0,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.
          ((\mforall{}i:\mBbbN{}MC  F  a@0.  ((a@0  i)  =  (b  i)))  {}\mRightarrow{}  ((F  a@0)  =  (F  b)))
\mvdash{}  False


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mexists{}M:Base
                                ((M  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{})
                                \mwedge{}  (\mforall{}F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.
                                          ((\mforall{}i:\mBbbN{}M  F.  ((a  i)  =  0))  {}\mRightarrow{}  ((F  a)  =  (F  (\mlambda{}x.0))))))\mkleeneclose{}\mcdot{}

---

Home Index