BedrockSeparation and replacement, in full
The separation chapter carved with bounded formulas, and the reflection chapters turned an arbitrary formula into a bounded one at the price of naming a stage. Putting the two together pays the two remaining comprehension fields of the model, for formulas of any complexity.
The pattern is the same for both. Name a stage that reflects the formula and contains everything the field will run on. Apply the bounded instrument to the relativized formula, which is Δ₀. Then transport the answer along the reflection, which is only valid inside the stage, and so has to be guarded: the guard is the field's own hypothesis that the element lies in the argument, and the argument lies in the stage.
Replacement needs one thing more. Its predicate quantifies over an image element that nothing confines, and the relativized formula, having lost its unbounded quantifiers, is free to be satisfied by elements outside the stage where the reflection says nothing. The cure is to confine it explicitly: conjoin to the matrix the atom saying the image lies in the stage. True images satisfy it automatically, because the stage was chosen to contain them, so the conjunction changes no answer while removing every answer the reflection could not certify.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Axioms.Full {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( con; var; Formula; _∈̇_; _∧̇_ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧ ) open import FOL.Manipulation.Renaming using ( renameFo; module Sat ) open import FOL.Manipulation.Relativize using ( relativize; Δ₀-relativize ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans; Lset-mono ) open import L.Ordinal {ℓ} using ( boundingOrd; bound2 ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem ) open import L.Axioms.Separation {ℓ} lem using ( ReplImage; separateΔ₀; replaceΔ₀ ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.ReflectFo {ℓ} lem using ( mkReflect ) open import Cubical.Data.Unit using ( tt* ) open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) module Ren = Sat (hPropAlgebra (ℓ-suc ℓ)) 𝒮ʟ id
Two small tools
A stage is a transitive set, so membership in the argument puts an element in the stage as soon as the argument is there. That is the guard, and it is used at every transport below.
And the variable calculus is needed once. The model states replacement with the image first and the source second; the bounded instrument was written the other way round, since that is the order in which the recursion produces them. Exchanging two variables is an instance of renaming, and the correctness theorem says the environments agree, which for a transposition is two refls.
private transIn : (β : V ℓ) {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩ transIn β = layer-trans (Lset-layer β) swap : Fin 2 → Fin 2 swap zero = suc zero swap (suc _) = zero swapFo : Formula S 2 → Formula S 2 swapFo = renameFo swap swapAgrees : (x z : S) → Ren.Agrees swap (x ∷ z ∷ []) (z ∷ x ∷ []) swapAgrees x z zero = refl swapAgrees x z (suc zero) = refl ⊨-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
Reflect the formula at a stage containing the argument's own earliest stage, so that the argument is in the stage and, by transitivity, so is every element of it. Separate with the relativized formula, which is Δ₀ by construction. Then the two predicates agree pointwise: on the left the membership conjunct is in hand, so the element is in the stage, so the reflection applies and converts the second conjunct; on the right the same, backwards.
Predicates are what SetOf depends on, so the pointwise agreement is turned into a path of predicates by function extensionality and transported. The whole field is that transport applied to the bounded instrument.
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 φ)) where sa = stage (fst a) (a .snd) R = mkReflect φ sa (stage-ord (fst a) (a .snd)) β = R .fst oβ = R .snd .fst c = LsetS β oβ fa∈β : ⟨ fst a ∈ Lset β ⟩ fa∈β = Lset-mono {α = β} {β = sa} (R .snd .snd .fst) (stage-mem (fst a) (a .snd)) bridge : (x : S) → ⟨ x ∈ˢ a ⟩ → ((x ∷ []) ⊨ φ) ≡ ((x ∷ []) ⊨ relativize c φ) bridge x x∈a = R .snd .snd .snd (x ∷ []) (transIn β x∈a fa∈β , tt*) 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
Replacement's stage has to contain the images too, and functionality is what makes that possible: each member of the argument has exactly one image, so the images form a family indexed by the argument's member type, and the bounding lemma bounds their stages.
The image of a member is read off the centre of the contractible type functionality provides. It depends on the membership proof as well as the element, but only apparently: membership is a proposition, so equal elements have equal images, and the congruence lemma below is what lets an arbitrary element of the argument be identified with the indexed one that the bound was computed for.
module Images (a : S) (φ : Formula S 2) (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where Mem : Type (ℓ-suc ℓ) Mem = Σ[ x ∈ S ] ⟨ x ∈ˢ a ⟩ img : Mem → S img p = fc (p .fst) (p .snd) .fst .fst img-sat : (p : Mem) → ⟨ (img p ∷ p .fst ∷ []) ⊨ φ ⟩ img-sat p = fc (p .fst) (p .snd) .fst .snd img-cong : {p q : Mem} → p .fst ≡ q .fst → img p ≡ img q img-cong e = cong img (Σ≡Prop (λ w → snd (w ∈ˢ a)) e) img-uniq : (p : Mem) (y : S) → ⟨ (y ∷ p .fst ∷ []) ⊨ φ ⟩ → img p ≡ y img-uniq p y h = cong fst (fc (p .fst) (p .snd) .snd (y , h)) memS : ⟪ fst a ⟫ → Mem memS m = (⟪ fst a ⟫↪ m , isL-trans {x = fst a} {y = ⟪ fst a ⟫↪ m} fm∈fa (a .snd)) , fm∈fa where fm∈fa : ⟨ ⟪ fst a ⟫↪ m ∈ fst a ⟩ fm∈fa = ∈∈ₛ {a = ⟪ fst a ⟫↪ m} {b = fst a} .snd (∈ₛ⟪ fst a ⟫↪ m) private bImg = boundingOrd ⟪ fst a ⟫ (λ m → stage (fst (img (memS m))) (img (memS m) .snd)) (λ m → stage-ord (fst (img (memS m))) (img (memS m) .snd)) βimg : V ℓ βimg = bImg .fst βimg-ord : IsOrd βimg βimg-ord = bImg .snd .fst img∈βimg : (p : Mem) → ⟨ fst (img p) ∈ Lset βimg ⟩ img∈βimg p = subst (λ w → ⟨ fst w ∈ Lset βimg ⟩) (img-cong fib) (Lset-mono {α = βimg} {β = stage (fst (img (memS m))) (img (memS m) .snd)} (bImg .snd .snd m) (stage-mem (fst (img (memS m))) (img (memS m) .snd))) where m : ⟪ fst a ⟫ m = ∈-asFiber {a = fst (p .fst)} {b = fst a} (p .snd) .fst fib : memS m .fst ≡ p .fst fib = Σ≡Prop (λ w → (isL w) .snd) (∈-asFiber {a = fst (p .fst)} {b = fst a} (p .snd) .snd)
Replacement
The stage is asked to contain the argument's own stage and the bound on the images, and the reflection is taken for the transposed formula, since that is the order the instrument wants. The matrix handed over is the relativized transpose conjoined with the confinement atom, which is Δ₀ on both sides.
Functionality for that matrix then holds with no residue. Its centre is the image that functionality already provided, which satisfies the confinement because the stage contains it; and any other solution satisfies the confinement by assumption, hence lies in the stage, hence is a genuine solution of the original formula, hence is the same image. That is exactly what the confinement was added for: without it a solution outside the stage could not be ruled out, and uniqueness would fail.
The final transport is the same pointwise argument as for separation, now under the existential over members: forwards the image is confined by the bound, backwards it is confined by hypothesis, and in both directions the reflection and the transposition compose to carry the matrix across.
hasReplacementL : (a : S) (φ : Formula S 2) → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) → isContr (SetOf (λ y → ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)))) hasReplacementL a φ fc = subst (λ Q → isContr (SetOf Q)) (sym Q≡) (replaceΔ₀ a ψ dψ fc′) where open Images a φ fc sa = stage (fst a) (a .snd) bδ = bound2 sa βimg (stage-ord (fst a) (a .snd)) βimg-ord R = mkReflect (swapFo φ) (bδ .fst) (bδ .snd .fst) β = R .fst oβ = R .snd .fst δ∈β = R .snd .snd .fst c = LsetS β oβ fa∈β : ⟨ fst a ∈ Lset β ⟩ fa∈β = Lset-mono {α = β} {β = sa} (oβ .fst {x = bδ .fst} {y = sa} (bδ .snd .snd .fst) δ∈β) (stage-mem (fst a) (a .snd)) imgβ : (p : Mem) → ⟨ fst (img p) ∈ Lset β ⟩ imgβ p = Lset-mono {α = β} {β = βimg} (oβ .fst {x = bδ .fst} {y = βimg} (bδ .snd .snd .snd) δ∈β) (img∈βimg p) ψ : Formula S 2 ψ = relativize c (swapFo φ) ∧̇ (var (suc zero) ∈̇ con c) dψ : Δ₀ ψ dψ = δ-∧ (Δ₀-relativize c (swapFo φ)) δ-∈ bridge : (x z : S) → ⟨ x ∈ˢ a ⟩ → ⟨ fst z ∈ Lset β ⟩ → ((z ∷ x ∷ []) ⊨ φ) ≡ ((x ∷ z ∷ []) ⊨ relativize c (swapFo φ)) bridge x z x∈a fz∈β = sym (⊨-swap φ x z) ∙ R .snd .snd .snd (x ∷ z ∷ []) (transIn β x∈a fa∈β , (fz∈β , tt*)) fc′ : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ (x ∷ z ∷ []) ⊨ ψ ⟩) fc′ x x∈a = (img p , centre) , uniq where p : Mem p = x , x∈a centre : ⟨ (x ∷ img p ∷ []) ⊨ ψ ⟩ centre = subst ⟨_⟩ (bridge x (img p) x∈a (imgβ p)) (img-sat p) , imgβ p uniq : (r : Σ[ z ∈ S ] ⟨ (x ∷ z ∷ []) ⊨ ψ ⟩) → (img p , centre) ≡ r uniq (z , (hrel , fz∈β)) = Σ≡Prop (λ w → snd ((x ∷ w ∷ []) ⊨ ψ)) (img-uniq p z (subst ⟨_⟩ (sym (bridge x z x∈a fz∈β)) hrel)) Q≡ : (λ y → ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))) ≡ ReplImage a ψ Q≡ = funExt (λ z → ⇔toPath (fwd z) (bwd z)) where fwd : (z : S) → ⟨ ⋁ S (λ x → (x ∈ˢ a) ⊓ ((z ∷ x ∷ []) ⊨ φ)) ⟩ → ⟨ ReplImage a ψ z ⟩ fwd z = PT.map (λ { (x , (x∈a , h)) → let zβ = subst (λ w → ⟨ fst w ∈ Lset β ⟩) (img-uniq (x , x∈a) z h) (imgβ (x , x∈a)) in x , (x∈a , (subst ⟨_⟩ (bridge x z x∈a zβ) h , zβ)) }) bwd : (z : S) → ⟨ ReplImage a ψ z ⟩ → ⟨ ⋁ S (λ x → (x ∈ˢ a) ⊓ ((z ∷ x ∷ []) ⊨ φ)) ⟩ bwd z = PT.map (λ { (x , (x∈a , (hrel , fz∈β))) → x , (x∈a , subst ⟨_⟩ (sym (bridge x z x∈a fz∈β)) hrel) })
Recap
hasSeparationL and hasReplacementL are the model's two comprehension fields at 𝒮ʟ, for arbitrary formulas, with no hypothesis beyond the excluded middle. The frontier loses two of its four debts, and what remains is the power set and choice.
Both proofs are one shape: reflect, apply the bounded instrument, transport under a guard. The only asymmetry is the confinement atom, and the reason for it is worth remembering, because it is the one place where relativization is not harmless. Relativizing a formula weakens what it says about anything outside the stage, so a predicate that quantifies over an unconfined element must say where that element lives, or it will admit solutions the reflection never promised.