Ordinals below a successor cardinal inject into its base

Fix a universe level ℓ and assume lem : LEM (ℓ-suc ℓ). This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

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.

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 to decide the formula presenting Ex; the remaining ingredients are structural facts about V, L, ordinals and internal injections.

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.

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.Induction.WellFounded as WF

open hPropView 𝒮ᵥ 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 = hPropView 𝒮ᵥ 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 = hPropView 𝒮ʟ using ( S )
module Sem = FOL.Semantics 𝒮ʟ
module At = Sem.At SL.S id

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 α' → ⊥₀
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

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

    exFo : Formula SL.S 
    exFo = ∃̇ ((var zero ∈̇ var (suc zero))
             ∧̇ injLAt (suc zero) zero)

    exFill : Ex → ⟨ (α' ∷ []) At.⊨ exFo ⟩
    exFill = map₁ (λ { (γ , γ∈a , inj) → γ , γ∈a
      , InjLAt.fill (suc zero) zero (γ ∷ α' ∷ []) inj })

    exRead : ⟨ (α' ∷ []) At.⊨ exFo ⟩ → Ex
    exRead = map₁ (λ { (γ , γ∈a , sat) → γ , γ∈a
      , InjLAt.read (suc zero) zero (γ ∷ α' ∷ []) sat })

    exDecision : Dec Ex
    exDecision = mapDec exRead (λ ns e → ns (exFill e))
      (FOL.Semantics.decideSatisfaction 𝒮ʟ id lem (α' ∷ []) exFo)

The formula exFo binds the possible γ, conjoins γ ∈ α' with the formula injLAt α' γ, and therefore presents exactly Ex. The maps exFill and exRead prove the two directions under propositional truncation. Excluded middle is then applied through decideSatisfaction to this formula. If satisfaction holds, the required mere witness is present; if it is refuted, every proposed member and injection yields a contradiction, precisely the condition saying that α' is a cardinal.

    some-γ : ⟨ κ .fst ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide exDecision
      where
      decide : Dec Ex → 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 (yes e) = e
      decide (no ¬e) =
        ⊥₀-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)) = 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.