--- title: "Absoluteness" module: FOL.Absoluteness lang: en site: "Bedrock" description: "Absoluteness" stage: "First-order logic" reading_order: 10 canonical: https://bedrock.institute/en/FOL.Absoluteness.html html: FOL.Absoluteness.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Absoluteness.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics] routes: [common-foundations] translations: [https://bedrock.institute/zh/FOL.Absoluteness.md, https://bedrock.institute/ja/FOL.Absoluteness.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Absoluteness A formula is absolute when interpreting it in a transitive substructure gives the same truth value as interpreting it in the ambient structure. Here the substructure has carrier `𝒮 ↾ M`, whose elements are pairs consisting of an ambient element and evidence that it belongs to the class `M`; the ambient interpretation uses the same syntax after projecting those pairs with `fst`. Transitivity supplies the key step: if a bound belongs to `M`, then every member of that bound belongs to `M` as well. The chapter proves by induction that every Δ₀ formula has equal inner and outer truth values. Atomic formulas follow from agreement of term evaluation, connectives preserve the induction hypotheses, and transitivity is needed exactly when a bounded quantifier must turn an ambient member into an element of the substructure. The final results extend this equality to one-way laws: Σ₁ truth passes upward from the substructure, while Π₁ truth passes downward from the ambient structure. Structures here are proposition-valued: a `ZFStructure` has a carrier whose equality and membership take values in `hProp ℓ`, so a satisfaction statement is a proposition with an underlying type, and two satisfaction statements can be compared by path equality. Two further notions carry the mathematics. `Transitive` is the closure condition `y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M`: a member of an element of `M` is again in `M`. And `_↾_` restricts a structure to a class, taking as its new carrier the pairs of an element with evidence that it lies in the class; what changes is what counts as an element, while the relations are inherited along the first projection. ```agda {-# OPTIONS --cubical --safe --guardedness #-} module FOL.Absoluteness where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure; Transitive; _↾_ ) ``` On the syntactic side, formulas have constants `con` and variables `var` and the two bounded quantifiers `∀̇∈` and `∃̇∈`, whose range is the members of a term's value. The Lévy hierarchy enters through its inductive characterizations: `Δ₀` is the inductive class of formulas built from atomic membership and equality by the propositional connectives and the bounded quantifiers, with constructors named `δ-`. `Σ₁` and `Π₁` are built on top: either a Δ₀ formula, or an unbounded existential (respectively universal) whose matrix is again Σ₁ (respectively Π₁), witnessed by `σ-∃` and `π-∀`. These witnesses are exactly the induction data the absoluteness proof will consume. ```agda open import FOL.Syntax using ( Term; con; var; Formula; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ; Σ₁; σ-Δ₀; σ-∃; Π₁; π-Δ₀; π-∀ ) import FOL.Semantics ``` The semantics is generic, so the chapter will use it twice over the same syntax, once for each world. Three pieces of notation serve the proofs to come: `map` applies the first projection to a whole environment, `⇔toPath` turns two implications into a path of truth values, and the truncation machinery appears as `PT` because satisfaction of an unbounded existential is a merely-inhabited type, so transferring witnesses between the two worlds happens under truncation. ```agda open import Cubical.Data.Vec using ( map ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT ``` ## The setting: one syntax, two semantics Fix an ambient structure `𝒮` and a transitive class `M`; the inner world is the restriction `𝒮 ↾ M`, whose carrier `SM` consists of the members of `M`. The syntax takes `K := SM`: a constant in a formula must be a member of `M`, so the parameter discipline is enforced by the type. The same formula family then receives **two semantics**: evaluated outside, in `𝒮`, with constants interpreted through `fst`; and evaluated inside, in `𝒮 ↾ M`, with constants standing for themselves. Relativization is thus not a syntactic operation but two readings of one generic semantics; the superscripts `ᵛ` and `ᵐ` on the satisfaction symbols read "evaluated where". The section works under three fixed parameters: a structure `𝒮`, a class `M` valued in `hProp ℓ` on its carrier, and a proof `trans` of transitivity. The carrier `S` and the truth-valued relations `_∈ˢ_`, `_≈ˢ_` belong to `𝒮`; the hProp operations `⊓`, `⊔`, `⇒` interpret the connectives. Nothing about `M` is used yet except that it is a class; transitivity enters the proof of the theorem, not the definitions that state it. ```agda module Single {ℓ} (𝒮 : ZFStructure ℓ) (M : ZFStructure.S 𝒮 → hProp ℓ) (trans : Transitive 𝒮 M) where open ZFStructure 𝒮 ``` The carrier of the inner world is the Σ-type `SM`: a pair of an element of `S` with evidence that it lies in `M`. Since `𝒮 ↾ M` interprets its relations on first projections, an inner element and its `fst` image name the same inhabitant of `S` as far as `𝒮` is concerned. The generic semantics is then used twice over this carrier: once evaluating in the outer structure `𝒮`, once in the restriction `𝒮M`. The two readings share the syntax because both take constant domain `SM`; they differ only in the structure and in the constant interpretation. ```agda SM : Type ℓ SM = Σ[ x ∈ S ] (x ∈ᶜ M) 𝒮M : ZFStructure ℓ 𝒮M = 𝒮 ↾ M module SemV = FOL.Semantics 𝒮 ``` The outer reading uses the constant interpretation `ι := fst`: a constant naming a member of `M` denotes that member itself in `𝒮`. The fixed notation is `_⊨ᵛ_` for satisfaction in `𝒮` and `⟦_⟧ᵛ` for term values, and the environment notation `_^_` is available throughout. ```agda module SemM = FOL.Semantics 𝒮M open SemV using ( _^_ ) public open module V = SemV.At SM fst public renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ ) open module Mse = SemM.At SM id public ``` The inner reading uses `ι := id`: inside `𝒮 ↾ M`, a constant is the pair it names, and the relations of the restriction read off that pair's first projection. Hence an inner atomic statement `xm ∈ˢ ym` means exactly `fst xm ∈ˢ fst ym` in `𝒮`, which is why the two satisfaction relations can be compared at all. The notation is `_⊨ᵐ_` and `⟦_⟧ᵐ`, so each formula can be read both as `δ ⊨ᵐ φ` (inside) and as `(map fst δ) ⊨ᵛ φ` (outside). ```agda renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) ``` The two worlds differ only in how environments are read: an inner environment `δ : SM ^ n` names outer values through `fst`, so `map fst δ` is the corresponding outer environment. Two lemmas connect the term evaluation on the two sides. A constant evaluates to its own first projection on both sides, and a variable is a lookup in both worlds, so the dictionary is settled at the atoms. The first lemma commutes lookup with projection, pointwise along the vector: reading the `i`-th entry of the projected environment is the same as projecting the `i`-th entry. The proof is a case split on the index, `refl` at the head and recursion down the tail, since both `lookup` and `map` compute entry by entry. ```agda private lookup-fst : ∀ {n} (i : Fin n) (δ : SM ^ n) → lookup i (map fst δ) ≡ fst (lookup i δ) lookup-fst zero (m ∷ δ) = refl lookup-fst (suc i) (m ∷ δ) = lookup-fst i δ ``` The second lemma lifts this to terms: evaluating a term in the inner world and projecting gives its outer value under the projected environment. For a constant, both sides compute to `fst m` by the respective interpretations `id` and `fst`, so `refl` suffices. For a variable, the outer value is a lookup into `map fst δ`, which the first lemma rewrites into the projection of the inner lookup; `sym` places the equation in the required direction. Any term is built from these two cases, so the dictionary is complete. ```agda ⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : SM ^ n) → fst (⟦ t ⟧ᵐ δ) ≡ ⟦ t ⟧ᵛ (map fst δ) ⟦⟧-fst (con m) δ = refl ⟦⟧-fst (var i) δ = sym (lookup-fst i δ) ``` ## The theorem Absoluteness for Δ₀ is proved by structural induction on the Δ₀ witness. The atomic and connective cases are bookkeeping: atoms go through the term lemmas of the previous section, and each connective computes the whole truth value from the parts, so equality of the parts transports to equality of the whole. The bounded universal is the case where the mathematics happens. Outward, an outer member `x` of the bound must be repackaged for the inner semantics as a member of `M`; since the bound's value lies in `M`, `x ∈ ⟦ t ⟧` together with `⟦ t ⟧ ∈ᶜ M` yields exactly `x ∈ᶜ M` by transitivity. The reverse direction needs only the projection. The bounded existential is the dual argument, carried out under propositional truncation. Transitivity is used when the proof must turn a bare outer element into an inner element: in the inner-to-outer direction for the bounded universal, and in the outer-to-inner direction for the bounded existential. The statement is a path of truth values, not a mere implication: for every Δ₀ witness `d` certifying `φ` and every environment `δ` into `SM`, inner satisfaction `δ ⊨ᵐ φ` is equal, as a type, to outer satisfaction under the projected environment. In the atomic cases the term lemma evaluates both sides: `∈` reads the structure field `_∈ˢ_`, `≐` reads `_≈ˢ_`, and `cong₂` moves the equality of the two term values through the relation. On the connectives `∧`, `∨` and `⇒` the semantics is by `⊓`, `⊔` and `⇒`, so `abs₀` on the two subwitnesses, fed to `cong₂`, is the whole case: these operations are functions, hence preserve equality. ```agda abs₀ : ∀ {n} {φ : Formula SM n} → Δ₀ φ → (δ : SM ^ n) → (δ ⊨ᵐ φ) ≡ ((map fst δ) ⊨ᵛ φ) abs₀ (δ-∈ {t = t} {u}) δ = cong₂ _∈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ) abs₀ (δ-≐ {t = t} {u}) δ = cong₂ _≈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ) abs₀ (δ-∧ d e) δ = cong₂ _⊓_ (abs₀ d δ) (abs₀ e δ) ``` Absurdity needs no work: `δ-⊥` gives `⊥` on both sides, so the required path is `refl`. What remains are the two bounded quantifiers, where the ranges `⟦ t ⟧` live in the outer world but the inner quantification runs over pairs of a value with its membership evidence in `M`. The next blocks unpack one direction at a time. ```agda abs₀ (δ-∨ d e) δ = cong₂ _⊔_ (abs₀ d δ) (abs₀ e δ) abs₀ (δ-⇒ d e) δ = cong₂ _⇒_ (abs₀ d δ) (abs₀ e δ) abs₀ δ-⊥ δ = refl abs₀ (δ-∀∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd where ``` For `∀̇∈`, both directions are packaged by `⇔toPath` into one path. Two abbreviations are set up first: `tm` is the inner value of the bounding term, and `p` is the term lemma `fst tm ≡ ⟦ t ⟧ᵛ (map fst δ)` specialized to it, the bridge between the inner range (a pair) and the outer range (its first projection). ```agda tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩ ``` The forward direction takes an inner verifier `h` and must supply, for each outer `x` with `x ∈ˢ ⟦ t ⟧ᵛ (map fst δ)`, the body's outer truth. Here `x` is a bare element, not a member of `M`, so it must first be repackaged. The transport along `sym p` moves the membership evidence to the inner range `fst tm`, and then transitivity applies: `x ∈ fst tm` together with `fst tm ∈ᶜ M` gives `x ∈ᶜ M`, so `xm := x , trans hx' (snd tm)` is a legitimate inner element. Running `h` at `xm` gives the inner truth of the body, and the induction hypothesis `abs₀ d (xm ∷ δ)` transports it outward. This is the only step of the whole induction that consumes the hypothesis `trans`. ```agda fwd h x hx = let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in subst ⟨_⟩ (abs₀ d (xm ∷ δ)) (h xm hx') bwd : ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ ``` The backward direction runs the other way: an outer verifier `g` quantifies over bare elements, while the inner clause expects a pair `xm` with its membership evidence attached. The projection `fst xm` is the outer element, and the term lemma transports its membership from `fst tm` to `⟦ t ⟧ᵛ (map fst δ)`, exactly the form `g` expects. Calling `g` yields outer truth, and `abs₀ d (xm ∷ δ)` transported along `sym` brings it back inside. This direction needs no transitivity: the pair `xm` arrives with its evidence attached. ```agda bwd g xm hxm = subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) (g (fst xm) (subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm)) abs₀ (δ-∃∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd where ``` The existential case `∃̇∈` mirrors the universal one, with one structural difference: satisfaction of an existential is defined as a join over the carrier, the least truth value above all the per-element contributions, and a join of truncated statements lives under propositional truncation, so both directions operate via `PT.map`. The same abbreviations `tm` and `p` are in scope; the mathematics of repacking witnesses through the range is identical. ```agda tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩ ``` Forward, a truncated inner witness is a triple: an inner element `xm` in the range, its membership evidence, and the body's inner truth. The map sends it to `fst xm`, transports the membership outward along `p` into the shape `⟨ fst xm ∈ˢ ⟦ t ⟧ᵛ (map fst δ) ⟩`, and transports the body's truth outward through the induction hypothesis `abs₀ d (xm ∷ δ)`. The witness itself is used only inside the truncation, never extracted. ```agda fwd = PT.map λ { (xm , hxm , hφ) → fst xm , subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm , subst ⟨_⟩ (abs₀ d (xm ∷ δ)) hφ } bwd : ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ ``` Backward, an outer witness is a triple of a bare element `x`, its membership in the outer range, and the body's outer truth. The transport along `sym p` pulls the membership to the inner range, transitivity then certifies `x ∈ᶜ M` so that `xm` is an inner element, and the body's truth is transported inward through `sym (abs₀ d (xm ∷ δ))`. The truncated output is again assembled by `PT.map`, so no choice principle is invoked anywhere: the two bounded-quantifier cases hold with merely-inhabited witnesses on both sides. ```agda bwd = PT.map λ { (x , hx , hφ) → let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in xm , hx' , subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) hφ } ``` ## Σ₁ upward, Π₁ downward Beyond Δ₀, absoluteness becomes one-directional, and the directions are dual: a Σ₁ formula true inside is true outside, while a Π₁ formula true outside is true inside. The asymmetry comes from quantifier variance. A Σ₁ witness may be built by any finite string of unbounded existentials over a Δ₀ core, and an inner existential witness travels outward through `fst`. A Π₁ witness may likewise be built by unbounded universals, and an outer verifier is specialized, at each step, to `fst` of an inner element. No additional appeal to transitivity occurs in these unbounded steps; the Δ₀ base of each induction still rests on the absoluteness theorem, and hence on the transitivity hypothesis. In the Δ₀ base case, `abs₀ d δ` is a path between the inner and outer truth values, so `subst` carries a proof of the inner truth value along that path. No propositional truncation is introduced in this base case. The Σ₁ case `σ-∃` is an unbounded existential over the carrier, and its satisfaction is a truncated join, so `PT.map` acts on a truncated pair: an inner witness `xm` with the body's inner truth `h` is sent to the outer element `fst xm`, and the recursive call `σ₁-up s (xm ∷ δ) h` extends the environment with the full pair, keeping the witness inside until the base case discards the wrapper. ```agda σ₁-up : ∀ {n} {φ : Formula SM n} → Σ₁ φ → (δ : SM ^ n) → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ (map fst δ) ⊨ᵛ φ ⟩ σ₁-up (σ-Δ₀ d) δ = subst ⟨_⟩ (abs₀ d δ) σ₁-up (σ-∃ s) δ = PT.map λ { (xm , h) → fst xm , σ₁-up s (xm ∷ δ) h } π₁-down : ∀ {n} {φ : Formula SM n} → Π₁ φ → (δ : SM ^ n) ``` The downward law is its mirror. The Δ₀ case transports along `sym (abs₀ d δ)`, and the Π₁ case `π-∀` is an unbounded universal: given an outer verifier `h`, it is instantiated at `fst xm` for each inner element `xm`, and the recursive call proves the body at the extended environment. No truncation appears here, since satisfaction of a universal is a meet, the greatest truth value below all the per-element contributions, and it is verified explicitly by giving the verifier; and the unbounded steps use no transitivity, because unbounded quantifiers range over the whole carrier, where the pair construction and the projection are already available. ```agda → ⟨ (map fst δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩ π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ)) π₁-down (π-∀ s) δ h xm = π₁-down s (xm ∷ δ) (h (fst xm)) ``` ## Recap The boundary is exact. Under transitivity, Δ₀ truth agrees between `𝒮 ↾ M` and `𝒮`: `abs₀` gives a path of truth values for every Δ₀ witness. The bounded universal uses transitivity when passing from an inner verifier to arbitrary outer members of the bound; the bounded existential uses it when an outer witness must be admitted to the inner carrier. From this base, `σ₁-up` preserves Σ₁ truth upward and `π₁-down` preserves Π₁ truth downward. The reverse directions are unavailable in general: an arbitrary outer existential witness need not lie in `M`, while an inner universal verifier says nothing about outer elements outside `M`.