Ordinals

The tower of the previous chapter is indexed by ordinals, and so far the book has needed exactly one fact about them: that being one is a proposition. The constructions ahead need more. Every closure argument for the constructible universe has the same shape: a set is built from ingredients that live at various stages, and the argument must place the result at a single stage. So what the axioms need from ordinals is not a theory of order, but a supply of upper bounds.

This chapter provides exactly that supply, and nothing else. Zero is an ordinal; successors of ordinals are ordinals; a union of ordinals is an ordinal; and, the chapter's deliverable, every small family of ordinals lies below a single ordinal. That last statement is what turns "each ingredient has some stage" into "all of them share one stage", which is the move every closure proof in the next chapter makes.

Notably absent is comparison. One expects ordinals to be linearly ordered, and they are, but that fact is not constructive and it is not needed here: a common bound is cheaper than a comparison, and it is all the axioms ask for. The book takes the cheaper road, and the basic axioms of the constructible universe cost no classical logic as a result.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth

module L.Ordinal {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( #-inj′ )
open import L.Constructible {ℓ}
  using ( isTransV; isPropIsTransV; ∅-trans; setUnion-trans; IsOrd; isPropIsOrd )

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 )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⋃_; union-ax; module InfinitySet )
open InfinitySet using ( sucV; #_; ω; #-in-ω )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
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.

∅-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, and the hierarchy chapter left the tool for reasoning about it: a member of sucV A is either a member of A or A itself, and that case split is a proposition-level eliminator. Both halves of the ordinal predicate follow it. For transitivity, a member of a member of sucV A lands back in A either by A's transitivity or, in the degenerate branch, immediately; for the second half, the members of sucV A are members of A (transitive by assumption) or A itself (transitive by assumption again).

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

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
  memTr z z∈⋃ = PT.rec (isPropIsTransV z)
    (λ { (w , (w∈ₛsett , z∈ₛw)) → PT.rec (isPropIsTransV z)
        (λ { (x , fx≡w) → hf x .snd z
               (∈∈ₛ {a = z} {b = f x} .snd
                 (subst (λ W → ⟨ z ∈ₛ W ⟩) (sym fx≡w) z∈ₛw)) })
        (∈∈ₛ {a = w} {b = sett X f} .snd w∈ₛsett) })
    (union-ax (sett X f) z .fst (∈∈ₛ {a = z} {b = ⋃ (sett X f)} .fst 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. Then f x belongs to sucV (f x), which belongs to the family being unioned, so f x belongs to the union, which is what the closure arguments need. The result is a genuine pair, not a truncated existence: the consumers name the bound and form its stage.

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
  g x = sucV (f x)
  β : S
  β = ⋃ (sett X g)
  ordβ : IsOrd β
  ordβ = setUnion-ord X g (λ x → suc-ord (hf x))
  memβ : (x : X) → ⟨ f x ∈ˢ β ⟩
  memβ x = ∈∈ₛ {a = f x} {b = β} .snd
    (union-ax (sett X g) (f x) .snd
      ∣ sucV (f x) , (s∈ₛsett , fx∈ₛs) ∣₁)
    where
    s∈ₛsett : ⟨ sucV (f x) ∈ₛ sett X g ⟩
    s∈ₛsett = ∈∈ₛ {a = sucV (f x)} {b = sett X g} .fst ∣ x , refl ∣₁
    fx∈ₛs : ⟨ f x ∈ₛ sucV (f x) ⟩
    fx∈ₛs = ∈∈ₛ {a = f x} {b = sucV (f x)} .fst (self∈sucV (f x))

The two-element case is worth naming, because it is the one that gets used most: merging two ordinals into one that contains 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.

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
  f : Lift {ℓ-zero} {ℓ} Bool → S
  f (lift true)  = σ₁
  f (lift false) = σ₂
  fo : (b : Lift {ℓ-zero} {ℓ} Bool) → IsOrd (f b)
  fo (lift true)  = o₁
  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.

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, one induction deep. Their limit ω is an ordinal too, and that is the fact the collection step will need. Its second half is free from the numerals; 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.

numeral-ord : (n : ℕ) → IsOrd (# n)
numeral-ord zero    = ∅-ord
numeral-ord (suc n) = suc-ord (numeral-ord n)

#∈ω : (k : ℕ) → ⟨ (# k) ∈ˢ ω ⟩
#∈ω k = ∈∈ₛ {a = # k} {b = ω} .snd (#-in-ω k)

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)
  (λ 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∈ω

ω-ord : IsOrd ω
ω-ord = trans-ω , (λ x x∈ω → ω-mem-ord x x∈ω .fst)
  where
  trans-ω : isTransV ω
  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.

∈#-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
  (λ 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 })
  (∈#-elim b (# a) h)

Recap

Zero, successors and small unions of ordinals are ordinals, and

boundingOrd bounds any small family by a single ordinal. That last result is the chapter's whole purpose: it is how "each of finitely many ingredients lives at some stage" becomes "all of them live at one stage", and the next chapter spends it three times over, once for each of the first closure axioms. Downward closure, the absence of self-membership, and ω itself as an ordinal are the same theory continued; they wait here for the collection step of infinity, which is what first needs them.