Von Neumann rank

The rank of a set is the union, over its members, of the successors of their ranks; in symbols, the computation theorem rank-compute identifies rank x with rankStep x (λ y _ → rank y). Four facts about it are proved in this chapter: rank-mono says that rank strictly increases along membership, rank-ord says that rank is always an ordinal, rank-upper gives a conditional inclusion of a rank into an ordinal, and rank-fix says that rank fixes ordinals.

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 directly guarantees. Thus every theorem in this chapter is proved without an excluded-middle parameter.

Rank is defined inside the cumulative hierarchy V ℓ, with carrier S. A membership statement x ∈ˢ y is proposition-valued, and regularity makes this membership relation well-founded. The induction principle ∈-induction can therefore define a value in S from values already defined for every member.

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

open import Base.Prelude

module L.Rank {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

For rank, the value at a set must collect the successor ranks of all its members. The operations sucV and small indexed union express this construction. Once the recursive member ranks are known to be ordinals, suc-ord and setUnion-ord show that the collected value is again an ordinal; mem-ord later supplies ordinality for members of an ordinal.

open import V.Hierarchy {ℓ}
  using ( 𝒮ᵥ; extensionalV; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( union-family-in; union-family-out; ∈sucV-elim; self∈sucV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( suc-ord; setUnion-ord; mem-ord )

The indexing is genuinely small. Each set x has a small member type ⟪ x ⟫ and an embedding ⟪ x ⟫↪ into S; ∈ₛ⟪ x ⟫↪ m proves that the represented set belongs to x. Conversely, a given membership proof can be converted by ∈-asFiber into an index together with a path identifying its represented set with the member. These two directions connect recursion over membership with the small family used by the union.

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

The recursive step can now be read mathematically: take the small family of members, replace each member by the successor of its recursively computed rank, and form their union. The next section states this construction as rankStep and records its computation path.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ᵥ

The recursion

The step takes the union, over the members of x, of the successors of their ranks. The recursive calls run over the small type of members, and the computation law holds propositionally as a path rather than definitionally, which is what later proofs use.

The recursion equation says: to rank a set x, rank every member and take the union of the successors. Formally, the family being unioned is indexed by ⟪ x ⟫, the small type of members, so the expression ⋃ (sett ⟪ x ⟫ …) is a legal small union; the embedding ⟪ x ⟫↪ turns an index m into the actual set ⟪ x ⟫↪ m, and the helper mem supplies the proof that this embedded set really is a member of x, which is what the recursive call rec demands. Note the shape of the step: it receives the recursive values through a function rec rather than calling rank directly, which is what makes it usable as the step of ∈-induction.

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)

The rank itself is the membership induction applied to this step: ∈-induction rankStep turns the step function into a total family on all of S. The definition is marked opaque to keep the checker from unfolding the well-founded eliminator inside it. What is available instead is the computation law rank-compute, which exposes the recursion equation as a propositional path: rank x is a path to rankStep x (λ y _ → rank y), the same equation with rank itself filling every recursive call. Later proofs rewrite by this path rather than reducing rank directly.

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 theorem rank-mono states that if x ∈ˢ y then rank x ∈ˢ rank y. It follows directly from the shape of the defining union: rank y is a union of successors sucV (rank w) indexed by the members w of y, so exhibiting rank x as a member of one such successor suffices. No IsOrd hypothesis appears anywhere in the statement.

Given x ∈ˢ y, the goal is rank x ∈ˢ rank y. Unfold rank y once by rank-compute: the goal becomes membership in the union ⋃ (sett ⟪ y ⟫ (λ m → sucV (rank (⟪ y ⟫↪ m)))). Now it suffices to exhibit rank x as a member of one family member, namely sucV (rank w) for some member w of y; self∈sucV puts rank x inside its own successor, and union-family-in lifts that into the union, transport along the computation path included.

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))
  (union-family-in ⟪ y ⟫ (λ m → sucV (rank (⟪ y ⟫↪ m))) (fib .fst) (rank x)
    (subst (λ w → ⟨ rank x ∈ˢ sucV (rank w) ⟩) (sym (fib .snd)) (self∈sucV (rank x))))
  where

The remaining piece is where the index for the union member comes from. The function ∈-asFiber turns the given proof x∈y into a fiber of the embedding ⟪ y ⟫↪: a pair whose first component fib .fst is an index into ⟪ y ⟫, and whose second component fib .snd is a path saying that the indexed set equals x. That path is transported along so that the membership in the successor speaks of rank x itself; this is exactly what the code shows.

  fib = ∈-asFiber {a = x} {b = y} x∈y

Rank is an ordinal

One membership induction. Unfold once by rank-compute; the inductive hypothesis makes each member's rank an ordinal, the closure lemma suc-ord makes each successor an ordinal, and the closure lemma setUnion-ord makes the union of that family of ordinals an ordinal again.

The statement quantifies over all sets, so the proof is a membership induction with the predicate λ A → IsOrd (rank A). The induction hypothesis hands us, for each member y of A, the certificate that rank y is an ordinal. Since rank-compute A propositionally identifies rank A with the step, the goal is reached by transporting IsOrd along the computation path rank-compute A, so what remains is to show that the union of the step is 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))

