The power set in L

For a constructible set a, what should its power set inside L contain? The quantifiers of the model range over its carrier S, so the required members are the constructible model elements x that satisfy the internal inclusion x ⊆ˢ a. The ambient hierarchy can form the power set of the underlying set A = fst a, but its membership condition ranges over all of V ℓ and imposes no constructibility requirement. That ambient set can therefore supply indices, but it cannot simply be returned as the power set in L.

The proof follows three mathematical steps. It uses the ambient power set to obtain a small presentation of all candidates, retains the indices that present constructible candidates and bounds their stages by one ordinal β, then uses Separation inside Lset β to collect exactly the internally included model elements. The host-level construction provides the bound; the final set itself is produced inside the constructible model.

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

The construction needs two kinds of smallness. Propositional resizing replaces a proposition at the model's truth-value level by an equivalent proposition at the small index level. The impredicativity package also provides a small classifier for small propositions, from which the ambient hierarchy can form a power set. Both are derived from excluded middle. They solve different size problems and should not be confused: resizing will make constructibility fit inside a small index type, whereas the classifier builds the ambient power set that supplies the indices.

open import Base.Prelude
open import Base.Classical using ( LEM; lem→resizing; lem→impredicativity )
open import Base.Impredicativity using ( module Impredicativity )

Fix a universe level ℓ and one assumption lem : LEM (ℓ-suc ℓ). The goal is the model field saying that, for each a in L, there is a unique model element whose members are exactly the model elements internally included in a. Uniqueness is packaged by the host type isContr; the object-theoretic content is the power-set axiom, and extensionality supplies its uniqueness. The same single lem reaches the proof through four routes: propositional resizing, the small classifier for the ambient power set, the canonical stage function, and the reflection used by full Separation. No further classical assumption is introduced.

module L.Axioms.Power {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Three levels of discourse meet in the proof. Host types organize indices and proofs. The ambient structure 𝒮ᵥ has all sets of the cumulative hierarchy as its elements. The restricted structure 𝒮ʟ has pairs consisting of an ambient set and evidence that it is constructible. The formula language supplies the bounded universal needed to express inclusion inside 𝒮ʟ. Thus the ambient structure can enumerate possible subsets, while the restricted structure is where the object-theoretic power-set axiom must be established.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ∀̇∈ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

The ambient hierarchy provides a set 𝒫V A containing every ambient subset of A, together with its membership specification. The constructible hierarchy provides the stages Lset α and their strict monotonicity: membership in an earlier stage lifts along α ∈ β. For each constructible candidate, the stage function supplies a canonical ordinal index whose stage contains it. The bounding lemma then places this small family of ordinal indices strictly below one ordinal. Although the stage function also proves minimality, this chapter uses only its ordinality and membership facts.

open import V.Model {ℓ} using ( module Power )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

Once the ordinal bound β is available, LsetS β oβ is a model element known to contain every internal subset under consideration. The remaining mathematical operation is therefore Separation by the one-variable inclusion formula. The general theorem hasSeparationL accepts arbitrary formulas: it finds a reflecting stage, replaces the formula there by its bounded relativization, and applies bounded Separation. The present formula is already Δ₀, but this invocation still follows that general route. Consequently formula reflection and the stage construction for the parameter are actual uses of the same lem, even in this bounded instance.

open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )

Every hierarchy set has a small presentation: a type ⟪P⟫ of indices and an embedding ⟪P⟫↪ that presents its members. Membership in P is the propositional truncation of a fibre of this embedding. Because the map is an embedding, each fibre is already a proposition, so ∈-asFiber may recover the index and its identifying path without invoking Choice. The equivalence maps also let the proof move between a resized proposition and its original form. At the end, propositional extensionality turns two implications into a path of truth values.

open import Cubical.Foundations.Equiv using ( _≃_; invEq; equivFun )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )

Opening 𝒮ʟ fixes the unqualified carrier S and membership relation for the rest of the proof. An element of S is a constructible set together with its constructibility evidence; fst forgets that evidence and returns its ambient set. The parameter ℓ controls small presentation types such as ⟪P⟫, while V ℓ, the carrier S, and the structures' truth values live at ℓ-suc ℓ. Thus the smallness argument concerns the index type, not the model carrier.

