Step
*
1
1
of Lemma
not-choice-baire-to-nat-ssq
1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
⇐⇒ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t])
2. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ. ((f = g ∈ (ℕM f ⟶ ℕ))
⇒ ((F f) = (F g) ∈ ℕ))
⊢ False
BY
{ ((Assert ⌜¬unsquashed-WCP⌝⋅ THENA Auto)
THEN D (-1)
THEN (D 0 THENA Auto)
THEN (InstHyp [⌜F⌝] (-2)⋅ THENA Auto)
THEN ExRepD
THEN InstConcl [⌜M⌝]⋅
THEN Auto) }
Latex:
Latex:
1. \mforall{}P:((\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}. (\mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. (\mdownarrow{}P[t]) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mforall{}t:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. P[t])
2. \mforall{}F:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mexists{}M:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} ((F f) = (F g)))
\mvdash{} False
By
Latex:
((Assert \mkleeneopen{}\mneg{}unsquashed-WCP\mkleeneclose{}\mcdot{} THENA Auto)
THEN D (-1)
THEN (D 0 THENA Auto)
THEN (InstHyp [\mkleeneopen{}F\mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN ExRepD
THEN InstConcl [\mkleeneopen{}M\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index