---

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