---

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

(∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))) ⇒ (¬(∀A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ. squashed-continuity1-rel(A)))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. ∀A:ℙ. ⇃(∃a:ℕ ⟶ ℕ. (A ⇐⇒ ∃n:ℕ. ((a n) = 1 ∈ ℤ)))
2. ∀A:(ℕ ⟶ ℕ) ⟶ (ℕ ⟶ ℕ) ⟶ ℙ. squashed-continuity1-rel(A)
⊢ False

---

Latex:

---

Latex:
(\mforall{}A:\mBbbP{}.  \00D9(\mexists{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (A  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((a  n)  =  1))))
{}\mRightarrow{}  (\mneg{}(\mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  squashed-continuity1-rel(A)))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index