More reverse mathematics of the Heine-Borel Theorem (2012)

JEFFRY L HIRST & JESSICA MILLER, JLA 2012

On page 2 of the paper, "HB(X): X is a subset of [0,1] and for every closed (in the topology on ℝ) subset A ⊆ X, every open cover of A contains a finite sub cover"

Here we prove a scheme formalizing the Heine-Borel Theorem for subsets of [0,1] in ℝ. This will be later used to give characterization of subsets of [0,1] for which the HB theorem is equivalent to Weak Konig's Lemma (WKL0) in the big five reverse mathematics axiom systems.

theorem HirstMiller.bounded_icc {r_c : ℝ} : Bornology.IsBounded {r : ℝ | 0 ≤ r ∧ r ≤ r_c}

show that an interval is bounded

theorem HirstMiller.subset_bounded_01 : Bornology.IsBounded (Set.Icc 0 1)

show that [0,1] is bounded

theorem HirstMiller.subset_bounded_X {X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) : Bornology.IsBounded X

show that X ⊆ [0,1], is bounded

theorem HirstMiller.subset_bounded_A {X A : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) : Bornology.IsBounded A

show that A ⊆ X, is bounded

theorem HirstMiller.compact_A {A X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) (hClosed : IsClosed A) : IsCompact A

show that A is compact for every closed subset of A

theorem HirstMiller.finite_subcover_A {I : Type u_1} {A X : Set ℝ} (hX : X ⊆ Set.Icc 0 1) (hA : A ⊆ X) (hClosed : IsClosed A) (U : I → Set ℝ) (hOpen : ∀ (i : I), IsOpen (U i)) (hCover : A ⊆ ⋃ (i : I), U i) : ∃ (J : Finset I), A ⊆ ⋃ i ∈ J, U i

show that every open cover of A contains a finite subcover

show that (X ⊆ [0,1], A ⊆ X) doesn't matter in HB(X) Thus the usual Heine-Borel theorem states "If X is closed and bounded ↔ X is compact thus every open cover of X has a finite subcover."

instance HirstMiller.instProperSpaceReal_marginis : ProperSpace ℝ

X is compact → X is closed ∧ bounded

On page 2 of the paper, "S(X): X is a subset of [0,1] and there is a countable dense in itself set Y which is contained in every closed superset of X"

Here we prove a scheme formalizing the S(X) proposition for subsets of [0,1] in ℝ. This will be later used to give characterization of subsets of [0,1] which will be used in theorem 2 to prove Weak Konig's Lemma (WKL0) and Recursive Comprehension Axiom (RCA0). Thus, theorem 2 states "If S(X) holds, then the Heine-Borel theorem for X implies WKL0. That is, S(X) implies HB(X) → WKL0." In order to do so, we prove scenarios of when S(X) holds or not.

theorem HirstMiller.dense_empty : Preperfect ∅

show that the empty set is dense in itself (dense in itself is called preperfect in LEAN v4)

def HirstMiller.S (X : Set ℝ) : Prop

define S(X) by introducing C as the closed superset of X

Equations

• HirstMiller.S X = (X ⊆ Set.Icc 0 1 ∧ ∃ (Y : Set ℝ), Countable ↑Y ∧ Preperfect Y ∧ ∀ (C : Set ℝ), IsClosed C ∧ X ⊆ C → Y ⊆ C)

def HirstMiller.φ (X Y : Set ℝ) : Prop

define φ as "Y which is contained in every closed superset of X"

Equations

• HirstMiller.φ X Y = ∀ (C : Set ℝ), IsClosed C ∧ X ⊆ C → Y ⊆ C

def HirstMiller.ψ (X : Set ℝ) : Prop

define ψ as S(X) except X being a subset of [0,1] is omitted

Equations

• HirstMiller.ψ X = ∃ (Y : Set ℝ), Y ≠ ∅ ∧ Countable ↑Y ∧ Preperfect Y ∧ HirstMiller.φ X Y

def HirstMiller.S_prime (X : Set ℝ) : Prop

define S(X) in a condensed manner including [0,1]

Equations

• HirstMiller.S_prime X = (X ⊆ Set.Icc 0 1 ∧ HirstMiller.ψ X)

theorem HirstMiller.S_true (X : Set ℝ) (hX : X ⊆ Set.Icc 0 1) : S X

prove S(X) is always true ∀ x ∈ [0,1]

theorem HirstMiller.Y_dense (Y : Set ℝ) (hY : Y ≠ ∅ ∧ Countable ↑Y ∧ Preperfect Y ∧ ∀ (C : Set ℝ), IsClosed C ∧ {1} ⊆ C → Y ⊆ C) (this : Y ⊆ {1}) : Y = {1}

prove that there is a countable dense in itself set Y which is contained in every closed superset of X