open hPropStructure 𝒮ʟ

The two model interfaces give two subset relations with the same notation but different quantifier domains. In ModelL, x ⊆ˢ a quantifies over S, so it tests only constructible elements. In ModelV, the corresponding relation quantifies over every set in V ℓ. The latter is stronger for an arbitrary left side. When the left side is constructible, transitivity of L turns each of its ambient members into an element of S, and this supplies the precise bridge from internal inclusion to ambient inclusion used below.

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; _⊆ˢ_ )
module ModelV = FOL.ZFModel 𝒮ᵥ

The notation _⊨_ here is the inner satisfaction relation for formulas over the carrier S, evaluated in the restricted structure 𝒮ʟ. Constants denote the model elements that they name, and the restricted membership relation reads their first projections in the ambient hierarchy. The surrounding absoluteness module makes an outer reading available as well, but this chapter does not apply an absoluteness theorem. Its only satisfaction statement is the direct inner meaning of the bounded inclusion formula.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

The ambient power-set construction is instantiated with the small classifier obtained from lem→impredicativity lem. This construction uses only the hPropSmallness component: it represents a characteristic function by a function into a small type of truth-value codes and forms the corresponding hierarchy set. Propositional resizing of isL is a separate operation and does not enter this instantiation. Keeping these roles distinct will make the later index construction transparent.

module Pow = Power (Impredicativity.hPropSmallness (lem→impredicativity lem))

The condition, as a formula

For a : S, the formula subFo a has one free slot for a candidate x and reads

for every y in x, y is in a.

The two occurrences of var zero lie in different contexts. Outside the bounded universal it denotes the candidate x; inside the body it denotes the newly bound member y. The term con a is allowed because the constant domain is the model carrier. At the environment x ∷ [], the semantics of the bounded universal reduces directly to x ⊆ˢ a. This is internal inclusion, with y ranging over constructible model elements. The formula is Δ₀, even though the proof later passes it to the general Separation interface.

subFo : S → Formula S 
subFo a = ∀̇∈ (var zero) (var zero ∈̇ con a)

Bounding the constructible subsets

Fix a : S. Its first projection A is the same set viewed in the ambient hierarchy, with the constructibility evidence forgotten. The set P = Pow.𝒫V A satisfies the full ambient power-set specification: membership in P requires only ambient inclusion in A, with no constructibility hypothesis. Thus any nonconstructible ambient subset, if one is present, also belongs to P. Moreover, the construction supplies no proof that P itself is constructible. The proof uses only the small presentation ⟪P⟫ and later filters its indices by constructibility; P is not the power set returned in the model.

module Bound (a : S) where
  private
    A P : V ℓ
    A = fst a
    P = Pow.𝒫V A

For an ambient set v, constructibility isL v is a proposition at level ℓ-suc ℓ. Concretely, it is the propositional truncation of the existence of an ordinal stage containing v. Such a proposition is too large to use as the second component of a type at level ℓ. The function rsz therefore chooses a small proposition Q : hProp ℓ and an equivalence between its underlying type and isL v. This changes only the universe level of the truth value. It neither removes the propositional truncation nor selects an ordinal stage.

    rsz : (v : V ℓ) → Σ[ Q ∈ hProp ℓ ] (⟨ isL v ⟩ ≃ ⟨ Q ⟩)
    rsz v = lem→resizing lem (isL v)

The host type Ix indexes exactly the constructible members of the ambient power set. An element consists of an index m : ⟪P⟫, presenting an ambient subset of A, together with a proof of the resized constructibility proposition for the presented set. Both components are small, so Ix : Type ℓ and the ordinal bounding lemma can quantify over it. Ix is only a host-level index type. It is neither an element of L nor a class defined by an object-language formula, and it will not become the final power set.

  Ix : Type ℓ
  Ix = Σ[ m ∈ ⟪ P ⟫ ] ⟨ rsz (⟪ P ⟫↪ m) .fst ⟩