That last step composes two closure facts. Each family member sucV (rank (⟪ A ⟫↪ m)) is the successor of an ordinal, hence an ordinal by suc-ord, with the induction hypothesis and the helper mem supplying the input certificate. Then setUnion-ord closes the small indexed union of ordinals under union. The chain from hypothesis to conclusion: if the ranks of the members are ordinals, so is the rank of the set.

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

Bounding a rank

If every member's rank lies in an ordinal, the rank of the set is included in that ordinal. Every member of the defining union lies in a successor of a member's rank; transitivity closes the inclusion. Both ordinal fixed points and bounds on the ranks in a constructible stage use this argument.

The statement is a pointwise inclusion, not a strict membership: assuming IsOrd β and that every member rank rank y lies strictly in β, it concludes that every member of rank A lies in β. The proof eliminates from the shape of the defining union. Membership in the union yields, via union-family-out, merely an index m with x ∈ˢ s m; since the target x ∈ˢ β is a proposition, eliminating this truncation is legitimate, and ∈sucV-elim then splits membership in the successor s m = sucV (rank (⟪ A ⟫↪ m)) into its two cases.

rank-upper : (A β : S) → IsOrd β
           → ((y : S) → ⟨ y ∈ˢ A ⟩ → ⟨ rank y ∈ˢ β ⟩)
           → (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ β ⟩
rank-upper A β oβ bound x hx = PT.rec (snd (x ∈ˢ β))
  (λ { (m , hm) → ∈sucV-elim (snd (x ∈ˢ β)) hm

The two cases of the successor are where ordinality earns its keep. If x is a member of rank (⟪ A ⟫↪ m), then since β is transitive and that rank is already in β, so is x: this is the branch oβ .fst h (below m). If instead x equals rank (⟪ A ⟫↪ m) outright, the second branch transports the bound below m across that path. Either way the conclusion lands in x ∈ˢ β. What the eliminator receives from the union is hm : ⟨ x ∈ˢ s m ⟩ merely, so the fiber (m , hm) is consumed inside a propositional elimination and no index is ever extracted as data.

    (λ h → oβ .fst h (below m))
    (λ q → subst (λ w → ⟨ w ∈ˢ β ⟩) (sym q) (below m)) })
  (union-family-out ⟪ A ⟫ s x
    (subst (λ w → ⟨ x ∈ˢ w ⟩) (rank-compute A) hx))
  where

The family s is the successor-rank family from the recursion equation, sending an index m to sucV (rank (⟪ A ⟫↪ m)). The fact below m is the hypothesis bound applied to the embedded member ⟪ A ⟫↪ m together with its membership proof, yielding rank (⟪ A ⟫↪ m) ∈ˢ β. The whole lemma therefore uses no induction: rewrite by the computation law, take the union apart, and let the ordinal's transitivity absorb the successor.

  s : ⟪ A ⟫ → S
  s m = sucV (rank (⟪ A ⟫↪ m))
  below : (m : ⟪ A ⟫) → ⟨ rank (⟪ A ⟫↪ m) ∈ˢ β ⟩
  below m = bound (⟪ A ⟫↪ 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 theorem states that rank fixes every ordinal, as a path rather than an iff. The induction is set up with a predicate that packages the ordinality hypothesis together with the conclusion, λ A → IsOrd A → rank A ≡ A, because the step genuinely needs it: to compare rank A with A it must know that members of the ordinal A are themselves ordinals. So the step receives, alongside the recursive equalities rank y ≡ y, the certificate IsOrd A and returns the equality at A.

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

The equality itself comes from extensionalV, which turns a pointwise equivalence of membership into a path of sets, and ⇔toPath packages the two directions. the two sets being compared stay folded. The forward direction toA is none other than rank-upper at β = A: the ordinal bound on member ranks is A itself, and the bounding hypothesis is produced on the fly from the induction hypothesis.

  step A IH ordA = extensionalV (λ x → ⇔toPath (toA x) (fromA x))
    where
    toA : (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ A ⟩
    toA = rank-upper A A ordA
      (λ y hy → subst (λ w → ⟨ w ∈ˢ A ⟩)

Both bounding directions lean on the same fact, mem-ord: a member of the ordinal A is again an ordinal, so the induction hypothesis applies to it. For toA, the hypothesis required by rank-upper is rank y ∈ˢ A; since rank y ≡ y by IH and y ∈ˢ A is given, the transport lands it. For fromA, the reverse holds: rank-mono x A x∈A gives rank x ∈ˢ rank A, and the path rank x ≡ x from the IH transports it to x ∈ˢ rank A. Every ingredient is now in place, and the path rank A ≡ A follows.

        (sym (IH y hy (mem-ord {A = A} ordA y hy))) hy)

    fromA : (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ rank A ⟩
    fromA x x∈A = subst (λ w → ⟨ w ∈ˢ rank A ⟩)
      (IH x x∈A (mem-ord {A = A} ordA x x∈A)) (rank-mono x A x∈A)

Recap

rank measures every set by an ordinal (rank-ord) and fixes the ordinals themselves (rank-fix), which show that it is an ordinal-valued measure agreeing with each ordinal. Both proofs are membership inductions on regularity, so the chapter uses no additional assumptions. It gives a strict ordinal-valued measure of membership and the fixed-point law needed when the measured set is already an ordinal.