Step
*
1
of Lemma
not-LPO
1. ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))
2. ∀f:ℕ ⟶ ℕ. ∃k:ℕ. (0 < k
⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
3. F : f:(ℕ ⟶ ℕ) ⟶ ℕ
4. ∀f:ℕ ⟶ ℕ. (0 < F f
⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
⊢ False
BY
{ ((InstLemma `weak-continuity-nat-nat` [⌜F⌝;⌜λn.0⌝]⋅ THENA Auto)
THEN (FLemma `squash-from-quotient` [-1] THENA Auto)
THEN RepeatFor 2 (D -1)) }
1
1. ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))
2. ∀f:ℕ ⟶ ℕ. ∃k:ℕ. (0 < k
⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
3. F : f:(ℕ ⟶ ℕ) ⟶ ℕ
4. ∀f:ℕ ⟶ ℕ. (0 < F f
⇐⇒ ∀n:ℕ. ((f n) = 0 ∈ ℤ))
5. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ))
⇒ ((F (λn.0)) = (F g) ∈ ℕ)))
6. n : ℕ
7. ∀g:ℕ ⟶ ℕ. (((λn.0) = g ∈ (ℕn ⟶ ℕ))
⇒ ((F (λn.0)) = (F g) ∈ ℕ))
⊢ False
Latex:
Latex:
1. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}n:\mBbbN{}. ((f n) = 0)) \mvee{} (\mneg{}(\mforall{}n:\mBbbN{}. ((f n) = 0))))
2. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mexists{}k:\mBbbN{}. (0 < k \mLeftarrow{}{}\mRightarrow{} \mforall{}n:\mBbbN{}. ((f n) = 0))
3. F : f:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}
4. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (0 < F f \mLeftarrow{}{}\mRightarrow{} \mforall{}n:\mBbbN{}. ((f n) = 0))
\mvdash{} False
By
Latex:
((InstLemma `weak-continuity-nat-nat` [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}\mlambda{}n.0\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (FLemma `squash-from-quotient` [-1] THENA Auto)
THEN RepeatFor 2 (D -1))
Home
Index