Bounded subsets appear at controlled stages

The bounded-subset theorem starts with an internal cardinal κ whose underlying set is an ordinal and does not belong to ω, together with an arbitrary constructible set y whose ambient members all lie in κ. Under propositional truncation, it gives a constructible ordinal β such that y ∈ Lset β and a coded injection β ↪ κ exists. It assumes no formula defining y, selects no least stage, and makes no uniform choice of β as y varies.

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

The proof is classical only through the displayed instance of excluded middle. This hypothesis supports the earlier constructions of stages, hulls, and coded maps used here; it does not turn the final truncated existence into a chosen family of witnesses.

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

Fix a universe level ℓ and excluded middle at level ℓ-suc ℓ. Every construction below, including the final bounded-subset theorem, depends on this single classical hypothesis and on no choice principle.

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

Two levels of objects must be kept separate throughout the argument. Symbols such as κ, α₀, lam, and later β denote sets in the ambient cumulative hierarchy, some proved to be ordinals; Lset κ, Lset α₀, Lset lam, and Lset β denote the corresponding constructible stages. Membership in a stage index and membership in its indexed stage are different assertions.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω )

The first task is to place both κ and y in one sufficiently high constructible stage. Since y is already supplied as a constructible set, an occurrence stage can be obtained directly; no formula defining y, and no finite list of defining parameters, enters this construction.

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( pairʟ )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )

The central strategy is to enlarge Lset κ by the single point y, generate an elementary Skolem hull from that transitive starting set, and apply condensation. Counting the starting set by κ will count the whole hull by κ; condensation will then convert the collapsed hull into a stage Lset β.

open import L.GCH.Assembly {ℓ} lem using ( InternalBoundedSubset )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.SkolemHull {ℓ} lem
  using ( module UnionKit; module HullStage; module HullElemDown )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; ω⊆; Goal; module Step )

This plan needs two different kinds of control. A sufficiently closed ordinal lam provides the ambient stage in which the hull and condensation argument can be carried out. Coded injections control size: first X ↪ κ, then M ↪ κ, and finally β ↪ κ.

open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )
open import L.GCH.StageInjection {ℓ} lem using ( stage-counted; module Site )
open import L.GCH.OmegaRecursion {ℓ} lem using ( pairʟ-in )
open import L.GCH.HullCounting {ℓ} lem

The size estimate begins with two elementary pieces. The stage Lset κ can be coded into κ, and a singleton can also be coded into κ. Finite tags keep their images disjoint, while the square law for the infinite internal cardinal κ absorbs the resulting product back into κ.

  using ( ord⊆Lset; module Union2; tag-union; module Point; module Count )

Several equalities below are proved by comparing membership in both directions. The alternatives arising from union membership are propositionally truncated, but each target membership statement is a proposition, so those alternatives may be used locally without selecting a lasting branch.

open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )

Finite von Neumann numerals provide the tags used in the union coding, while ordinal successor closure is part of the environment needed for the hull. Well-foundedness supports the square law. Propositional truncation records the existence of coded injections without exposing a chosen graph.