To find a stage for an index i : Ix, the proof first restores the original constructibility proposition. The inverse of the resizing equivalence sends i.snd from the small proposition back to isL (⟪P⟫↪ i.fst). The result still asserts only, under propositional truncation, that some ordinal stage contains the presented set. Thus unres reverses the change of universe level but does not extract a witness from the truncation. The next definition performs the additional work needed to obtain a definite stage index.

  private
    unres : (i : Ix) → ⟨ isL (⟪ P ⟫↪ (i .fst)) ⟩
    unres i = invEq (rsz (⟪ P ⟫↪ (i .fst)) .snd) (i .snd)

The function stg assigns each entry of Ix its canonical stage index: the least ordinal σ for which the presented set belongs to Lset σ. This is a separate classical step from resizing. Internally, stage uses excluded middle to decide whether a smaller witness exists during a well-founded descent. Propositional truncation is eliminated only into LeastOrd, whose propositionhood is proved using ordinal trichotomy and uniqueness of the remaining evidence. The result is therefore a definite ordinal index without a general rule for extracting arbitrary truncated witnesses. Only stage-ord and stage-mem, not minimality, are used here.

    stg : Ix → V ℓ
    stg i = stage (⟪ P ⟫↪ (i .fst)) (unres i)

Now stg : Ix → V ℓ is a genuinely small family, and stage-ord proves that each value is an ordinal. The lemma boundingOrd returns explicit data: an ordinal β together with a proof that every stg i is a member of β. Its construction is carried out in the host theory by taking successors of the given ordinals and then their union. It is not an application of Replacement inside L; no Replacement field is used anywhere in this chapter. The strict bound is exactly the form later required by Lset-mono.

    b = boundingOrd Ix stg (λ i → stage-ord (⟪ P ⟫↪ (i .fst)) (unres i))

The first projection of the bounding data is named β. It is an ambient hierarchy set produced by a host-level construction, and the accompanying proof will show that it is an ordinal. What later becomes an element of the model is the stage Lset β, packaged by LsetS β oβ; the proof does not need to package β itself. Moreover, β depends on the stages of all constructible ambient subsets of A, rather than only on the stage of a. Such a family-dependent bound suffices for the power-set axiom, so no condensation estimate is needed.

  β : V ℓ
  β = b .fst

The proof oβ records that the bound is an ordinal. The other component of b.snd, used later as b.snd.snd i, says stg i ∈ β for every i : Ix. This is strict membership of ordinal indices. Given stage-mem : presented-set ∈ Lset (stg i), Lset-mono uses precisely that membership to lift the presented set into Lset β. Ordinality and this strict bounding property are the two facts about β needed in the remainder.

  oβ : IsOrd β
  oβ = b .snd .fst

The lemma below states the essential coverage property of the bound. If x : S is internally included in a, then its underlying ambient set fst x belongs to Lset β. The proof first identifies fst x with the member of P presented by a suitable index i : Ix. The candidate belongs to Lset (stg i) by stage-mem, and stg i ∈ β lets Lset-mono lift this membership to Lset β. The final subst transports the result along the presenting path. The local definitions below justify the existence and properties of that particular i.

  below : (x : S) → ⟨ x ⊆ˢ a ⟩ → ⟨ fst x ∈ Lset β ⟩
  below x x⊆a =
    subst (λ w → ⟨ w ∈ Lset β ⟩) pa
      (Lset-mono {α = β} {β = stg i} (b .snd .snd i) (stage-mem _ (unres i)))
    where

To obtain the index, first convert internal inclusion into ambient inclusion. Given an arbitrary ambient member v ∈ fst x, transitivity of constructibility produces isL v from x.snd; the pair (v , proof) is then a model element to which x⊆a applies. Hence fst x is an ambient subset of A. The reverse direction of Pow.power-spec turns this inclusion into fst x ∈ P. Membership in P is a propositionally truncated fibre, but the presentation map is an embedding, so its fibre is a proposition. Accordingly ∈-asFiber returns an actual presentation index and a path pa identifying its image with fst x. This is elimination justified by uniqueness, not an application of Choice.

    vsub : ⟨ ModelV._⊆ˢ_ (fst x) A ⟩
    vsub v v∈ = x⊆a (v , isL-trans {x = fst x} {y = v} v∈ (x .snd)) v∈
    fib = ∈-asFiber {a = fst x} {b = P}
            (subst ⟨_⟩ (sym (Pow.power-spec A (fst x))) vsub)
    pa : ⟪ P ⟫↪ (fib .fst) ≡ fst x

