Unique paths as formal points

by Thierry Coquand, Peter Schuster

The paper mentions Weak König's Lemma.

We (define and) prove:

• WKL (Fin 0) (this is vacuous for any set, not just trees).
• WKL (Fin 1). This is computable and uses a nice exercise in list induction, zerolist.
• An equivalent, using Classical.choice, of WKL (Fin 2) at https://github.com/bjoernkjoshanssen/jla/blob/main/2012-dorais-hirst-shafer.lean
• ¬ WKL ℕ.

For Fin 1 the path is indeed (obviously) unique.

def tree {α : Type} (T : Set (List α)) : Prop

Equations

• tree T = ∀ σ ∈ T, ∀ (τ : List α), τ <+: σ → τ ∈ T

def has_a_path {α : Type} (T : Set (List α)) : Prop

Equations

• has_a_path T = ∃ (p : ℕ → α), ∀ (k : ℕ), (List.ofFn fun (i : Fin k) => p ↑i) ∈ T

def WKL {α : Type} : Prop

Equations

• WKL = ∀ (T : Set (List α)), tree T → Infinite ↑T → has_a_path T

theorem wklFin0 : WKL

theorem notWklFinNat : ¬WKL

theorem zerolist (σ : List (Fin 1)) : σ = List.replicate σ.length 0

theorem wklFin1 : WKL