Step
*
1
of Lemma
not-choice-baire-to-nat
1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P[t])
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
2. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((t f) = (t g) ∈ ℕ)))
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((t f) = (t g) ∈ ℕ)))
⊢ False
BY
{ (InstLemma `strong-continuity2-implies-weak-skolem` [] THEN RWO "-2" (-1)) }
1
1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P[t])
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]))
2. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((t f) = (t g) ∈ ℕ)))
⇐⇒ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((t f) = (t g) ∈ ℕ)))
3. ⇃(∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((F f) = (F g) ∈ ℕ)))
⊢ False
Latex:
Latex:
1. \mforall{}P:((\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}. (\mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \00D9(P[t]) \mLeftarrow{}{}\mRightarrow{} \00D9(\mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. P[t]))
2. \mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}M:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((t f) = (t g))))
\mLeftarrow{}{}\mRightarrow{} \00D9(\mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mexists{}M:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((t f) = (t g))))
\mvdash{} False
By
Latex:
(InstLemma `strong-continuity2-implies-weak-skolem` [] THEN RWO "-2" (-1))
Home
Index