Rank

Every set has a rank: the least stage of the cumulative hierarchy at which it appears, measured in ordinals. The definition is one of the oldest in set theory and reads as a recursion on membership: the rank of x is the least ordinal above the ranks of all members of x, which is the union of their successors.

Two facts about it carry this part of the book. The rank of any set is an ordinal, so rank really is a measurement in ordinals; and an ordinal is its own rank, so rank is the canonical ordinal index rather than a second, parallel numbering. The second fact is what lets a question about stages be turned into a question about ranks and back again, and the collection step of infinity is exactly such a question.

A remark on how the recursion is set up, because it is the same trick the tower used. Nothing here needs an external type of ordinals: rank takes values in the hierarchy itself, and the recursion runs on well-founded membership, which regularity supplied for free. So the whole chapter is constructive, and the classical assumption that the next chapter introduces is not needed for any of it.

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

open import Base.Prelude
open import Base.Truth

module L.Rank {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ}
  using ( 𝒮ᵥ; extensionalV; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( suc-ord; setUnion-ord; mem-ord )

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; union-ax; module InfinitySet )
open InfinitySet using ( sucV )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

The recursion

The step takes the union, over the members of x, of the successors of their ranks. As with the tower, the recursive calls run over the small type of members, and the computation rule holds propositionally rather than definitionally, which is all any later proof asks of it.

The rank itself is sealed, for the same reason the tower is: it unfolds to an accessibility eliminator, and any goal that mentions the rank of a set built by nesting, a pair inside a pair inside a pair, drags that eliminator through normalization. Measured, on a goal four constructions deep: 163 seconds without the seal, 1.4 with. rank-compute is the official unfolding and lives inside the seal, so nothing downstream loses anything.

rankStep : (x : S) → (∀ y → y ∈ᵗ x → S) → S
rankStep x rec = ⋃ (sett ⟪ x ⟫ (λ m → sucV (rec (⟪ x ⟫↪ m) (mem m))))
  where
  mem : (m : ⟪ x ⟫) → ⟪ x ⟫↪ m ∈ᵗ x
  mem m = ∈∈ₛ {a = ⟪ x ⟫↪ m} {b = x} .snd (∈ₛ⟪ x ⟫↪ m)

opaque
  rank : S → S
  rank = ∈-induction rankStep

  rank-compute : (x : S) → rank x ≡ rankStep x (λ y _ → rank y)
  rank-compute = ∈-induction-compute rankStep

Rank strictly increases along membership

The one fact that makes rank a descent measure. It is the outward half of the fixed-point argument below with the ordinality hypothesis dropped: the same union witness, no IsOrd anywhere. A recursion that must descend into a set built by nesting, rather than into a member, has no membership to induct on and uses this instead.

