Ordinals are linearly ordered by membership

Of any two ordinals, one belongs to the other or the two are equal. This chapter isolates the classical step needed for that comparison and explains why it requires an explicit hypothesis.

Everything about ordinals up to now has been closure: zero is one, successors are, unions are, bounds exist. Closure statements build; they never have to decide anything. Trichotomy decides. Given two ordinals with no relation assumed between them, it returns one of the three comparison cases, and this chapter obtains that decision from its explicit excluded-middle parameter. So the chapter takes the excluded middle as a module parameter, using the level-indexed packaging fixed in the foundations, and modules that use ord-tri receive that parameter explicitly.

Two ingredients from the ambient hierarchy make the proof shorter than the textbook version. Regularity gives a well-founded induction, used twice over, once in each argument. Extensionality means that mutual inclusion is equality, so the equal case needs no separate work. Excluded middle decides the two inclusions and the membership propositions used to turn a failed inclusion into a truncated counterexample.

The chapter runs under a single classical hypothesis, stated once as a module parameter: an instance of LEM (ℓ-suc ℓ). Recall its shape from the foundations: for each proposition P : hProp (ℓ-suc ℓ), it returns either a proof of ⟨ P ⟩ or a refutation, a map from ⟨ P ⟩ into the empty type. This level matches ⊆ᵇ-prop A B : hProp (ℓ-suc ℓ) and the membership propositions decided inside the counterexample argument. Keeping the assumption as an explicit module parameter records the classical input at each use of this module.

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Ordinal.Linear {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The proof works directly in the ambient hierarchy V rather than through the object language. The carrier and the structure membership ∈ˢ come from the ZF structure packaged over 𝒮ᵥ, so ⟨ x ∈ˢ A ⟩ is the underlying proposition of an hProp truth value. Two principles of V carry the mathematical weight: extensionalV, which converts a family of membership biconditionals into a path of equality, and regularityV, which makes membership well-founded and thus supports induction on it. The remaining import from the L-side, mem-ord, matters at every recursive call: it shows that any member of an ordinal is itself an ordinal, which is what lets the induction hypothesis apply below.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

The decision procedure returns which of three cases holds, so the return type is built from a three-way sum: membership on the left, equality in the middle, membership on the right. Also needed is the conversion from an iff to a path, which the extensionality argument will apply to each point of the carrier. The empty type plays the role of refutation throughout: to refute a proposition is to map it into something with no inhabitants.

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
import Cubical.Induction.WellFounded as WF

Two final conventions are opened for the whole file. The direct operations on hProp supply the propositional connectives used inside membership statements, and the structure vocabulary fixes S as the carrier and ∈ˢ as its membership, so the code reads as set theory rather than as logic plumbing. These conventions let the proof track membership, equality, and well-founded recursion for ordinal elements directly.

open hPropStructure 𝒮ᵥ

Inclusion, and what fails it

The proof pivots on one relation: pointwise inclusion. If it holds both ways, extensionality makes the two ordinals equal; if it fails in one direction, excluded middle supplies a truncated member witnessing the failure; well-founded induction and transitivity then turn that counterexample into a strict comparison. This subsection fixes the relation and its packaging. Note what the level arithmetic already says: inclusion lives at Type (ℓ-suc ℓ), which is precisely where the supplied instance of excluded middle can decide it.

Inclusion of A in B is not a primitive here but a defined notion: every member x of A, in the structure sense, must be a member of B. Each membership x ∈ˢ A is an hProp proposition, so the definition quantifies over the carrier S and over propositions at level ℓ, which places the whole relation in Type (ℓ-suc ℓ). The matching hProp packaging attaches the propositionhood proof: a dependent function into a proposition is again a proposition, applied twice to the two nested function types. This matters because the excluded middle is decided per hProp, and it is exactly this packaged statement that the proof will hand to lem.

_⊆ᵇ_ : S → S → Type (ℓ-suc ℓ)
A ⊆ᵇ B = (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ B ⟩

⊆ᵇ-prop : (A B : S) → hProp (ℓ-suc ℓ)
⊆ᵇ-prop A B = (A ⊆ᵇ B) , isPropΠ (λ x → isPropΠ (λ _ → snd (x ∈ˢ B)))

ext-⊆ᵇ : {A B : S} → A ⊆ᵇ B → B ⊆ᵇ A → A ≡ B

The equal case of trichotomy comes for free from extensionality of the hierarchy. Given inclusions both ways, each point x of the carrier yields an iff between ⟨ x ∈ˢ A ⟩ and ⟨ x ∈ˢ B ⟩; ⇔toPath turns that iff into a path, and extensionalV assembles the family of paths into the equality A ≡ B. No classical input is used here at all: extensionality is a theorem of V itself.

ext-⊆ᵇ {A} {B} s₁ s₂ = extensionalV (λ x → ⇔toPath (s₁ x) (s₂ x))

Here is the one genuinely classical step. From a failure of inclusion the proof needs a member witnessing it, and passing from "not every member of B lies in A" to "some member does not" is not constructive. Excluded middle decides the existence statement directly: were there no such witness, then each member of B could be shown to lie in A, one decided membership at a time, contradicting the assumed failure. The witness that comes out remains propositionally truncated, and that is enough, because the only thing the trichotomy proof will do with it is eliminate it into a membership proposition.

The statement is a conditional: if inclusion A ⊆ᵇ B is refutable, then a truncated witness exists, a member a of A with a ∉ B. The conclusion is deliberately an existence claim under ∥ ∥₁ rather than a chosen pair. The first classical move decides the truncated existence statement Witness itself. Note the level bookkeeping: the witness statement is an hProp at ℓ-suc ℓ, exactly where the module's lem applies, so no lifting is needed. In the positive branch the witness is already in hand; the interesting branch is the negative one.

¬⊆ᵇ→witness : (A B : S) → (A ⊆ᵇ B → Empty.⊥)
            → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
¬⊆ᵇ→witness A B ¬sub = decide (lem Witness)
  where
  Witness : hProp (ℓ-suc ℓ)

Suppose Witness is refutable. Then the refutation of inclusion can itself be refuted: for arbitrary x, we decide the membership x ∈ˢ B separately, and on the negative branch assemble the witness x with x ∈ˢ A and the refutation of x ∈ˢ B into an inhabitant of Witness, contradicting the given refutation. So inclusion holds after all, and feeding it to the assumed refutation of inclusion yields the empty type. This is exactly the pattern announced above: the single global decision on Witness plus a pointwise decision on each x ∈ˢ B together convert "no witness exists" into "inclusion holds".

  Witness = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
          , PT.isPropPropTrunc
  decide : ⟨ Witness ⟩ ⊎ (⟨ Witness ⟩ → Empty.⊥) → ⟨ Witness ⟩
  decide (inl wit)  = wit
  decide (inr ¬wit) = Empty.rec (¬sub sub)

The pointwise decision is worth pausing on, because it shows how a truncated conclusion tolerates a truncated input. To prove x ∈ˢ B from x ∈ˢ A, decide that single membership with lem. If it holds, done. If it fails, the refutation of x ∈ˢ B, together with x ∈ˢ A and x, is exactly the data of a witness, and its truncation ∣ x , (x∈A , ¬x∈B) ∣₁ is an inhabitant of Witness, contradicting the negative branch's hypothesis.

    where
    sub : A ⊆ᵇ B
    sub x x∈A = at (lem (x ∈ˢ B))
      where
      at : ⟨ x ∈ˢ B ⟩ ⊎ (⟨ x ∈ˢ B ⟩ → Empty.⊥) → ⟨ x ∈ˢ B ⟩

Assembling the pieces: the outer decision on Witness returns the truncated witness directly in the positive case, and in the negative case derives a contradiction from the assumed failure of inclusion. The helper ¬⊆ᵇ→witness is now available for both directions of the trichotomy argument, and it never promises more than a truncated witness. Keeping the truncation explicit is what makes the later elimination legal: propositional truncation may be eliminated only into propositions, and the membership statements the next subsection eliminates into are exactly that.

      at (inl x∈B)  = x∈B
      at (inr ¬x∈B) = Empty.rec (¬wit ∣ x , (x∈A , ¬x∈B) ∣₁)

Trichotomy

Everything is now in place for the main theorem. The comparison is stated as a three-way sum: either A is a member of B, or the two are equal by a path, or B is a member of A. The proof runs well-founded induction twice, once on each argument, so that at a leaf it may recurse into members of either ordinal. The two inclusions A ⊆ᵇ B and B ⊆ᵇ A are decided in each induction step by excluded middle; the previous subsection then does the rest. Note the direction bookkeeping that the reader should carry through the case analysis: failure of B ⊆ᵇ A produces a member of B outside A and concludes A ∈ˢ B, while failure of A ⊆ᵇ B produces a member of A outside B and concludes B ∈ˢ A.

The statement Tri A B packages the three possible answers in one type, built from nested sums. Its two outer cases are membership in the structure sense; the middle case is a path of equality. The type sits at Type (ℓ-suc ℓ), which is the level forced by the membership propositions inside it.

Tri : S → S → Type (ℓ-suc ℓ)
Tri A B = ⟨ A ∈ˢ B ⟩ ⊎ ((A ≡ B) ⊎ ⟨ B ∈ˢ A ⟩)

ord-tri : (A : S) → IsOrd A → (B : S) → IsOrd B → Tri A B
ord-tri = WF.WFI.induction regularityV {P = P} stepA
  where

The theorem's shape is a well-founded induction supplied by regularity. The predicate being proven, P A, says that A behaves correctly for every ordinal B it is compared with, taking the two ordinality certificates as hypotheses. Regularity thus provides induction on the first argument: to prove P A, it suffices to prove P A' for every member A' of A. This is the first of the two nested inductions; the second, on B, will appear inside the step.

  P : S → Type (ℓ-suc ℓ)
  P A = IsOrd A → (B : S) → IsOrd B → Tri A B

  stepA : (A : S) → (∀ A' → ⟨ A' ∈ˢ A ⟩ → P A') → P A
  stepA A IHA ordA =
    WF.WFI.induction regularityV {P = λ B → IsOrd B → Tri A B} stepB

The outer step receives the induction hypothesis for every member of A and immediately runs a second well-founded induction, this time on B, with its own predicate λ B → IsOrd B → Tri A B. At the inner leaf the two inclusions are decided by lem applied to the packaged propositions ⊆ᵇ-prop A B and ⊆ᵇ-prop B A. These two decisions begin the classical case analysis; the earlier helper also uses excluded middle to obtain a truncated counterexample from each failed inclusion.

    where
    stepB : (B : S) → (∀ B' → ⟨ B' ∈ˢ B ⟩ → IsOrd B' → Tri A B')
          → IsOrd B → Tri A B
    stepB B IHB ordB = decide (lem (⊆ᵇ-prop A B)) (lem (⊆ᵇ-prop B A))
      where

The first failure case supposes B ⊆ᵇ A fails, so a member b of B outside A is merely known to exist. The helper fromB shows what one such explicit pair would give: since b is a member of the ordinal B, mem-ord certifies that b is itself an ordinal, and the inner induction hypothesis IHB may compare A with b. Its first outcome is A ∈ˢ b; ordinal transitivity, the first component of IsOrd B, then lifts this through b ∈ˢ B to A ∈ˢ B.

      fromB : Σ[ b ∈ S ] (⟨ b ∈ˢ B ⟩ × (⟨ b ∈ˢ A ⟩ → Empty.⊥)) → ⟨ A ∈ˢ B ⟩
      fromB (b , (b∈B , ¬b∈A)) = at (IHB b b∈B (mem-ord {A = B} ordB b b∈B))
        where
        at : Tri A b → ⟨ A ∈ˢ B ⟩
        at (inl A∈b)       = ordB .fst A∈b b∈B

The other two outcomes of comparing A with b are handled in turn. If A ≡ b by a path, then transporting b ∈ˢ B backward along that path, which is what subst with sym does, yields A ∈ˢ B. And if b ∈ˢ A, the choice of b as outside A is contradicted directly. All three branches land in the same proposition ⟨ A ∈ˢ B ⟩, which is exactly why a merely existing witness suffices here: the truncated pair is eliminated into a proposition, never into data.

        at (inr (inl A≡b)) = subst (λ w → ⟨ w ∈ˢ B ⟩) (sym A≡b) b∈B
        at (inr (inr b∈A)) = Empty.rec (¬b∈A b∈A)

      fromA : Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) → ⟨ B ∈ˢ A ⟩
      fromA (a , (a∈A , ¬a∈B)) =
        at (IHA a a∈A (mem-ord {A = A} ordA a a∈A) B ordB)

The mirrored helper fromA covers the other failure: A ⊆ᵇ B fails, so some member a of A lies outside B. Now the outer induction hypothesis does the work, since it compares A's members and is applied at a. If a turns out to be in B, the choice of a is contradicted; if a ≡ B, transport gives B ∈ˢ A; and if B ∈ˢ a, transitivity of A lifts it through a ∈ˢ A. Note the asymmetry the mirror introduces: the equality branch transports a ∈ˢ A along the path rather than reversing it, because this time the compared pair sits the other way round.

        where
        at : Tri a B → ⟨ B ∈ˢ A ⟩
        at (inl a∈B)       = Empty.rec (¬a∈B a∈B)
        at (inr (inl a≡B)) = subst (λ w → ⟨ w ∈ˢ A ⟩) a≡B a∈A
        at (inr (inr B∈a)) = ordA .fst B∈a a∈A

With the two converters in hand, the four verdict combinations sort into the three answers. If both inclusions hold, mutual inclusion is equality by the previous subsection, and the middle answer is returned. If A ⊆ᵇ B holds but B ⊆ᵇ A fails, the truncated witness for the failure is eliminated with PT.rec, which is legal precisely because the target ⟨ A ∈ˢ B ⟩ is a proposition, its propositionhood supplied by the second component of the membership hProp. The result is the left answer A ∈ˢ B: this is the branch where failure of B ⊆ᵇ A concludes that A belongs to B.

      decide : (A ⊆ᵇ B) ⊎ ((A ⊆ᵇ B) → Empty.⊥)
             → (B ⊆ᵇ A) ⊎ ((B ⊆ᵇ A) → Empty.⊥) → Tri A B
      decide (inl A⊆B) (inl B⊆A) = inr (inl (ext-⊆ᵇ A⊆B B⊆A))
      decide (inl A⊆B) (inr ¬B⊆A) =
        inl (PT.rec (snd (A ∈ˢ B)) fromB (¬⊆ᵇ→witness B A ¬B⊆A))

The last combination covers failure of A ⊆ᵇ B, whatever the second verdict is, and the mirrored converter delivers B ∈ˢ A. Together with the two cases above, every leaf now returns an inhabitant of Tri A B, so the double induction closes and ord-tri stands as a theorem about arbitrary ordinals A and B. Later chapters on stage orders and on cardinals, for example L.GCH.CardinalSquareLaw, take it as their comparison primitive.

      decide (inr ¬A⊆B) _ =
        inr (inr (PT.rec (snd (B ∈ˢ A)) fromA (¬⊆ᵇ→witness A B ¬A⊆B)))

Recap

Together with the previously available irreflexivity of hierarchy membership and the transitivity contained in IsOrd, ord-tri now supplies comparison of any two ordinals. These comparison laws are the order-theoretic foundation for the stage monotonicity and cardinal arguments later in the book.

ord-tri compares any two ordinals, and the book supplies one instance of the excluded middle for it, taken as a module parameter. This is the boundary the groundwork was built to make auditable: nothing is postulated, and uses of ord-tri must supply the module’s excluded-middle parameter. The chapters that follow put the comparison to the question it was needed for: which ordinals appear at which stage of the constructible hierarchy.