open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet; ⁅_⁆s )
open InfinitySet {ℓ} using ( #_; ω; sucV )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

Whenever an injection is asserted through InjL, its graph exists only under propositional truncation. The proof may compose such existences inside propositions, but it never obtains a distinguished injection that can be used as computational data outside the truncation.

open PT using ( ∣_∣₁ )

The subset premise is deliberately stated with ambient membership. Thus an arbitrary ambient set z may be tested for membership in y and then in κ; z is not required to arrive together with its own proof of constructibility.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

By contrast, κ and y are elements of the constructible carrier S: each packages an ambient set with evidence that it belongs to L. The eventual witness is packaged in the same way, so the theorem produces a constructible ordinal rather than an arbitrary ambient ordinal.

open hPropStructure 𝒮ʟ using ( S )

Bounding a constructible subset of a cardinal

Fix a constructible set κ whose underlying set is an ordinal, an internal cardinal, and not a member of ω. Also fix an arbitrary constructible set y and assume pointwise that every ambient member of y belongs to κ. These are the complete hypotheses: in particular, no definition of y by a formula or by finitely many parameters is assumed.

module At (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ)
          (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
          (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩) where

The assumptions that κ is an ordinal and κ ∉ ω imply ω ⊆ κ. Since every finite von Neumann numeral # k belongs to ω, it follows that # k ∈ κ for every k. These elements will serve as the finite tags in the union coding.

  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)

The ordinal κ and the constructible stage indexed by it are different sets. We therefore package Lset κ as the internal set Lκ; this stage will form the large part of the starting set, while κ itself remains the cardinal into which that starting set is coded.

  Lκ : S
  Lκ = LsetS (fst κ) oκ

To place κ and y in one common stage, first form their unordered pair inside L. A stage containing this pair will contain both entries by transitivity, so one occurrence-stage construction suffices for the two objects.

  private
    P₀ : S
    P₀ = pairʟ κ y

Choose an ordinal stage index α₀ at whose stage the pair occurs. This is a convenient occurrence index supplied by constructibility; nothing here says that α₀ is the least stage at which the pair appears.

    α₀ : V ℓ
    α₀ = stage (fst P₀) (snd P₀)

The chosen stage index α₀ is an ordinal. This matters because the next construction asks for a superadequate ordinal strictly above it and because ordinal transitivity will later carry κ from below α₀ into lam.

    oα₀ : IsOrd α₀
    oα₀ = stage-ord (fst P₀) (snd P₀)

The cardinal κ belongs to Lset α₀. Indeed, κ is a member of the unordered pair, the pair belongs to Lset α₀, and this stage is transitive. This is stage membership, not yet the ordinal membership κ ∈ α₀ used later.

    κ∈Lα₀ : ⟨ fst κ ∈ˢ Lset α₀ ⟩
    κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst κ}
      (pairʟ-in κ y κ (inl refl)) (stage-mem (fst P₀) (snd P₀))

The same transitivity argument places y in Lset α₀ through the other member of the pair. Unlike κ, the set y is not assumed to be an ordinal, so this fact will be transported to Lset lam by stage monotonicity rather than converted into membership in α₀.

    y∈Lα₀ : ⟨ fst y ∈ˢ Lset α₀ ⟩
    y∈Lα₀ = layer-trans (Lset-layer α₀) {x = fst P₀} {y = fst y}
      (pairʟ-in κ y y (inr refl)) (stage-mem (fst P₀) (snd P₀))

Now choose explicitly a superadequate ordinal lam with α₀ ∈ lam. This strict extension provides enough closure for the later hull and condensation arguments. Although lam itself is explicit, the adequate subindices promised by its superadequacy remain under propositional truncation.

    sa = superadequate-above α₀ oα₀

Write this high ordinal as lam, corresponding to λ in the exposition. Its particular construction will play no further role; the proof uses its ordinality, successor closure, superadequacy, and its position above α₀.

  opaque
    lam : V ℓ
    lam = sa .fst

The first retained fact is that lam is an ordinal. Consequently it is transitive, which will allow ordinal memberships below lam to be carried farther upward.

    ordλ : IsOrd lam
    ordλ = sa .snd .fst

The second retained fact is closure under ordinal successor: whenever d ∈ lam, also sucV d ∈ lam. This closure is one of the structural hypotheses under which the finite Skolem construction remains inside the stage indexed by lam.

    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst

Superadequacy says that for each d ∈ lam there merely exists an adequate ordinal γ with d ∈ γ ∈ lam. It supplies local adequate room below lam without choosing a least γ or a family of such choices.

    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd

The cardinal κ belongs to the ordinal index lam. Because both κ and α₀ are ordinals, κ ∈ Lset α₀ first yields κ ∈ α₀. The relation α₀ ∈ lam and the transitivity of the ordinal lam then give κ ∈ lam. This conclusion concerns the index lam, rather than the stage Lset lam.

    κ∈λ : ⟨ fst κ ∈ˢ lam ⟩
    κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (fst κ) oκ κ∈Lα₀) (sa .snd .snd .fst)

For y, the required conclusion is instead membership in the stage Lset lam. Since α₀ ∈ lam, monotonicity gives Lset α₀ ⊆ Lset lam; applying it to the earlier fact y ∈ Lset α₀ yields y ∈ Lset lam. No ordinality of y is needed.

    y∈Lλ : ⟨ fst y ∈ˢ Lset lam ⟩
    y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀

Every ambient member of y lies in Lset κ. Indeed, the subset hypothesis sends z ∈ y to z ∈ κ; since κ is an ordinal, such a z is itself an ordinal, lies in its successor stage, and hence lies in Lset κ by cumulativity. Thus y ⊆ κ supplies the stage inclusion needed to make the starting set transitive.

  y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ Lset (fst κ) ⟩
  y⊆Lκ z hz = ord⊆Lset (fst κ) oκ z (y⊆κ z hz)

Form the starting set X = Lset κ ∪ {y} inside Lset lam. It contains y and is transitive: elements inherited from Lset κ stay in that transitive stage, while an element of y lies in κ by hypothesis and hence in Lset κ. This transitivity is precisely what will make the collapse fix y later.

  module UK = UnionKit (fst κ) lam (fst y) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω
    using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )

From now on, X denotes this transitive enlargement of Lset κ. The two features to retain are complementary: y ∈ X ensures that the hull contains the set we want to locate, and transitivity ensures that the collapse does not alter it.

  X : V ℓ
  X = UK.X

For counting, construct the singleton {y} internally together with its injection into κ, using the tag 0 ∈ κ, and take its internal union with Lκ. This produces a coded presentation of the same set Lset κ ∪ {y} whose two pieces already carry the injections needed for the tagged-union argument.

  module Pt = Point κ (num∈κ ) y using ( Y; Y-out; Y-in; injL )
  module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )

Call this internally constructed union Xʟ. It represents the same mathematical union as X, but its construction carries the internal coding data needed to prove an injection into κ.

  Xʟ : S
  Xʟ = U.D

To identify Xʟ with X, compare their members in both directions. In the forward direction, membership in the internally coded union yields, under propositional truncation, either a member of Lset κ or a member of the coded singleton; both cases imply membership in X. The elimination is valid because membership in X is a proposition.

  Xʟ-eq : fst Xʟ ≡ X
  Xʟ-eq = extensionalV {a = fst Xʟ} {b = X} (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ˢ fst Xʟ ⟩ → ⟨ z ∈ˢ X ⟩
    fwd z h = PT.rec (snd (z ∈ˢ X)) go (U.out zS h)

In the stage case, the left inclusion places the member in X. The temporary packaging of z as constructible is justified by transitivity of L: since z belongs to the constructible set Xʟ, it is constructible as well.

      where
      zS : S
      zS = z , isL-trans {x = fst Xʟ} {y = z} h (snd Xʟ)
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ fst Pt.Y ⟩ → ⟨ z ∈ˢ X ⟩
      go (inl hz) = UK.Lα∈X z hz

In the singleton case, the coded member is equal to y, already known to belong to X. Conversely, membership in X splits, again only under propositional truncation, into the Lset κ side and the singleton side; the target membership in Xʟ is a proposition, so this second elimination is equally legitimate.

      go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X
    bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩
    bwd z h = PT.rec (snd (z ∈ˢ fst Xʟ)) go (UK.X-mem z h)
      where
      go : ⟨ z ∈ˢ Lset (fst κ) ⟩ ⊎ ⟨ z ∈ˢ ⁅ fst y ⁆s ⟩ → ⟨ z ∈ˢ fst Xʟ ⟩

The reverse cases enter the two summands of Xʟ. A member of Lset κ enters on the left, with constructibility inherited from that stage; a member of {y} is first identified with y and then enters through the coded singleton. Thus extensionality proves fst Xʟ ≡ X without retaining either truncated case split.

      go (inl hz) = U.in₁ (z , isL-trans {x = Lset (fst κ)} {y = z} hz (snd Lκ)) hz
      go (inr hz) = subst (λ w → ⟨ w ∈ˢ fst Xʟ ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)

The starting set is constructible, since the internal copy is constructible and the two copies have equal underlying sets.

  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (snd Xʟ)

Package X together with this constructibility proof as XS : S. Its underlying ambient set is still exactly X; the packaging merely supplies the internal domain required by InjL.

  XS : S
  XS = X , X-isL

The infinite-cardinal square law gives the propositionally truncated existence of a coded injection κ × κ ↪ κ. Its hypotheses are exactly the facts fixed at the start: κ is an ordinal internal cardinal and is not a member of ω. No bijection or chosen injection graph is produced.

  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω

The two component injections feed the tagged-union construction, giving a coded injection Xʟ ↪ κ × κ: tags #0 and #1 distinguish the stage part from the singleton part. Composing with the square-law injection gives Xʟ ↪ κ, and transport along fst Xʟ ≡ X changes the domain to the constructible package XS. The result is the required coded injection X ↪ κ, still under propositional truncation.

  base : InjL XS κ
  base = move Xʟ XS κ κ Xʟ-eq refl
    (injl-trans Xʟ (prodL κ) κ
      (tag-union κ (num∈κ ) (num∈κ ) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL)
      pairκ)

Let M be the Skolem hull generated by X inside Lset lam. The Tarski-Vaught theorem for this hull shows that M is elementary in the sense required by condensation. The whole transitive set X is the starting set, so this is the same hull that contains y and whose collapse will later fix y.

  elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ

The hull-counting theorem propagates X ↪ κ through the finite stages of Skolem closure and then through their union. It yields the existence, under propositional truncation, of a coded injection M ↪ κ. The hull is therefore both elementary enough for condensation and small enough to remain controlled by κ.

  hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base

Condensation supplies an explicit ordinal β and identifies the collapse image of M with Lset β. It also packages Lset β and M as constructible sets and gives the propositionally truncated coded injection Lset β ↪ M induced by the inverse collapse. Here β is the stage index, while Lset β is the stage it indexes.

  module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )

