--- title: "Separation and replacement, in full" module: L.Axioms.Full lang: en site: "Bedrock" description: "Separation and replacement, in full" stage: "Constructible stages and the axioms" reading_order: 35 canonical: https://bedrock.institute/en/L.Axioms.Full.html html: L.Axioms.Full.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Full.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Manipulation.Relativization, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, L.Constructible, L.Stage, L.Axioms.Separation, L.Axioms.Basic, L.FormulaReflection] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Axioms.Full.md, https://bedrock.institute/ja/L.Axioms.Full.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Separation and replacement, in full Bounded separation can form the subset of a constructible set defined by a Δ₀ formula, but the separation scheme permits an arbitrary first-order formula. This chapter closes that gap by reflecting one formula at a stage containing the set to be separated. It then proves full replacement by placing all values of a functional relation on the source set in one stage and collecting them with the full separation result. These are the two formula-scheme fields proved here; the complete ZF and ZFC records are assembled later. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` The sole classical parameter is the host principle `LEM`. At the stated universe level it decides each proposition by returning either a proof or a refutation. This is not a host-level axiom of choice and gives no operation that selects witnesses from an arbitrary family of propositionally truncated existences. It is also distinct from the choice axiom later interpreted inside the set-theoretic model. ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` Fix `lem : LEM (ℓ-suc ℓ)`. All constructions in this module are relative to this one host assumption. The mathematical conclusions are the separation and replacement schemes for arbitrary first-order formulas in the constructible model; the object-theoretic axiom of choice is neither assumed nor proved here. The dependence on excluded middle enters through the least-stage and formula reflection results used below: the former decides whether a smaller qualifying stage merely exists, and the latter decides the matrix in the reverse direction of the unbounded universal case. ```agda module L.Axioms.Full {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` The argument moves between syntax and semantics. A value of `Formula S n` is an object-language formula with `n` variable positions and constants drawn from `S`; `con` inserts such a constant. Renaming changes which environment position a variable reads and comes with a satisfaction theorem. Relativization replaces each unbounded quantifier by one bounded by a chosen constant, and `Δ₀-relativize` proves structurally that the resulting formula is bounded. The agreement of the original and relativized formulas will come from reflection, not from the syntactic transformation alone. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( con; Formula; ∃̇∈ ) open import FOL.Manipulation.Renaming using ( renameFo; module Sat ) open import FOL.Manipulation.Relativization using ( relativize; Δ₀-relativize ) import FOL.Absoluteness ``` Two structures interpret this language. The ambient cumulative hierarchy `𝒮ᵥ` interprets all sets in `V ℓ`, while `𝒮ʟ` has as elements the sets equipped with proofs of constructibility. For an index `β`, `Lset β` is the corresponding constructible stage; its layer proof yields transitivity, and strict membership between ordinal indices lets membership be raised by `Lset-mono`. For every constructible set, `stage` gives the least ordinal index whose stage contains it, together with ordinality and membership proofs. Only the latter two facts, not minimality itself, are used in this chapter. ```agda import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset-layer; layer-trans; Lset-mono ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem ) ``` Bounded separation and reflection provide the bridge to arbitrary formulas. For a bounded unary formula, `separateΔ₀` constructs the unique constructible set with the required members. For one arbitrary formula `φ` and one ordinal `δ`, `mkReflect` produces an ordinal `β` with `δ ∈ β` and identifies `φ` with its relativization on environments lying in `Lset β`. This is reflection for the specified formula and parameters, not an elementary-submodel assertion about `Lset β`. For replacement, `FunctionalImage` gives one ordinal stage containing every `y` related to some `x ∈ˢ a`, and `LsetS` presents that stage as an object-language constant. ```agda open import L.Axioms.Separation {ℓ} lem using ( module FunctionalImage; separateΔ₀ ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.FormulaReflection {ℓ} lem using ( mkReflect ) ``` Several host constructions make the semantic equalities precise. `⇔toPath` turns implications in both directions between proposition-valued truths into a path, after which function extensionality can identify predicates pointwise. The indexed existential used in `hProp` is propositionally truncated. In the replacement proof, `PT.rec` eliminates such an existence only into another proposition, while `PT.map` transforms witnesses without taking them outside the truncation. Neither operation chooses a source globally. ```agda open import Cubical.Data.Unit using ( tt* ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) ``` The carrier `S` of `𝒮ʟ` consists of an underlying set in `V ℓ` together with a proof of its constructibility. Its equality and membership relations inspect the underlying sets, so `x ∈ˢ a` supplies the ambient membership used later by stage transitivity. Object-language formulas range over this carrier; their constants and environment entries therefore retain the constructibility certificates needed to remain inside the model. ```agda open hPropStructure 𝒮ʟ ``` For a host predicate `Q : S → hProp (ℓ-suc ℓ)`, `SetOf Q` is the type of pairs consisting of a model element `b` and a pointwise path `(x ∈ˢ b) ≡ Q x`. Thus `isContr (SetOf Q)` expresses strong unique existence: its centre supplies an actual realizing set, and its contraction identifies every other realizer with that centre. The predicate `Q` is a host-level function, even when it is built from satisfaction of an object-language formula. Projecting the centre is ordinary data extraction and uses no description principle. ```agda module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) ``` The absoluteness construction gives the same syntax an ambient reading in `𝒮ᵥ` and an inner reading in `𝒮ʟ`. Here the inner relation `_⊨ᵐ_` is renamed `_⊨_`. Consequently `γ ⊨ φ` is itself a host-level proposition asserting that the object-language formula `φ` is true in the constructible structure under the finite environment `γ`; it should not be confused with substituting an arbitrary host predicate into the syntax. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` To compare the two variable orders used later, instantiate the renaming semantics for `𝒮ʟ`, with constants interpreted by the identity function. `Ren.Agrees` states pointwise that a renamed variable position reads the same entry as the corresponding position in another environment. Whenever this agreement is given, `Ren.⊨-rename` identifies satisfaction of the renamed formula with satisfaction of the original formula in the rearranged environment. ```agda module Ren = Sat 𝒮ʟ id ``` ## Two small tools The first local lemma records transitivity on underlying sets. If `x ∈ y` and `y ∈ Lset β`, then `x ∈ Lset β`, because every constructible stage is a transitive set. The variables here lie in `V ℓ`; the lemma does not manufacture a proof that `x` is constructible. At its later use, `x : S` already carries that proof, while `transIn` supplies only the stage-membership fact required by reflection. ```agda private transIn : (β : V ℓ) {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩ transIn β = layer-trans (Lset-layer β) ``` Replacement uses a binary formula in two environment orders. In the model statement, `(y ∷ x ∷ []) ⊨ φ` places the image `y` in slot zero and the source `x` in slot one. After an existential quantifier binds the source, however, its body is evaluated in `(x ∷ y ∷ [])`, with the newly bound source in slot zero. The function `swap` exchanges precisely these two positions of `Fin 2`; it does not reverse the mathematical relation. ```agda swap : Fin 2 → Fin 2 swap zero = suc zero swap (suc _) = zero ``` Applying formula renaming to `swap` gives `swapFo`. If `φ` expects the image in position zero and the source in position one, then `swapFo φ` can be evaluated with the source first. This is a syntactic rearrangement of the free positions; its semantic justification is supplied separately by renaming correctness. ```agda swapFo : Formula S 2 → Formula S 2 swapFo = renameFo swap ``` For concrete elements `x` and `z`, the two environments agree under this transposition. At position zero, `swap` reads the second entry of `x ∷ z ∷ []`, namely `z`; at position one it reads `x`. Both required paths therefore compute to `refl`, giving the complete proof of `Ren.Agrees` for a two-entry environment. ```agda swapAgrees : (x z : S) → Ren.Agrees swap (x ∷ z ∷ []) (z ∷ x ∷ []) swapAgrees x z zero = refl swapAgrees x z (suc zero) = refl ``` Renaming correctness now gives the exact semantic conversion used in replacement: `(x ∷ z ∷ []) ⊨ swapFo φ` is the same proposition as `(z ∷ x ∷ []) ⊨ φ`. Reading `x` as the source and `z` as the image, the left side is the order created by the bounded existential and the right side is the image-first order required by the model. The path works in both directions by ordinary transport. ```agda ⊨-swap : (φ : Formula S 2) (x z : S) → ((x ∷ z ∷ []) ⊨ swapFo φ) ≡ ((z ∷ x ∷ []) ⊨ φ) ⊨-swap φ x z = Ren.⊨-rename swap φ (x ∷ z ∷ []) (z ∷ x ∷ []) (swapAgrees x z) ``` ## Separation Full separation quantifies over every unary object-language formula `φ : Formula S 1`, with no boundedness hypothesis. Its target says that there is a unique model set whose members are exactly those `x` that both belong to `a` and satisfy `φ`. The proof applies bounded separation to the relativized formula and then transports the entire contractible type of realizers along `sym Q≡`. Thus uniqueness comes from `separateΔ₀`; it is not reconstructed after reflection. ```agda hasSeparationL : (a : S) (φ : Formula S 1) → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))) hasSeparationL a φ = subst (λ Q → isContr (SetOf Q)) (sym Q≡) (separateΔ₀ a (relativize c φ) (Δ₀-relativize c φ)) ``` Begin by placing the parameter `a` below the stage where reflection will be used. Its underlying set has the least-stage index `sa`, and `stage-ord` proves that this index is an ordinal. Applying `mkReflect φ` with `sa` produces an ordinal `β`, a strict membership `sa ∈ β`, and a path between the satisfaction propositions of `φ` and its relativization for every environment lying in `Lset β`. Supplying `sa` at this point matters: the reflection theorem is built to contain that index and is not being enlarged afterwards. ```agda where sa = stage (fst a) (a .snd) R = mkReflect φ sa (stage-ord (fst a) (a .snd)) β = R .fst oβ = R .snd .fst ``` The index `β`, the underlying set `Lset β`, and the model element `c` are three different objects. Using `oβ : IsOrd β`, the term `LsetS β oβ` forms an element `c : S` from the stage and its constructibility proof. This is exactly the form required by `relativize`: its new quantifier bounds are object-language constants, so the stage must be represented inside the model rather than used only as an ambient set. ```agda c = LsetS β oβ ``` The parameter now lies in the reflection stage. `stage-mem` gives `fst a ∈ Lset sa`, while the reflection data give the strict ordinal membership `sa ∈ β`. Monotonicity of the constructible hierarchy combines them to obtain `fa∈β : fst a ∈ Lset β`. This does not identify `a` with an ordinal: `sa` and `β` are indices, whereas `fst a` is the set being placed in the higher stage. ```agda fa∈β : ⟨ fst a ∈ Lset β ⟩ fa∈β = Lset-mono {α = β} {β = sa} (R .snd .snd .fst) (stage-mem (fst a) (a .snd)) ``` Reflection is available only for environments whose entries lie in `Lset β`, so the membership conjunct in separation does essential work. Given `x ∈ˢ a`, transitivity combines this fact with `fa∈β` to put `fst x` in `Lset β`; `tt*` supplies the vacuous condition for the empty tail of the one-entry environment. The reflection component of `R` then gives `bridge`, a path from satisfaction of `φ` at `x` to satisfaction of its relativization. No comparison is asserted for arbitrary `x : S` outside `a`. ```agda bridge : (x : S) → ⟨ x ∈ˢ a ⟩ → ((x ∷ []) ⊨ φ) ≡ ((x ∷ []) ⊨ relativize c φ) bridge x x∈a = R .snd .snd .snd (x ∷ []) (transIn β x∈a fa∈β , tt*) ``` It remains to compare the two host predicates. In each direction, a proof of the common membership conjunct `x ∈ˢ a` is retained, and only the satisfaction proof is transported along `bridge` or its inverse. `⇔toPath` turns these two maps into a path between the proposition values at `x`, and `funExt` assembles the pointwise paths into `Q≡`. This is equality of predicates; no existential truncation is eliminated and no extensionality argument about candidate sets is performed here. ```agda Q≡ : (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) ≡ (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ relativize c φ)) Q≡ = funExt (λ x → ⇔toPath (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (bridge x x∈a) h }) (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (sym (bridge x x∈a)) h })) ``` ## Where the images live For every `x ∈ˢ a`, the hypothesis makes the dependent sum of related values `Σ y , (y ∷ x ∷ []) ⊨ φ` contractible. Its centre supplies a value and its contraction identifies every related value with that centre, so this step uses no host-level axiom of choice. `FunctionalImage` ranges over the small presentation `⟪ fst a ⟫`; for each small index it takes the least stage of the corresponding centre, and `boundingOrd` bounds all those stages by one ordinal `βimg`. Given an arbitrary member `x ∈ˢ a`, `∈-asFiber` returns a small index whose represented value is equal to the underlying set of `x`. That path moves the relation to the source represented by that index; contractibility then identifies its chosen centre with every related `y` and transports the common stage bound along that equality. The least-stage operation in this construction still depends on `lem`, although no choice axiom is used. ```agda module Images (a : S) (φ : Formula S 2) (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where open FunctionalImage a (λ x y → (y ∷ x ∷ []) ⊨ φ) fc public ``` ## Replacement The hypothesis of `hasReplacementL` makes each value fibre over a member of `a` contractible, while its conclusion makes the type of model sets realizing the image predicate contractible. These are different uniqueness statements: the first supplies one value for each source, and the second supplies one set containing exactly all such values. The source existential in the image predicate is propositionally truncated, so it records existence without exposing a chosen source. The `opaque` boundary changes only Agda's definitional reduction; it changes neither this statement nor its assumptions. ```agda opaque hasReplacementL : (a : S) (φ : Formula S 2) → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))) ``` The replacement proof now has exactly the two ingredients it needs. From the pointwise contractible fibres, `Images` provides an ordinal stage containing every value related to a member of `a`. Full separation on that stage, with the unary formula `imageFo`, gives a contractible type of sets realizing `BoundedImage`. The path `Q≡` proved below identifies that predicate with the image predicate `Image`, which has no stage condition; transport along `sym Q≡` therefore gives the required contractible type `SetOf Image`. This is full replacement for the arbitrary formula `φ`, rather than an application of the earlier bounded replacement theorem. Later, `L.Model` uses `hasSeparationL` and `hasReplacementL` as two of the twelve fields of `L⊨ZF`. Only after that ZF record has been assembled does `hasChoiceL L⊨ZF` supply the object-theoretic choice field used to form `L⊨ZFC`. Here `lem : LEM (ℓ-suc ℓ)` is the classical host assumption, while `fc` is the stated pointwise total-and-unique-value hypothesis. Projecting the centres already contained in `fc` requires no host-level axiom of choice, and the later choice field is a conclusion, not a premise of this proof. ```agda hasReplacementL a φ fc = subst (λ Q → isContr (SetOf Q)) (sym Q≡) (hasSeparationL (LsetS βimg βimg-ord) imageFo) where open Images a φ fc ``` The predicate required by replacement is stated directly in the variable order of the model axiom. A candidate `y` belongs to `Image` precisely when some `x ∈ˢ a` satisfies `φ` in the environment `y ∷ x ∷ []`, with the image first and the source second. The indexed existential in `hProp` uses propositional truncation: it retains the fact that a suitable source exists while forgetting which source was used. Thus contractibility of `SetOf Image` will say that there is a unique model set with exactly these image members; it does not say that the image itself has only one member. ```agda Image : S → hProp (ℓ-suc ℓ) Image y = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ``` To obtain the same condition by separation, it must be expressed as a unary object-language formula. In `imageFo`, the bounded existential ranges over members of the constant `a`; when its source witness `x` is introduced, the body is evaluated in the environment `x ∷ y ∷ []`. Since `φ` expects `y ∷ x ∷ []`, the body is `swapFo φ`, and `⊨-swap` proves that this change of positions preserves the intended relation. Only this newly added existential is bounded by `a`. The formula `φ` may still contain unbounded quantifiers, so `imageFo` need not be a Δ₀ formula and must be handled by full separation. ```agda imageFo : Formula S 1 imageFo = ∃̇∈ (con a) (swapFo φ) ``` Full separation is applied inside the model set representing the common stage, so the predicate it realizes contains two conditions. The first places `y` in `Lset βimg`; the second says that `y` satisfies `imageFo`. This first conjunct is the domain condition contributed by separation, rather than a bound on every quantifier of the formula. It is redundant for genuine image values because `range∈βimg` already places all of them in the common stage. The remaining proof shows that adding or removing this stage condition does not change the extension of the image predicate. ```agda BoundedImage : S → hProp (ℓ-suc ℓ) BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo) ``` The equality `Q≡` is obtained pointwise. For each candidate `y`, `into y` and `out y` prove the two implications between `Image y` and `BoundedImage y`; `⇔toPath` turns them into a path of proposition values, and `funExt` combines these paths into equality of predicates. The forward implication begins with a propositionally truncated source. `PT.rec` may inspect such a witness here because its target is the proposition underlying `BoundedImage y`, as certified by `snd (BoundedImage y)`. The witness is used only within that propositional target and cannot be returned as untruncated data. ```agda Q≡ : Image ≡ BoundedImage Q≡ = funExt (λ y → ⇔toPath (into y) (out y)) where into : (y : S) → ⟨ Image y ⟩ → ⟨ BoundedImage y ⟩ into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) → ``` Inside this permitted propositional elimination, suppose the source is `x`, with proofs `x ∈ˢ a` and `(y ∷ x ∷ []) ⊨ φ`. The range theorem `range∈βimg` supplies the first conjunct by placing `y` in the common stage. For the second conjunct, the same `x` is repackaged under propositional truncation. The reverse of the path `⊨-swap φ x y` transports satisfaction of `φ` at `y ∷ x ∷ []` to satisfaction of `swapFo φ` at `x ∷ y ∷ []`, which is exactly the body of `imageFo`. Thus the branch constructs both parts of `BoundedImage y` without extracting a source from the truncation. ```agda range∈βimg x x∈a y h , ∣ x , (x∈a , subst ⟨_⟩ (sym (⊨-swap φ x y)) h) ∣₁ } ``` For the reverse implication, the stage-membership component is simply discarded. Satisfaction of `imageFo` already contains, under propositional truncation, a source `x`, its membership in `a`, and satisfaction of `swapFo φ` at `x ∷ y ∷ []`. The map `PT.map` keeps the same source and membership proof inside the truncation while transport along `⊨-swap φ x y` changes the last component to satisfaction of `φ` at `y ∷ x ∷ []`. The result is `Image y`. Together with the forward implication this proves `Q≡`, and the transport in the defining equation above converts the set obtained by full separation into the unique set required by full replacement. No witness is selected during this comparison. ```agda out : (y : S) → ⟨ BoundedImage y ⟩ → ⟨ Image y ⟩ out y (_ , h) = PT.map (λ { (x , (x∈a , h')) → x , (x∈a , subst ⟨_⟩ (⊨-swap φ x y) h') }) h ``` ## Recap Full separation and full replacement arise from two reductions. Reflection for the chosen formula, on environments inside a stage containing the source set, turns its truth into that of a Δ₀ relativization; bounded separation then gives full separation. A pointwise contractible value fibre, the source set's small presentation, and ordinal bounding place every related value in one stage; full separation then collects the image and gives full replacement. Both results retain the single classical parameter `LEM (ℓ-suc ℓ)` and use no host-level axiom of choice. They later fill the separation and replacement fields of `L⊨ZF`; this chapter does not assemble the full ZF or ZFC record.