---
title: "Ordinals are linearly ordered by membership"
module: L.Ordinal.Linear
lang: en
site: "Bedrock"
description: "Ordinals are linearly ordered by membership"
stage: "Constructible stages and the axioms"
reading_order: 28
canonical: https://bedrock.institute/en/L.Ordinal.Linear.html
html: L.Ordinal.Linear.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal/Linear.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal]
routes: [constructible-axioms]
translations: [https://bedrock.institute/zh/L.Ordinal.Linear.md, https://bedrock.institute/ja/L.Ordinal.Linear.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

```agda
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.

```agda
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.

```agda
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`.

```agda
_⊆ᵇ_ : 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.

```agda
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.

```agda
¬⊆ᵇ→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".

```agda
  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.

```agda
    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.

```agda
      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.

```agda
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.

```agda
  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.

```agda
    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`.

```agda
      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.

```agda
        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.

```agda
        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`.

```agda
      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.

```agda
      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.