We now use three aspects of this single hull construction: the hull M, the inclusion X ⊆ M, and the collapse map π with image πX. The associated fixed-point theorem applies to transitive subsets of M. These facts will first show that y is unchanged by the collapse and then place that same y in the stage identified by condensation.

  module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ
    using ( πX; π; fixes; πX-intro )

The set y belongs to the Skolem hull M: it was placed in the starting set X, and every member of X lies in the hull generated from X.

  y∈M : ⟨ fst y ∈ˢ HS.M ⟩
  y∈M = HSH.X⊆M (fst y) UK.x∈X

The collapse fixes y: because the starting set X is transitive and contained in the hull, the collapse map acts as the identity on every member of X, and y is one of them.

  πy : HSC.π (fst y) ≡ fst y
  πy = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    UK.Xtr (fst y) UK.x∈X

The collapse image contains π(y), since y belongs to the hull. Condensation identifies that image with the constructible stage Lset β, and the fixed-point equation π(y) = y then gives y ∈ Lset β. The point is that the collapse has not replaced y by another set: it has located the original y inside a controlled constructible stage.

  y∈Lβ : ⟨ fst y ∈ˢ Lset St.β ⟩
  y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy
    (subst (λ w → ⟨ HSC.π (fst y) ∈ˢ w ⟩) St.ext (HSC.πX-intro (fst y) y∈M))

The ordinal β injects into κ by a chain of three coded injections: the inclusion from β into the level Lset β by ordinal membership, the restricted inverse collapse from Lset β into the hull M, and the hull counting from M into κ. The chain gives a coded injection, not a bare ordinal comparison.

  β↪κ : InjL St.βL κ
  β↪κ = injl-trans St.βL St.Lβ κ
    (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz))
    (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)

The local witness now packages the constructible ordinal β, its ordinality, the fact that y belongs to the stage Lset β, and the coded injection β ↪ κ. Here β is the stage index being returned, whereas Lset β is the constructible stage in which y has been located.

  result : Σ[ b ∈ S ] (IsOrd (fst b) × ⟨ fst y ∈ˢ Lset (fst b) ⟩ × InjL b κ)
  result = St.βL , St.oβ , y∈Lβ , β↪κ

Finally, ∣_∣₁ places the entire local witness under propositional truncation. The final theorem therefore retains only that some constructible ordinal β satisfies y ∈ Lset β and admits a coded injection β ↪ κ. It provides neither a least nor a canonical β, and it makes no uniform choice of witnesses as y varies.

internal-bounded-subset : InternalBoundedSubset
internal-bounded-subset κ oκ cκ κ∉ω y y⊆κ =
  ∣ At.result κ oκ cκ κ∉ω y y⊆κ ∣₁