The path pa completes the recovered presentation index into an element of Ix. Its first component is fib.fst. For the second, sym pa transports x.snd : isL (fst x) to constructibility of the set presented by that index, and the forward map of the resizing equivalence encodes this proposition at level ℓ. Thus i really indexes the same underlying set as x, and its stage is one of the stages bounded by β. Combining stage-mem, b.snd.snd i, and Lset-mono, then transporting along pa, proves the conclusion of below.

    pa = fib .snd
    i : Ix
    i = fib .fst
      , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd)
          (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))

The field

The type of hasPowerL is the exact model-theoretic statement to be proved. It asks for a contractible type of realizers p : S whose membership predicate, tested at every x : S, is x ⊆ˢ a. At this point the ambient set P has finished its work: it supplied the index family from which Bound.β a was constructed, but it does not appear in the result.

Applying hasSeparationL to the model element LsetS (Bound.β a) (Bound.oβ a) first gives a contractible SetOf for the stronger-looking predicate saying that x lies in this stage and satisfies subFo a. The only remaining task is to show that this predicate equals internal inclusion. The local equality Q≡ provides that identification, and the outer subst transports the contractible package to the predicate required by the power-set field.

hasPowerL : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
hasPowerL a =
  subst (λ Q → isContr (SetOf Q)) Q≡
    (hasSeparationL (LsetS (Bound.β a) (Bound.oβ a)) (subFo a))
  where

The remaining equality compares the class cut out by separation with the class required by the power-set field. Its left-hand side says that x lies in the bounding stage and that x satisfies subFo a; the satisfaction statement reduces to the internal inclusion x ⊆ˢ a. In the forward direction the proof therefore discards the stage-membership component. In the reverse direction, Bound.below supplies that component from x ⊆ˢ a. Propositional extensionality turns the two implications into a path at each x, and functional extensionality combines these paths into the predicate equality Q≡. The outer subst transports the contractible type of realizers supplied by separation along this equality. Set extensionality is not used in Q≡ itself; it has already supplied the uniqueness packaged by separation.

Thus hasPowerL a proves the power-set axiom for the object theory in its exact model-theoretic form. It gives a contractible type of elements p : S such that, for every x : S, membership x ∈ˢ p is equivalent to the internal statement x ⊆ˢ a. Both p and every candidate x range over the carrier of the constructible model. The ambient power set used earlier only provides a small index of candidates and is not the set produced here. The single assumption LEM (ℓ-suc ℓ) reaches this construction through propositional resizing, the small classifier, the choice of a canonical stage from propositionally truncated constructibility, and the reflection used by full separation.

  Q≡ : (λ x → (x ∈ˢ LsetS (Bound.β a) (Bound.oβ a)) ⊓ ((x ∷ []) ⊨ subFo a))
     ≡ (λ x → x ⊆ˢ a)
  Q≡ = funExt (λ x → ⇔toPath
    (λ { (_ , x⊆a) → x⊆a })
    (λ x⊆a → Bound.below a x x⊆a , x⊆a))

Recap

The construction has three distinct roles: the ambient power set supplies a small presentation, the host theory bounds the stages of its constructible members, and internal Separation cuts the desired set from that bound. L.Model installs hasPowerL as the hasPower field of L⊨ZF, after which the record defines the internal operation 𝒫. The later GCH arguments use this operation and the specification ℩-spec (hasPower κ) to pass between membership and internal inclusion; they never use the auxiliary ambient Pow.𝒫V.

The logical account is equally specific. The one assumption LEM (ℓ-suc ℓ) supplies the small classifier, propositional resizing, the canonical stage construction, and formula reflection for full Separation. No form of Choice, the Replacement field, or condensation is used in this proof.