|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Phase 1.1 of the WF-track "Option B" programme in |
| 4 | +-- `docs/buchholz-plan.adoc`. Establishes a constructive |
| 5 | +-- Brouwer-style ordinal notation with a direct well-foundedness |
| 6 | +-- proof. This file does NOT depend on `Ordinal.Buchholz.Order` |
| 7 | +-- or any `<ᵇ` infrastructure — that independence is the whole |
| 8 | +-- point. Later phases (2+) will embed the Buchholz order into |
| 9 | +-- this rank target and derive `wf-<ᵇ` for the enlarged order via |
| 10 | +-- `Subrelation.wellFounded`. |
| 11 | +-- |
| 12 | +-- Representation: zero, successor, ℕ-indexed supremum. This already |
| 13 | +-- exhausts countable ordinals below ω₁; for Buchholz rank up to |
| 14 | +-- ψ(Ω_ω) it is far more than we need. |
| 15 | +-- |
| 16 | +-- The strict order `_<_` is defined as `osuc α ≤ β`. WF is proved by |
| 17 | +-- structural induction on `Ord` directly; the higher-order `olim` |
| 18 | +-- branch is accepted by Agda's structural recursion on subterms of |
| 19 | +-- the function-indexed inductive. |
| 20 | + |
| 21 | +module Ordinal.Brouwer where |
| 22 | + |
| 23 | +open import Data.Empty using (⊥; ⊥-elim) |
| 24 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 25 | +open import Induction.WellFounded using (Acc; acc; WellFounded; wf⇒asym) |
| 26 | +open import Relation.Nullary using (¬_) |
| 27 | + |
| 28 | +---------------------------------------------------------------------------- |
| 29 | +-- Ordinal notations |
| 30 | +---------------------------------------------------------------------------- |
| 31 | + |
| 32 | +data Ord : Set where |
| 33 | + oz : Ord |
| 34 | + osuc : Ord → Ord |
| 35 | + olim : (ℕ → Ord) → Ord |
| 36 | + |
| 37 | +---------------------------------------------------------------------------- |
| 38 | +-- Strict and non-strict orders |
| 39 | +---------------------------------------------------------------------------- |
| 40 | + |
| 41 | +infix 4 _≤_ _<_ |
| 42 | + |
| 43 | +-- Reflexive closure. Three generators: |
| 44 | +-- * identity, |
| 45 | +-- * one-step successor on the right-hand side, |
| 46 | +-- * selecting a specific branch inside a limit on the right. |
| 47 | + |
| 48 | +data _≤_ : Ord → Ord → Set where |
| 49 | + ≤-refl : ∀ {α} → α ≤ α |
| 50 | + ≤-suc : ∀ {α β} → α ≤ β → α ≤ osuc β |
| 51 | + ≤-lim : ∀ {α f} n → α ≤ f n → α ≤ olim f |
| 52 | + |
| 53 | +-- Strict order: successor of α still fits at-or-below β. |
| 54 | + |
| 55 | +_<_ : Ord → Ord → Set |
| 56 | +α < β = osuc α ≤ β |
| 57 | + |
| 58 | +---------------------------------------------------------------------------- |
| 59 | +-- Basic structural properties |
| 60 | +---------------------------------------------------------------------------- |
| 61 | + |
| 62 | +-- Zero is minimum. Structural on the right-hand side. |
| 63 | + |
| 64 | +≤-zero : ∀ {α} → oz ≤ α |
| 65 | +≤-zero {oz} = ≤-refl |
| 66 | +≤-zero {osuc α} = ≤-suc ≤-zero |
| 67 | +≤-zero {olim f} = ≤-lim 0 ≤-zero |
| 68 | + |
| 69 | +-- Weakening into successor. |
| 70 | + |
| 71 | +≤-step : ∀ {α β} → α ≤ β → α ≤ osuc β |
| 72 | +≤-step = ≤-suc |
| 73 | + |
| 74 | +-- Each branch of a limit sits at-or-below it. Strict-below is not |
| 75 | +-- available in general — a constant sequence has `f n ≡ olim f` — |
| 76 | +-- but the ≤ witness is enough for rank bookkeeping. |
| 77 | + |
| 78 | +f-in-lim : ∀ f n → f n ≤ olim f |
| 79 | +f-in-lim f n = ≤-lim n ≤-refl |
| 80 | + |
| 81 | +-- Successor strictly above its predecessor. |
| 82 | + |
| 83 | +<-suc-self : ∀ {α} → α < osuc α |
| 84 | +<-suc-self = ≤-refl |
| 85 | + |
| 86 | +---------------------------------------------------------------------------- |
| 87 | +-- Transitivity |
| 88 | +---------------------------------------------------------------------------- |
| 89 | + |
| 90 | +-- Transitivity of ≤ by induction on the right leg. `≤-refl` case |
| 91 | +-- returns the left leg unchanged; `≤-suc` / `≤-lim` cases propagate. |
| 92 | + |
| 93 | +≤-trans : ∀ {α β γ} → α ≤ β → β ≤ γ → α ≤ γ |
| 94 | +≤-trans p ≤-refl = p |
| 95 | +≤-trans p (≤-suc q) = ≤-suc (≤-trans p q) |
| 96 | +≤-trans p (≤-lim n q) = ≤-lim n (≤-trans p q) |
| 97 | + |
| 98 | +-- β ≤ osuc β, the canonical one-step witness. |
| 99 | + |
| 100 | +≤-osuc : ∀ {β} → β ≤ osuc β |
| 101 | +≤-osuc = ≤-suc ≤-refl |
| 102 | + |
| 103 | +-- Transitivity of <: osuc α ≤ β ≤ osuc β ≤ osuc β... ≤ γ. |
| 104 | + |
| 105 | +<-trans : ∀ {α β γ} → α < β → β < γ → α < γ |
| 106 | +<-trans {α} {β} p q = ≤-trans (≤-trans p ≤-osuc) q |
| 107 | + |
| 108 | +---------------------------------------------------------------------------- |
| 109 | +-- Well-foundedness |
| 110 | +---------------------------------------------------------------------------- |
| 111 | + |
| 112 | +-- Predecessor of osuc α is either α itself (≤-refl case) or a |
| 113 | +-- strictly smaller β with β < α (≤-suc case). Both yield Acc. |
| 114 | + |
| 115 | +pred-of-osuc : ∀ {α} → Acc _<_ α → ∀ {β} → β < osuc α → Acc _<_ β |
| 116 | +pred-of-osuc (acc rsα) ≤-refl = acc rsα |
| 117 | +pred-of-osuc (acc rsα) (≤-suc q) = rsα q |
| 118 | + |
| 119 | +-- Predecessor of olim f: must come via ≤-lim with a branch index `n`, |
| 120 | +-- giving β < f n. Inductive accessibility of f n gives Acc β. |
| 121 | + |
| 122 | +pred-of-olim : |
| 123 | + ∀ {f} → (∀ n → Acc _<_ (f n)) → |
| 124 | + ∀ {β} → β < olim f → Acc _<_ β |
| 125 | +pred-of-olim wfs (≤-lim n q) with wfs n |
| 126 | +... | acc rs = rs q |
| 127 | + |
| 128 | +-- Top-level WF: structural induction on Ord. |
| 129 | + |
| 130 | +wf-< : WellFounded _<_ |
| 131 | +wf-< oz = acc λ () |
| 132 | +wf-< (osuc α) = acc (pred-of-osuc (wf-< α)) |
| 133 | +wf-< (olim f) = acc (pred-of-olim (λ n → wf-< (f n))) |
| 134 | + |
| 135 | +---------------------------------------------------------------------------- |
| 136 | +-- Derived corollaries |
| 137 | +---------------------------------------------------------------------------- |
| 138 | + |
| 139 | +-- Irreflexivity via wf⇒asym; no direct pattern match is needed. |
| 140 | + |
| 141 | +<-irrefl : ∀ {α} → ¬ (α < α) |
| 142 | +<-irrefl {α} p = wf⇒asym wf-< p p |
| 143 | + |
| 144 | +-- Worked small witnesses. |
| 145 | + |
| 146 | +one : Ord |
| 147 | +one = osuc oz |
| 148 | + |
| 149 | +two : Ord |
| 150 | +two = osuc one |
| 151 | + |
| 152 | +ω : Ord |
| 153 | +ω = olim nat-to-ord |
| 154 | + where |
| 155 | + nat-to-ord : ℕ → Ord |
| 156 | + nat-to-ord zero = oz |
| 157 | + nat-to-ord (suc n) = osuc (nat-to-ord n) |
| 158 | + |
| 159 | +oz<one : oz < one |
| 160 | +oz<one = <-suc-self |
| 161 | + |
| 162 | +one<two : one < two |
| 163 | +one<two = <-suc-self |
| 164 | + |
| 165 | +oz<two : oz < two |
| 166 | +oz<two = <-trans oz<one one<two |
| 167 | + |
| 168 | +one<ω : one < ω |
| 169 | +one<ω = ≤-lim 2 ≤-refl |
0 commit comments