Reverse mathematics, trichotomy, and dichotomy

by Dorais, Hirst and Shafer

We formalize Weak König's Lemma in the form of their Theorem 16, item 2:

If α_i^j, i ≤ n_j, j ∈ ℕ is a sequence of finite sequences of reals, then there is a function h : ℕ → ℕ such that ∀ j ∈ ℕ, ∀ i ≤ n_j, α_{h(j)}^j ≤ α_i^j

Note that the condition i ≤ n_j becomes i : Fin (n j).succ in Lean, so item 2 is correct as stated.

theorem least_real {n : ℕ} (α : Fin n.succ → ℝ) : ∃ (i : Fin n.succ), ∀ (j : Fin n.succ), α i ≤ α j

noncomputable def h₀ {n : ℕ} (α : Fin n.succ → ℝ) : { i : Fin n.succ // ∀ (j : Fin n.succ), α i ≤ α j }

Equations

• h₀ α = Classical.choice ⋯

theorem Weak_Konig's_Lemma (n : ℕ → ℕ) (α : (j : ℕ) → Fin (n j).succ → ℝ) : ∃ (h : (j : ℕ) → Fin (n j).succ), ∀ (j : ℕ) (i : Fin (n j).succ), α j (h j) ≤ α j i