Step
*
1
of Lemma
gen-continuity-contradicts-markov
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f)
⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ))
⇒ (P g))))
2. ∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n))))
⇒ (¬¬(∃n:ℕ. (A n)))
⇒ (∃n:ℕ. (A n)))
⊢ False
BY
{ Assert ⌜∀a:{a:ℕ ⟶ ℕ| init0(a) ∧ increasing-sequence(a)} . ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )⌝⋅ }
1
.....assertion.....
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f)
⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ))
⇒ (P g))))
2. ∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n))))
⇒ (¬¬(∃n:ℕ. (A n)))
⇒ (∃n:ℕ. (A n)))
⊢ ∀a:{a:ℕ ⟶ ℕ| init0(a) ∧ increasing-sequence(a)} . ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )
2
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f)
⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ))
⇒ (P g))))
2. ∀A:ℕ ⟶ ℙ. ((∀n:ℕ. ((A n) ∨ (¬(A n))))
⇒ (¬¬(∃n:ℕ. (A n)))
⇒ (∃n:ℕ. (A n)))
3. ∀a:{a:ℕ ⟶ ℕ| init0(a) ∧ increasing-sequence(a)} . ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )
⊢ False
Latex:
Latex:
1. \mforall{}P:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((P f) {}\mRightarrow{} \00D9(\mexists{}k:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} (P g))))
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)))
\mvdash{} False
By
Latex:
Assert \mkleeneopen{}\mforall{}a:\{a:\mBbbN{} {}\mrightarrow{} \mBbbN{}| init0(a) \mwedge{} increasing-sequence(a)\} . \mforall{}m:\mBbbN{}. \mexists{}n:\mBbbN{}. ((a n) \mgeq{} m )\mkleeneclose{}\mcdot{}
Home
Index