Ordinals below a successor cardinal inject into its base

A successor cardinal is the first cardinal strictly beyond its base. Suppose δ is the successor cardinal of κ inside L. This chapter proves that every ordinal α ∈ δ admits an internal injection into κ. The proof combines well-founded induction with ordinal trichotomy. Excluded middle has two precise roles: it supplies the trichotomy of ordinals, and in the case κ ∈ α it turns the failure of cardinality into the mere existence of a smaller target.

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

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

module L.GCH.BelowSuccessorCardinal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Fix one universe level and an instance of excluded middle at the level of the propositions used by the hierarchy. The classical hypothesis is explicit and precisely leveled. It is used first through ordinal trichotomy and later through a direct decision of Ex; the remaining ingredients are structural facts about V, L, ordinals and internal injections.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )

The argument moves between two structures. The ambient hierarchy supplies well-founded membership and its irreflexivity. The constructible universe supplies the ordinal and cardinal predicates. Ordinal trichotomy compares the current ordinal with κ, while inclusion coding and transitivity compose the resulting internal injections.

open import L.Cardinal {ℓ} lem using ( InjL; SuccCardL; IsCardinalL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty

The exceptional branch produces only a truncated witness. Accordingly, the proof uses sums and the empty type to analyze a decision, propositional truncation to state mere existence, and well-founded induction to descend through membership. These logical forms match the conclusion InjL, which is itself propositionally truncated.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
import Cubical.Induction.WellFounded as WF

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

Write SV.S for the carrier of the ambient hierarchy. Membership induction takes place on this type: an element is a set of V, without yet carrying evidence that it belongs to L.

module SV = hPropStructure 𝒮ᵥ using ( S )

Write SL.S for the carrier of the constructible universe. Its elements are pairs consisting of an ambient set and a certificate of constructibility. The predicates SuccCardL, IsCardinalL and InjL concern elements of this carrier.

module SL = hPropStructure 𝒮ʟ using ( S )

Assume that δ is the successor cardinal of κ, and let α be an ordinal belonging to δ. The goal InjL α κ says merely that an internal injection from α to κ exists. This is the precise form of the familiar statement that every ordinal below the successor of κ has cardinality at most κ.

below-succ-injects :
    (κ δ : SL.S) → SuccCardL δ κ
  → (α : SL.S) → IsOrd (fst α) → ⟨ fst α ∈ˢ fst δ ⟩
  → InjL α κ

Well-founded induction is performed on the underlying set of α. The predicate P a restores exactly the data needed to regard an ambient set a as the ordinal under consideration: a constructibility certificate, ordinalhood, and membership in δ. Under those assumptions it asks for an internal injection from (a , la) to κ.

below-succ-injects κ δ (ordδ , _ , κ∈δ , least) α =
  WF.WFI.induction regularityV {P = P} step (fst α) (snd α)
  where
  P : SV.S → Type (ℓ-suc ℓ)
  P a = (la : ⟨ isL a ⟩) → IsOrd a → ⟨ a ∈ˢ fst δ ⟩ → InjL (a , la) κ

Because κ ∈ δ and δ is an ordinal, κ is itself an ordinal. The induction step may therefore apply ordinal trichotomy to a and the underlying set of κ. Its induction hypothesis is available at every member of a, which is exactly what the third trichotomy branch will require.

  ordκ : IsOrd (fst κ)
  ordκ = mem-ord {A = fst δ} ordδ (fst κ) κ∈δ

  step : (a : SV.S) → (∀ a' → ⟨ a' ∈ˢ a ⟩ → P a') → P a
  step a ih la orda a∈δ = go (ord-tri a orda (fst κ) ordκ)
    where

Pair the ambient set a with its certificate la to obtain the corresponding element α' of L. This keeps the well-founded induction on the simple carrier SV.S, while cardinality statements are made in their proper domain SL.S.

    α' : SL.S
    α' = a , la

Consider the branch κ ∈ a. If α' were an L-cardinal, the leastness clause of SuccCardL δ κ would place δ inside α'. Since a ∈ δ, this would give a ∈ a, contradicting the irreflexivity of membership. Thus α' cannot be a cardinal in this branch.

The type Ex states the relevant negation of cardinality positively: merely, there is some γ ∈ α' into which α' internally injects.

    not-card : ⟨ fst κ ∈ˢ a ⟩ → IsCardinalL α' → Empty.⊥
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

    Ex : Type (ℓ-suc ℓ)
    Ex = ∥ Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) ∥₁

Apply excluded middle to the proposition Ex. If it holds, the required mere witness is already present. If it is refuted, then every proposed member γ and injection from α' to γ yields a contradiction; this is precisely the condition saying that the ordinal α' is a cardinal.

    some-γ : ⟨ fst κ ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide (lem (Ex , squash₁))
      where
      decide : Ex ⊎ (Ex → Empty.⊥) → Ex

The refutation branch is impossible by not-card, so both outcomes produce Ex. At this step excluded middle provides the case distinction; it does not remove the truncation or choose a particular γ.

      decide (inl e)  = e
      decide (inr ¬e) =
        Empty.rec (not-card κ∈a (λ γ γ∈a inj → ¬e ∣ γ , γ∈a , inj ∣₁))

A witness of the untruncated content of Ex consists of γ ∈ a and an internal injection from α' to γ. Since members of an ordinal are ordinals and δ is transitive, γ again satisfies the induction predicate. The induction hypothesis supplies an injection from γ to κ, and transitivity of internal injection composes the two.

    from-γ : Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) → InjL α' κ
    from-γ (γ , γ∈a , α↪γ) =
      injl-trans α' γ κ α↪γ

To invoke the induction hypothesis at γ, the proof supplies all three components of P: constructibility is the second component of γ; ordinalhood follows from γ ∈ a and the ordinalhood of a; membership in δ follows from γ ∈ a ∈ δ and the transitivity of the ordinal δ.

        (ih (fst γ) γ∈a (snd γ)
            (mem-ord {A = a} orda (fst γ) γ∈a)
            (ordδ .fst γ∈a a∈δ))

The first trichotomy branch has a ∈ κ. Because an ordinal is transitive, every member of a is then a member of κ; this inclusion is coded as an internal injection from α' to κ.

    go : Tri a (fst κ) → InjL α' κ
    go (inl a∈κ)       =
      inclusion-coded α' κ (λ z z∈a → ordκ .fst z∈a a∈κ)

In the equality branch, transport along a ≡ fst κ turns the same inclusion into the required injection. In the remaining branch κ ∈ a, the truncated witness supplied above is eliminated into InjL α' κ; this elimination is valid because InjL is itself a proposition.

    go (inr (inl e))   =
      inclusion-coded α' κ (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) e z∈a)
    go (inr (inr κ∈a)) = PT.rec squash₁ from-γ (some-γ κ∈a)

The three branches exhaust ordinal trichotomy. Hence every ordinal below the successor cardinal δ internally injects into its base κ. Well-founded membership permits the descent to γ. Excluded middle is used in two places: ord-tri obtains the trichotomy, and the branch above κ obtains the truncated smaller target.