--- title: "Ordinal closure and finite ordinals" module: L.Ordinal lang: en site: "Bedrock" description: "Ordinal closure and finite ordinals" stage: "Constructible stages and the axioms" reading_order: 26 canonical: https://bedrock.institute/en/L.Ordinal.html html: L.Ordinal.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Model, V.Coding, L.Constructible] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Ordinal.md, https://bedrock.institute/ja/L.Ordinal.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Ordinal closure and finite ordinals Ordinals are transitive sets whose members are transitive. This chapter proves closure under zero, successor, and unions, constructs ordinal bounds for small families, and identifies membership among the finite numerals and `ω`. The chapter develops these closure and bounding tools before turning to finite ordinals. Zero is an ordinal; successors of ordinals are ordinals; a union of ordinals is an ordinal; and, as the chapter's main result, every small family of ordinals lies below a single ordinal. That last statement turns "each member of a small family has *some* ordinal bound" into "the whole family shares *one* ordinal bound", a form used later in separation, power set, recursion, reflection, and GCH constructions. This chapter does not give comparison of ordinals. Ordinals are indeed linearly ordered, but that fact is not constructive and it is not needed here: the axioms ask only for a common bound, so the book constructs a common bound directly. None of the closure or bounding proofs in this chapter assumes classical logic. The ordinal predicate is defined in the constructible-universe chapter as `IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x)`: a pair of a transitivity proof and a proof that every member of `A` is itself transitive. Both components are propositions, and `isPropIsOrd` certifies this, so `IsOrd` is a genuine truth value rather than structure-bearing data. The module fixes an ambient universe level `ℓ` and works with the carrier `S` of the cumulative hierarchy over it. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Ordinal {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure ) ``` Two families of tools meet here. From the side of the ambient hierarchy `V` come the successor `sucV`, its membership eliminator, and the union of a small family. From the side of the constructible universe `L` come the transitivity lemma for the empty set and for small unions, and the predicate `IsOrd` itself. Everything in this chapter is proved about the underlying sets; nothing yet refers to constructibility, so no excluded-middle assumption appears in any statement below. ```agda open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Model {ℓ} using ( union-family-in; union-family-out; ∈sucV-elim; ∈sucV-inl; self∈sucV ) open import V.Coding {ℓ} using ( #-inj′ ) open import L.Constructible {ℓ} using ( isTransV; isPropIsTransV; ∅-trans; setUnion-trans; IsOrd; isPropIsOrd ) ``` A recurring pattern in the proofs is elimination of a truncated witness. Membership in a union is only *merely* witnessed by some index and member, so a fact about all union members is extracted with `PT.rec` into a proposition-valued target. This is why each closure lemma names its target proposition, such as `isPropIsTransV z`, before consuming the truncation: elimination of `∥ A ∥₁` is permitted exactly into such propositions. ```agda open import Cubical.Data.Nat.Order using ( _<_; ≤-suc; isProp≤ ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.Data.Bool using ( Bool; true; false ) ``` The numerals `# n` are the von Neumann naturals of the hierarchy: `# 0` is the empty set and `# (suc n)` is the successor of `# n`. Their limit `ω` and the facts that each numeral lies in `ω` come from the infinity construction. The final section of the chapter will read a natural index back out of a membership `z ∈ˢ (# n)`, using that the coding of numerals is injective. ```agda open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; ⋃_; module InfinitySet ) open InfinitySet using ( sucV; #_; ω; #-in-ω ) ``` One last convention: the direct `hProp` operations are available throughout, so the notation `⟨ P ⟩` for the underlying type of a proposition `P` and the indexed connectives act directly on propositions. The propositions here, such as `isTransV A` and `IsOrd A`, live one level above `ℓ`, which is exactly the level at which the later axioms will quantify. ```agda open hPropStructure 𝒮ᵥ ``` ## Zero and successors Recall the predicate: an ordinal is a transitive set whose members are all transitive. Both halves are vacuous for the empty set, so zero is an ordinal with nothing to prove. The certificate `∅-ord` packages the two vacuous halves. Transitivity of `∅` is the already-proved lemma `∅-trans`. For the second half, the function must accept any `x` with a claimed membership `x ∈ˢ ∅`, but the empty-set lemma converts that membership into an element of the empty host type, which `Empty.rec` eliminates to prove anything at all. A member that cannot exist imposes no obligation. ```agda ∅-ord : IsOrd ∅ ∅-ord = ∅-trans , (λ x x∈∅ → Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅))) ``` The successor `sucV A` adds `A` itself as a member. A member of `sucV A` is either a member of `A` or `A` itself, and that case split is a proposition-level eliminator, `∈sucV-elim`, which requires its target to be a proposition and takes two branches. Both halves of the ordinal predicate follow this eliminator. Transitivity of `sucV A` must show `y ∈ˢ sucV A` from `y ∈ˢ x` and `x ∈ˢ sucV A`. The eliminator consumes `x∈suc`, and the proof obligation it hands to each branch is again a membership in `sucV A`, so the propositionality argument `snd (y ∈ˢ sucV A)` is supplied as the target. ```agda suc-ord : ∀ {A} → IsOrd A → IsOrd (sucV A) suc-ord {A} (Atr , Amem) = trans-sucV , mem-sucV where trans-sucV : isTransV (sucV A) trans-sucV {x} {y} y∈x x∈suc = ∈sucV-elim (snd (y ∈ˢ sucV A)) x∈suc ``` In the first branch, `x` is a member of `A`, so `A`'s transitivity applied to `y ∈ˢ x` and `x ∈ˢ A` gives `y ∈ˢ A`, hence `y ∈ˢ sucV A`. In the second branch, `x` is identified with `A` itself, so `y ∈ˢ x` transports along that path directly into `y ∈ˢ A`; no extra fact about `A` is needed there. ```agda (λ x∈A → ∈sucV-inl (Atr y∈x x∈A)) (λ x≡A → ∈sucV-inl (subst (λ w → ⟨ y ∈ˢ w ⟩) x≡A y∈x)) mem-sucV : (x : S) → ⟨ x ∈ˢ sucV A ⟩ → isTransV x mem-sucV x x∈suc = ∈sucV-elim (isPropIsTransV x) x∈suc (λ x∈A → Amem x x∈A) ``` The second half, that every member of `sucV A` is transitive, is the same case split with a different target. Members of `A` are transitive by the hypothesis `Amem`; in the branch where `x` equals `A`, the transitivity `Atr` is transported back along the reversed path. The propositionality of `isTransV x` is what makes the eliminator applicable here. ```agda (λ x≡A → subst isTransV (sym x≡A) Atr) ``` ## Unions and bounds Ordinals are closed under small-indexed unions. Transitivity is the closure lemma already proved for transitive sets; for the second half, a member of the union sits inside some `f x`, and that family member is an ordinal by hypothesis, so its own members are transitive. The family is given by a small type `X` of indices and a map `f : X → S`, so the union `⋃ (sett X f)` is a set built from an honest function rather than a truncated enumeration. Its transitivity is borrowed directly from `setUnion-trans`, feeding it the first component of each hypothesis `hf x`. ```agda setUnion-ord : (X : Type ℓ) (f : X → S) → ((x : X) → IsOrd (f x)) → IsOrd (⋃ (sett X f)) setUnion-ord X f hf = setUnion-trans X f (λ x → hf x .fst) , memTr where memTr : (z : S) → ⟨ z ∈ˢ (⋃ (sett X f)) ⟩ → isTransV z ``` For the remaining obligation, `union-family-out` states that `z ∈ˢ ⋃ (sett X f)` means merely that `z` lies in some `f x`. Since the goal `isTransV z` is a proposition, `PT.rec` may eliminate that truncation, and in each branch `hf x .snd z hz` supplies exactly the needed certificate: a member of an ordinal family member is transitive. ```agda memTr z z∈⋃ = PT.rec (isPropIsTransV z) (λ { (x , hz) → hf x .snd z hz }) (union-family-out X f z z∈⋃) ``` And the chapter's deliverable. Given a small family of ordinals, a single ordinal contains every member of the family. The naive attempt, take the union of the family, gives only inclusion: a union absorbs its members' *elements*, not the members themselves, and no set contains itself. The repair is one step of successor: union the family of successors instead. The result is a genuine pair, not a truncated existence: the consumers name the bound and form its stage. The result returns the bound `β` as explicit data, together with its ordinal certificate and, for each index, a strict membership `f x ∈ˢ β`. Later proofs can project the bound and these memberships directly, without eliminating a truncated existence. ```agda boundingOrd : (X : Type ℓ) (f : X → S) → ((x : X) → IsOrd (f x)) → Σ[ β ∈ S ] (IsOrd β × ((x : X) → ⟨ f x ∈ˢ β ⟩)) boundingOrd X f hf = β , (ordβ , memβ) where g : X → S ``` The construction is three lines of mathematics. Replace `f` by its successor `g x = sucV (f x)`; take the union `β` of that family; and apply the union closure just proved, whose hypotheses hold because each `sucV (f x)` is an ordinal by the successor lemma. ```agda g x = sucV (f x) β : S β = ⋃ (sett X g) ordβ : IsOrd β ordβ = setUnion-ord X g (λ x → suc-ord (hf x)) ``` The memberships are why the detour through successors is necessary. Each `f x` lies strictly inside its own successor, `union-family-in` lifts that into the union, and the union's own transitivity then upgrades the strict memberships to the inclusion the closure arguments use downstream. ```agda memβ : (x : X) → ⟨ f x ∈ˢ β ⟩ memβ x = union-family-in X g x (f x) (self∈sucV (f x)) ``` The two-element case is worth naming, because it is the one that gets used most: merging two ordinals into a single ordinal strictly containing both. The family is indexed by the booleans, lifted to the ambient universe so that the general lemma applies, and the two memberships are read off at the two indices. The result packages three pieces of data: the bound β, a proof that β is an ordinal, and the two strict memberships ⟨ σ₁ ∈ˢ β ⟩ and ⟨ σ₂ ∈ˢ β ⟩, combined with nested products. The body simply extracts these from `r`, reading the two memberships at the two boolean indices `lift true` and `lift false`; the `where` block constructs `r` below. ```agda bound2 : (σ₁ σ₂ : S) → IsOrd σ₁ → IsOrd σ₂ → Σ[ β ∈ S ] (IsOrd β × ⟨ σ₁ ∈ˢ β ⟩ × ⟨ σ₂ ∈ˢ β ⟩) bound2 σ₁ σ₂ o₁ o₂ = fst r , (r .snd .fst , r .snd .snd (lift true) , r .snd .snd (lift false)) where ``` The indexing type needs one word of care. `Bool` lives in `Type ℓ-zero` while `S` lives in `Type ℓ`, but `boundingOrd` requires its index type to sit in `Type ℓ`. `Lift` raises the level without changing the elements: they become `lift true` and `lift false`. The function `f` sends them to σ₁ and σ₂, and `fo` attaches the corresponding ordinality hypothesis at each index. ```agda f : Lift {ℓ-zero} {ℓ} Bool → S f (lift true) = σ₁ f (lift false) = σ₂ fo : (b : Lift {ℓ-zero} {ℓ} Bool) → IsOrd (f b) fo (lift true) = o₁ ``` Nothing new remains to prove. `r` is the general lemma applied to this two-point family; it already supplies an ordinal bound together with a membership for every index, and the two displayed memberships of the result are that same proof instantiated at the two booleans. ```agda fo (lift false) = o₂ r = boundingOrd (Lift {ℓ-zero} {ℓ} Bool) f fo ``` ## Members Ordinals are closed downwards: a member of an ordinal is an ordinal. Its own transitivity is the second half of the hypothesis; that its members are transitive follows by pulling them back into the ambient ordinal along transitivity. The hierarchy chapter's irreflexivity, that no set belongs to itself, is the other fact these arguments need; it is recalled here because this is where the ordinal proofs start reaching for it. Unpacked, the hypothesis `IsOrd A` is a pair: `Atr`, the transitivity of `A`, and `Amem`, the assertion that every member of `A` is transitive. So the first half of the conclusion is just `Amem x x∈A`. For the second half, take `y` with `y ∈ x ∈ A`: transitivity of `A` yields `y ∈ A`, and then `Amem y` says `y` is transitive, which is exactly what is claimed about each member of `x`. ```agda mem-ord : ∀ {A} → IsOrd A → (x : S) → ⟨ x ∈ˢ A ⟩ → IsOrd x mem-ord {A} (Atr , Amem) x x∈A = Amem x x∈A , (λ y y∈x → Amem y (Atr y∈x x∈A)) ``` ## The numerals, and their limit The hierarchy's numerals are the iterated successors of zero, so they are ordinals by the two facts above, by a single induction. Their limit `ω` is an ordinal too, and that is the fact the collection step will need. Its second half follows directly from the numeral lemmas; its first half, transitivity, says that a member of a numeral is again a numeral, which is another induction, the successor case splitting by the eliminator. One warning about the reasoning style: membership in `ω` only *merely* presents an index. The proofs below therefore never extract a chosen natural number; they eliminate the truncation into targets that are propositions, such as `IsOrd y` or a membership statement. The definition `# zero = ∅` and `# suc n = sucV (# n)` makes the induction one line per case: the empty set is an ordinal by the first section, and the successor of an ordinal is an ordinal by the second. ```agda numeral-ord : (n : ℕ) → IsOrd (# n) numeral-ord zero = ∅-ord numeral-ord (suc n) = suc-ord (numeral-ord n) ``` Inside the cumulative hierarchy library, `ω` is presented as the set whose members are indexed by natural numbers, so membership in `ω` amounts to carrying a numerical index. The lemma `#-in-ω` supplies that index for each numeral, and `∈∈ₛ` converts the resulting index into the membership proposition ⟨ `# k` ∈ˢ `ω` ⟩. ```agda #∈ω : (k : ℕ) → ⟨ (# k) ∈ˢ ω ⟩ #∈ω k = ∈∈ₛ {a = # k} {b = ω} .snd (#-in-ω k) ``` The next statement is downward closure for numerals, phrased directly as membership in `ω`: every member of `# k` is a member of `ω`. The induction on `k` has a vacuous base, since nothing belongs to the empty set. In the successor case the eliminator for `sucV` splits in two: either `y` already lies in `# k`, where the induction hypothesis applies, or `y` equals `# k` itself, where membership in `ω` follows from the previous lemma. ```agda numeral-mem : (k : ℕ) (y : S) → ⟨ y ∈ˢ (# k) ⟩ → ⟨ y ∈ˢ ω ⟩ numeral-mem zero y y∈ = Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈)) numeral-mem (suc k) y y∈ = ∈sucV-elim (snd (y ∈ˢ ω)) y∈ (λ y∈#k → numeral-mem k y y∈#k) ``` Conversely, every member of `ω` is an ordinal. Membership in `ω` merely presents a natural `k` with `# k ≡ y`; the goal `IsOrd y` is a proposition by `isPropIsOrd`, so the truncation may be eliminated into it. Along the path `# k ≡ y` the ordinality of `# k` transports to `y`. No particular index is chosen; the argument works uniformly for whichever one the truncation hides. ```agda (λ y≡#k → subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym y≡#k) (#∈ω k)) ω-mem-ord : (y : S) → ⟨ y ∈ˢ ω ⟩ → IsOrd y ω-mem-ord y y∈ω = PT.rec (isPropIsOrd y) (λ { (k , #k≡y) → subst IsOrd #k≡y (numeral-ord (lower k)) }) y∈ω ``` Assembling the halves gives `ω-ord : IsOrd ω`. Its first component, `trans-ω`, establishes `isTransV ω`: from `y ∈ x ∈ ω`, the hypothesis on `x` merely presents an index `k` with `# k ≡ x`, and after transporting along that path, `numeral-mem` places `y` in `ω`. This elimination goes into a proposition-valued target, which is what licenses removing the truncation. ```agda ω-ord : IsOrd ω ω-ord = trans-ω , (λ x x∈ω → ω-mem-ord x x∈ω .fst) where trans-ω : isTransV ω ``` For each member `x` of `ω`, `ω-mem-ord x x∈ω` proves `IsOrd x`; its first component is the transitivity of `x` required by the second component of `IsOrd ω`. Together the two components yield `IsOrd ω`. ```agda trans-ω {x} {y} y∈x x∈ω = PT.rec (snd (y ∈ˢ ω)) (λ { (k , #k≡x) → numeral-mem (lower k) y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym #k≡x) y∈x) }) x∈ω ``` ## What lies below a numeral The numerals are not merely ordinals, they are *counted* by ordinals: the members of the numeral for `n` are exactly the numerals for the smaller naturals. The first half of that, elimination, is one induction with the successor eliminator; the second half, that a numeral belonging to a numeral means the indices compare, follows by injectivity. The coding chapters will use these to read an index out of a set, which is what a bound on a variable ultimately means. The elimination lemma states that a member `z` of `# n` merely comes from a smaller index: there merely exists `m < n` with `z ≡ # m`. The statement lands in a propositional truncation on purpose. The proof does not choose a witness from the truncation; it uses only the proposition that some such decomposition exists. The base case is vacuous, since membership in the empty set is contradictory. ```agda ∈#-elim : (n : ℕ) (z : S) → ⟨ z ∈ˢ (# n) ⟩ → ∥ Σ[ m ∈ ℕ ] ((m < n) × (z ≡ # m)) ∥₁ ∈#-elim zero z h = Empty.rec (∅-empty z (∈∈ₛ {a = z} {b = ∅} .fst h)) ∈#-elim (suc n) z h = ∈sucV-elim {A = # n} {x = z} {P = ∥ Σ[ m ∈ ℕ ] ((m < suc n) × (z ≡ # m)) ∥₁} squash₁ h ``` In the successor case the eliminator for `sucV` splits membership in `# (suc n)` into two branches. If `z` lies in `# n`, the induction hypothesis gives `m < n` with `z ≡ # m`, and `≤-suc` lifts that to `m < suc n`. If `z` equals `# n` itself, the witness is `n` itself, with the strict inequality witnessed by `0` and `refl`. For the companion statement `#∈#-elim`, apply this to `z = # a` in `# b`: a truncated triple results, whose equation `# a ≡ # m` the injectivity lemma `#-inj′` turns into `a ≡ m`, and transporting along that identification converts `m < b` into the claimed `a < b`. ```agda (λ z∈#n → PT.map (λ { (m , p , e) → m , ≤-suc p , e }) (∈#-elim n z z∈#n)) (λ e → ∣ n , (0 , refl) , e ∣₁) #∈#-elim : (a b : ℕ) → ⟨ (# a) ∈ˢ (# b) ⟩ → a < b #∈#-elim a b h = PT.rec isProp≤ (λ { (m , p , e) → subst (_< b) (sym (#-inj′ e)) p }) ``` The final step is the elimination of the truncation itself. The strict order on ℕ is proposition-valued, by `isProp≤`, so eliminating into `a < b` is legitimate; the conclusion needs only that *some* witnessing index works, not a canonical one. ```agda (∈#-elim b (# a) h) ``` ## Recap Zero, successors and small unions of ordinals are ordinals, and `boundingOrd` bounds any small family by a single ordinal. The bound converts pointwise ordinal bounds for any small family into one strict common bound. Later chapters use these results independently: the ZF axiom proofs use ordinal bounds to collect stages, while the finite-ordinal lemmas and `ω-ord` support the treatment of infinity and later coding arguments.