---

Step * 1 1 1 of Lemma kripke's-schema-contradicts-squashed-continuity1-rel


1. ∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))
2. ∀A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ. squashed-continuity1-rel(A)
3. ∀a:ℕ ⟶ ℕ. ⇃(∃b:ℕ ⟶ ℕ. (∀n:ℕ. ((a n) = 1 ∈ ℤ) ⇐⇒ ∃n:ℕ. ((b n) = 1 ∈ ℤ)))
4. ⇃(∃c:(ℕ ⟶ ℕ) ⟶ ℕ
      ((∀a:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((c a) = (c b) ∈ ℕ))))
      ∧ (∀a:ℕ ⟶ ℕ. (∀n:ℕ. ((a n) = 1 ∈ ℤ) ⇐⇒ ∃n:ℕ. ((shift-seq(c;a) n) = 1 ∈ ℤ)))))
⊢ False
BY
{ ((Assert ⌜↓False⌝⋅ THENM Auto)
   THEN (BLemma `squash-from-quotient` THENA Auto)
   THEN MoveToConcl (-1)
   THEN (BLemma `implies-quotient-true` THENA Auto)
   THEN (D 0 THENA Auto)) }

1
1. ∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))
2. ∀A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ. squashed-continuity1-rel(A)
3. ∀a:ℕ ⟶ ℕ. ⇃(∃b:ℕ ⟶ ℕ. (∀n:ℕ. ((a n) = 1 ∈ ℤ) ⇐⇒ ∃n:ℕ. ((b n) = 1 ∈ ℤ)))
4. ∃c:(ℕ ⟶ ℕ) ⟶ ℕ
    ((∀a:ℕ ⟶ ℕ. ⇃(∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((c a) = (c b) ∈ ℕ))))
    ∧ (∀a:ℕ ⟶ ℕ. (∀n:ℕ. ((a n) = 1 ∈ ℤ) ⇐⇒ ∃n:ℕ. ((shift-seq(c;a) n) = 1 ∈ ℤ))))
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}A:\mBbbP{}.  \00D9(\mexists{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (A  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((a  n)  =  1)))
2.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  squashed-continuity1-rel(A)
3.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (\mforall{}n:\mBbbN{}.  ((a  n)  =  1)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((b  n)  =  1)))
4.  \00D9(\mexists{}c:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}
            ((\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((a  =  b)  {}\mRightarrow{}  ((c  a)  =  (c  b)))))
            \mwedge{}  (\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (\mforall{}n:\mBbbN{}.  ((a  n)  =  1)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((shift-seq(c;a)  n)  =  1)))))
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}\mdownarrow{}False\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  (BLemma  `squash-from-quotient`  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (BLemma  `implies-quotient-true`  THENA  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index