Step
*
1
1
of Lemma
afcs-contradicts-markov
1. ∃a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a) ∧ init0(a) ∧ increasing-sequence(a))
2. ∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n))))
⇒ (¬¬(∃n:ℕ. (A n)))
⇒ (∃n:ℕ. (A n)))
3. ∀a:ℕ ⟶ ℕ. (is-absolutely-free{i:l}(a)
⇒ increasing-sequence(a)
⇒ (∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )))
⊢ False
BY
{ (InstLemma `Kripke2b` [] THEN ExRepD THEN (InstHyp [⌜a⌝] (-2)⋅ THENA Auto) THEN InstHyp [⌜a⌝] (-2)⋅ THEN Auto) }
Latex:
Latex:
1. \mexists{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (is-absolutely-free\{i:l\}(a) \mwedge{} init0(a) \mwedge{} increasing-sequence(a))
2. \mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbP{}. ((\mforall{}n:\mBbbN{}. ((A n) \mvee{} (\mneg{}(A n)))) {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}. (A n))) {}\mRightarrow{} (\mexists{}n:\mBbbN{}. (A n)))
3. \mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (is-absolutely-free\{i:l\}(a) {}\mRightarrow{} increasing-sequence(a) {}\mRightarrow{} (\mforall{}m:\mBbbN{}. \mexists{}n:\mBbbN{}. ((a n) \mgeq{} m )))
\mvdash{} False
By
Latex:
(InstLemma `Kripke2b` []
THEN ExRepD
THEN (InstHyp [\mkleeneopen{}a\mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN InstHyp [\mkleeneopen{}a\mkleeneclose{}] (-2)\mcdot{}
THEN Auto)
Home
Index