Step
*
1
1
2
1
of Lemma
unsquashed-weak-continuity-base-false
1. M : Base
2. M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕM F. ((a i) = 0 ∈ ℕ))
⇒ ((F a) = (F (λx.0)) ∈ ℕ))
⊢ False
BY
{ TACTIC:Assert ⌜∃J,K:ℕ. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ))
⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))⌝⋅ }
1
.....assertion.....
1. M : Base
2. M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕM F. ((a i) = 0 ∈ ℕ))
⇒ ((F a) = (F (λx.0)) ∈ ℕ))
⊢ ∃J,K:ℕ. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ))
⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))
2
1. M : Base
2. M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕM F. ((a i) = 0 ∈ ℕ))
⇒ ((F a) = (F (λx.0)) ∈ ℕ))
4. ∃J,K:ℕ. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ))
⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))
⊢ False
Latex:
Latex:
1. M : Base
2. M \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbN{} \mcap{} Base {}\mrightarrow{} \mBbbN{} \mcap{} Base {}\mrightarrow{} \mBbbN{}
3. \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))))
\mvdash{} False
By
Latex:
TACTIC:Assert \mkleeneopen{}\mexists{}J,K:\mBbbN{}. \mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{} \mcap{} Base. ((\mforall{}i:\mBbbN{}K. ((a i) = 0)) {}\mRightarrow{} ((M (\mlambda{}f.(a (f J)))) = J))\mkleeneclose{}\mcdot{}
Home
Index