--- title: "The power set in L" module: L.Axioms.Power lang: en site: "Bedrock" description: "The power set in L" stage: "Constructible stages and the axioms" reading_order: 36 canonical: https://bedrock.institute/en/L.Axioms.Power.html html: L.Axioms.Power.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Power.lagda.md prerequisites: [Base.Prelude, Base.Classical, Base.Impredicativity, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Axioms.Power.md, https://bedrock.institute/ja/L.Axioms.Power.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 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. ```agda {-# 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda subFo : S → Formula S 1 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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`. ```agda 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. ```agda β : 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. ```agda 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`. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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.