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.

{-# 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.

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.

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.

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.

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.

∅-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.

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.

    (λ 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.

    (λ 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.

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.

  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.

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.

  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.

  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.

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.

  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.

  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.

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.

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 ∈ˢ ω ⟩.

#∈ω : (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.

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.

  (λ 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.

ω-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 ω.

  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.

∈#-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.

  (λ z∈#n → PT.map (λ { (m , p , e) → m , ≤-suc p , e }) (∈#-elim n z z∈#n))
  (λ e → ∣ n , ( , 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.

  (∈#-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.