rank-mono : (x y : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank x ∈ˢ rank y ⟩
rank-mono x y x∈y = subst (λ w → ⟨ rank x ∈ˢ w ⟩) (sym (rank-compute y))
  (∈∈ₛ {a = rank x} {b = ⋃ (sett ⟪ y ⟫ s)} .snd
    (union-ax (sett ⟪ y ⟫ s) (rank x) .snd
      ∣ sucV (rank (⟪ y ⟫↪ m)) , (sm∈ₛsett , x∈ₛsm) ∣₁))
  where
  s : ⟪ y ⟫ → S
  s k = sucV (rank (⟪ y ⟫↪ k))
  fibx = ∈-asFiber {a = x} {b = y} x∈y
  m = fibx .fst
  q : ⟪ y ⟫↪ m ≡ x
  q = fibx .snd
  sm∈ₛsett : ⟨ sucV (rank (⟪ y ⟫↪ m)) ∈ₛ sett ⟪ y ⟫ s ⟩
  sm∈ₛsett = ∈∈ₛ {a = sucV (rank (⟪ y ⟫↪ m))} {b = sett ⟪ y ⟫ s} .fst ∣ m , refl ∣₁
  x∈ₛsm : ⟨ rank x ∈ₛ sucV (rank (⟪ y ⟫↪ m)) ⟩
  x∈ₛsm = ∈∈ₛ {a = rank x} {b = sucV (rank (⟪ y ⟫↪ m))} .fst
    (subst (λ w → ⟨ rank x ∈ˢ sucV (rank w) ⟩) (sym q) (self∈sucV (rank x)))

Rank is an ordinal

One membership induction. Unfold once; the inductive hypothesis makes each member's rank an ordinal, successors of ordinals are ordinals, and the previous chapter's closure under small unions collects the family back into an ordinal.

rank-ord : (A : S) → IsOrd (rank A)
rank-ord = ∈-induction {P = λ A → IsOrd (rank A)} step
  where
  step : (A : S) → (∀ y → y ∈ᵗ A → IsOrd (rank y)) → IsOrd (rank A)
  step A IH = subst IsOrd (sym (rank-compute A))
    (setUnion-ord ⟪ A ⟫ (λ m → sucV (rank (⟪ A ⟫↪ m)))
      (λ m → suc-ord (IH (⟪ A ⟫↪ m) (mem m))))
    where
    mem : (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ∈ᵗ A
    mem m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)

Ordinals are their own rank

Again by membership induction, and this time the proof is an extensionality between rank A and A. Left to right, an element of rank A sits inside the successor of the rank of some member, and that rank is the member by the inductive hypothesis, so the element is the member or belongs to it, and either way it belongs to A by transitivity. Right to left, a member of A is the rank of itself, hence belongs to the successor of that rank, which is one branch of the union.

The shape of the argument is worth one remark: extensionality is applied to rank A and A directly, both of them neutral terms, and the nested union is only ever reached through the computation rule as a path. Feeding the unfolded union to extensionality instead would force the checker to normalize a deeply nested set expression, which is the standard way these proofs become uncheckable.

rank-fix : (A : S) → IsOrd A → rank A ≡ A
rank-fix = ∈-induction {P = λ A → IsOrd A → rank A ≡ A} step
  where
  step : (A : S) → (∀ y → y ∈ᵗ A → IsOrd y → rank y ≡ y)
       → IsOrd A → rank A ≡ A
  step A IH ordA = extensionalV (λ x → ⇔toPath (toA x) (fromA x))
    where
    s : ⟪ A ⟫ → S
    s m = sucV (rank (⟪ A ⟫↪ m))
    mem : (m : ⟪ A ⟫) → ⟨ ⟪ A ⟫↪ m ∈ˢ A ⟩
    mem m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)
    rk : (m : ⟪ A ⟫) → rank (⟪ A ⟫↪ m) ≡ ⟪ A ⟫↪ m
    rk m = IH (⟪ A ⟫↪ m) (mem m) (mem-ord {A = A} ordA (⟪ A ⟫↪ m) (mem m))

    toA : (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ A ⟩
    toA x x∈r = PT.rec (snd (x ∈ˢ A))
      (λ { (v , (v∈ₛsett , x∈ₛv)) → PT.rec (snd (x ∈ˢ A))
          (λ { (m , sm≡v) →
              ∈sucV-elim (snd (x ∈ˢ A))
                (∈∈ₛ {a = x} {b = sucV (rank (⟪ A ⟫↪ m))} .snd
                  (subst (λ w → ⟨ x ∈ₛ w ⟩) (sym sm≡v) x∈ₛv))
                (λ x∈rm → ordA .fst (subst (λ w → ⟨ x ∈ˢ w ⟩) (rk m) x∈rm) (mem m))
                (λ x≡rm → subst (λ w → ⟨ w ∈ˢ A ⟩) (sym (x≡rm ∙ rk m)) (mem m)) })
          (∈∈ₛ {a = v} {b = sett ⟪ A ⟫ s} .snd v∈ₛsett) })
      (union-ax (sett ⟪ A ⟫ s) x .fst
        (∈∈ₛ {a = x} {b = ⋃ (sett ⟪ A ⟫ s)} .fst
          (subst (λ w → ⟨ x ∈ˢ w ⟩) (rank-compute A) x∈r)))

    fromA : (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ rank A ⟩
    fromA x x∈A = subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (rank-compute A))
      (∈∈ₛ {a = x} {b = ⋃ (sett ⟪ A ⟫ s)} .snd
        (union-ax (sett ⟪ A ⟫ s) x .snd
          ∣ sucV (rank (⟪ A ⟫↪ m)) , (sm∈ₛsett , x∈ₛsm) ∣₁))
      where
      fibx = ∈-asFiber {a = x} {b = A} x∈A
      m = fibx .fst
      q : ⟪ A ⟫↪ m ≡ x
      q = fibx .snd
      sm∈ₛsett : ⟨ sucV (rank (⟪ A ⟫↪ m)) ∈ₛ sett ⟪ A ⟫ s ⟩
      sm∈ₛsett = ∈∈ₛ {a = sucV (rank (⟪ A ⟫↪ m))} {b = sett ⟪ A ⟫ s} .fst
        ∣ m , refl ∣₁
      x∈ₛsm : ⟨ x ∈ₛ sucV (rank (⟪ A ⟫↪ m)) ⟩
      x∈ₛsm = ∈∈ₛ {a = x} {b = sucV (rank (⟪ A ⟫↪ m))} .fst
        (subst (λ w → ⟨ w ∈ˢ sucV (rank (⟪ A ⟫↪ m)) ⟩) (rk m ∙ q)
          (self∈sucV (rank (⟪ A ⟫↪ m))))

Recap

rank measures every set by an ordinal (rank-ord) and fixes the ordinals themselves (rank-fix), which together certify it as the canonical index. Both proofs are membership inductions on regularity, so the chapter costs nothing in assumptions. What it buys is the ability to ask "how far up does this set appear" and get an ordinal answer, and the next two chapters spend that on the one remaining question about the tower: which ordinals appear at which stage.