Separation and replacement, in full

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

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.

{-# 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

  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.

  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.

  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.

  ⊨-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.

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.

  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.

  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.

  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.

  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.

  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.

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.

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.

  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.

    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.

    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.

    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.

    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.

        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.

      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.