Relativization

Relativization replaces each unbounded quantifier by one bounded by a chosen constant. The transformed formula is Δ₀, and its ordinary satisfaction agrees with a semantics in which the original formula's unbounded quantifiers range only over members of the chosen set. The chapter builds three pieces in order: the rewriting operator itself, a witness that its output lies in the Δ₀ class of the Lévy hierarchy (see the chapter on that hierarchy for the definition of bounded formulas), and the correctness theorem identifying the meaning of the rewrite with bounded quantification over the chosen set. The setting is deliberately general: formulas may have constants from any type K, and the semantics may take values in the proposition universe hProp ℓ through a structure 𝒮, so the theorem applies wherever a genuine ZF-like structure is later supplied.

The setting: formulas may mention constants from an arbitrary type K, and satisfaction may take values in the proposition universe through a structure 𝒮. Consider a formula with an unbounded quantifier, for example ∃̇ (x ∈̇ y), which asks for some element of the whole universe belonging to y. Given a constant c, relativization rewrites the quantifier by supplying it with the bound con c: the result is ∃̇∈ (con c) (x ∈̇ y), which asks only for a member of y that lies in whatever the constant c names. No other part of the formula changes. This rewriting is purely syntactic; whether the rewritten formula still expresses the original intention is a separate semantic question, taken up in the correctness section.

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.Relativization where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

Rewriting one unbounded quantifier at one spot is easy; the task here is to do it uniformly at every depth of every formula, and to keep the bookkeeping afterward. The chapter's three pieces answer three questions. First, the operator relativize c performs the replacement itself, leaving already bounded quantifiers and their bounds untouched. Second, a witness Δ₀-relativize certifies that the output lies in the Δ₀ class of the Lévy hierarchy, that is, every quantifier occurring in it is bounded (the definition of bounded formulas is given in the chapter on that hierarchy). Third, the theorem relativize-correct connects the two readings: under any interpretation of the constants, the ordinary satisfaction of the rewritten formula agrees with a reading of the original one in which its unbounded quantifiers range only over the set named by c.

open import FOL.Syntax using
  ( con; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Semantics

The operator

relativize c leaves atoms and already bounded quantifiers unchanged, while replacing ∃̇ and ∀̇ by quantifiers bounded by con c. Because the bound is a constant, it passes beneath binders without any variable shifting. The definition is a plain recursion on the ten formula constructors, and its fixed point is a syntactic invariant worth stating before reading the code: after relativization, every quantifier in the result is bounded, and the only bounds introduced are occurrences of con c itself.

The signature fixes the data: a constant c drawn from any type K of constant symbols, and a formula φ of arity n, returning another formula of the same arity. The clauses for the atoms and the three binary connectives, and for falsity, do no rewriting at all; they only recurse into subformulas, preserving the connective structure. Relativization is thus depth-preserving: the only structural change it can make is at quantifier nodes.

relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} → Formula K n → Formula K n
relativize c (t ∈̇ u)  = t ∈̇ u
relativize c (t ≐ u)  = t ≐ u
relativize c (φ ∧̇ ψ)  = relativize c φ ∧̇ relativize c ψ
relativize c (φ ∨̇ ψ)  = relativize c φ ∨̇ relativize c ψ

The two unbounded clauses carry the whole point. ∃̇ φ becomes ∃̇∈ (con c) φ′ and ∀̇ φ becomes ∀̇∈ (con c) φ′, where φ′ is the relativization of the body: the quantifier now ranges only over elements of the constant con c. The two already bounded clauses keep their original bound term t untouched, precisely because it already restricts the quantifier; only the body is relativized. Note that the bound con c is a term, not a variable, so extending the environment with a freshly bound value never disturbs it: no de Bruijn style reindexing is needed anywhere in the transformation.

relativize c (φ ⇒̇ ψ)  = relativize c φ ⇒̇ relativize c ψ
relativize c ⊥̇        = ⊥̇
relativize c (∃̇ φ)    = ∃̇∈ (con c) (relativize c φ)
relativize c (∀̇ φ)    = ∀̇∈ (con c) (relativize c φ)
relativize c (∀̇∈ t φ) = ∀̇∈ t (relativize c φ)

This completes the case analysis: all ten constructors are covered, and the recursion is structural on the input formula, so relativize c φ is defined for every formula. Because the two bounded clauses merely recurse, the bounded quantifiers originally present in φ survive with their own bounds, and the new bounds are exactly the relativized images of the unbounded ones.

relativize c (∃̇∈ t φ) = ∃̇∈ t (relativize c φ)

Every unbounded quantifier became bounded and nothing else changed, so the result has no ∃̇ or ∀̇ constructors at all. In the terminology of the Lévy hierarchy chapter, that is exactly what it means to be Δ₀: the inductive family Δ₀ has one constructor per permitted shape, and none for the unbounded quantifiers. The function Δ₀-relativize assembles such a witness by recursion on φ, one line per constructor.

The statement quantifies over all formulas φ and produces Δ₀ (relativize c φ), a witness in the inductive family, not a Boolean flag. For atoms, the witnesses δ-∈ and δ-≐ are given outright: an atomic formula has no quantifiers, so membership in Δ₀ is immediate. The connective clauses combine witnesses with δ-∧, δ-∨ and δ-⇒, mirroring the closure rules of the class under its binary operations.

Δ₀-relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} (φ : Formula K n) → Δ₀ (relativize c φ)
Δ₀-relativize c (t ∈̇ u)  = δ-∈
Δ₀-relativize c (t ≐ u)  = δ-≐
Δ₀-relativize c (φ ∧̇ ψ)  = δ-∧ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c (φ ∨̇ ψ)  = δ-∨ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)

Falsity carries no quantifier, so δ-⊥ suffices. The decisive rows are again the quantifiers: where relativize changed an unbounded quantifier into a bounded one, Δ₀-relativize applies δ-∃∈ or δ-∀∈, the constructors reserved for bounded quantification, to the witness for the relativized body. A bounded quantifier of the original formula gets the same treatment on its own body. In every case the inductive hypothesis supplies the witness for the subformula, and the constructor lifts it through the surrounding connective or quantifier.

Δ₀-relativize c (φ ⇒̇ ψ)  = δ-⇒ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c ⊥̇        = δ-⊥
Δ₀-relativize c (∃̇ φ)    = δ-∃∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇ φ)    = δ-∀∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇∈ t φ) = δ-∀∈ (Δ₀-relativize c φ)

All ten cases are now covered, and the recursion on φ guarantees the witness exists for every input. This is the syntactic half of the chapter's promise: relativized formulas are not merely intuitively bounded, they carry an explicit Δ₀ certificate that later absoluteness and definability arguments can consume directly.

Δ₀-relativize c (∃̇∈ t φ) = δ-∃∈ (Δ₀-relativize c φ)

Correctness

The comparison semantics interprets the original formula while restricting only its unbounded quantifiers to the value of the chosen bound. Structural induction shows that this is exactly the ordinary semantics of the relativized formula. Two semantics are therefore in play: the standard one γ ⊨ _ from FOL.Semantics, and the auxiliary relation γ ⊨ᴬ _ defined here, which agrees with the standard one at every connective, atom, and bounded quantifier, and differs only at ∃̇ and ∀̇, where it adds the condition that the bound variable lies in the chosen set. The theorem to prove is the path (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ), so the two relations must land in a type with an identity type; this is why the module is parameterized by a proposition-valued structure 𝒮 and a constant interpretation ι.

To compare the two readings, fix a proposition-valued ZF structure 𝒮 with domain S, an interpretation ι assigning each constant symbol a carrier element, and a distinguished constant c. The standard semantics γ ⊨ _ and term evaluation ⟦_⟧ come from FOL.Semantics, for the given ι. To these data the section adds a companion relation γ ⊨ᴬ _, which interprets the original formula exactly as the standard semantics does, except that its unbounded quantifiers are restricted to a single carrier element A, the denotation ι c of the chosen constant. At atoms, connectives, falsity, and bounded quantifiers the companion is meant to agree with the standard semantics; it differs only where unbounded quantification is replaced by quantification inside A. The argument uses the proposition-valued relations of 𝒮 directly.

module Correct {ℓ} (𝒮 : ZFStructure ℓ)
               {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) (c : K) where

  open ZFStructure 𝒮
  open module Sem = FOL.Semantics 𝒮 using ( module At; _^_ )

The bound is named once and for all: A = ι c, the carrier element denoted by the chosen constant. The relation γ ⊨ᴬ φ takes an environment γ : S ^ n and a formula φ of the same arity n, and returns a proposition in hProp ℓ, just as the standard satisfaction does. The superscript ᴬ records that quantifiers are relativized to A; the clauses follow, and only the unbounded quantifier clauses will differ from the standard ones.

  open At K ι using ( _⊨_; ⟦_⟧ )

  A : S
  A = ι c

  infix  _⊨ᴬ_
  _⊨ᴬ_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ

The first five clauses copy the standard semantics verbatim: atoms become the structure's proposition-valued membership and equality applied to the denotations ⟦ t ⟧ γ and ⟦ u ⟧ γ, connectives become the logical operations ⊓, ⊔, ⇒, and falsity becomes ⊥. This is deliberate: at these shapes there is nothing to relativize, and making the clauses definitionally identical to the standard ones is what will let the corresponding correctness cases be proved by refl. The recursion is again structural, so ⊨ᴬ is total.

  γ ⊨ᴬ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ᴬ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ᴬ (φ ∧̇ ψ)  = (γ ⊨ᴬ φ) ⊓ (γ ⊨ᴬ ψ)
  γ ⊨ᴬ (φ ∨̇ ψ)  = (γ ⊨ᴬ φ) ⊔ (γ ⊨ᴬ ψ)
  γ ⊨ᴬ (φ ⇒̇ ψ)  = (γ ⊨ᴬ φ) ⇒ (γ ⊨ᴬ ψ)

The quantifier clauses are where the two semantics differ. For the unbounded existential, γ ⊨ᴬ (∃̇ φ) is the indexed join ∃[ x ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ): it ranges over all carrier elements x and conjoins the proposition-valued guard x ∈ˢ A. Dually, the unbounded universal uses ∀[ x ] P x with the implication guard x ∈ˢ A ⇒ _. The bounded clauses already restrict their quantifier to a term, evaluated in the original environment γ; their guards use ⟦ t ⟧ γ rather than A, and otherwise match the standard reading exactly.

  γ ⊨ᴬ ⊥̇        = ⊥
  γ ⊨ᴬ (∃̇ φ)    = ∃[ x ∶ S ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ)
  γ ⊨ᴬ (∀̇ φ)    = ∀[ x ∶ S ] (x ∈ˢ A) ⇒ ((x ∷ γ) ⊨ᴬ φ)
  γ ⊨ᴬ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ᴬ φ)
  γ ⊨ᴬ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ᴬ φ)

Correctness is then one structural induction: the standard meaning of relativize c φ equals the A-bounded meaning of φ. The atoms are refl; the two clauses the operator actually changes are exactly where the standard semantics of ∃̇∈ (con c) _ unfolds, by computation, to the companion's clause, since ⟦ con c ⟧ γ is A; everything else is congruence. The conclusion is a path in the proposition universe hProp ℓ, not a mere iff, so the two propositions are identified outright and can be transported along in later arguments.

The statement quantifies over both the formula φ and the environment γ, and asserts a path in the proposition universe hProp ℓ. Because relativize c left atoms untouched, the left side γ ⊨ (t ∈̇ u) computes to exactly the proposition ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ, which is what γ ⊨ᴬ (t ∈̇ u) is by definition; the same holds for equality and falsity, so those cases are proved by refl, meaning definitional equality, with no further step. The connective cases use cong₂ applied to the corresponding logical operation: since the subresults agree, the combined propositions agree.

  relativize-correct : ∀ {n} (φ : Formula K n) (γ : S ^ n)
                     → (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ)
  relativize-correct (t ∈̇ u)  γ = refl
  relativize-correct (t ≐ u)  γ = refl
  relativize-correct (φ ∧̇ ψ)  γ = cong₂ _⊓_ (relativize-correct φ γ) (relativize-correct ψ γ)

The existential case is the crux. On the left, relativize c (∃̇ φ) is ∃̇∈ (con c) φ′, and the standard semantics of a bounded existential is ∃[ x ] (x ∈ˢ ⟦ con c ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ′). But ⟦ con c ⟧ γ computes to A = ι c, so this expression is definitionally the ᴬ-clause for ∃̇ φ, once the inner satisfaction ⊨ φ′ is replaced by ⊨ᴬ φ using the induction hypothesis at the extended environment x ∷ γ. Formally, funExt converts the pointwise agreement over every x into agreement of the indexed families, cong transports it through the guard x ∈ˢ A ⊓ _, and the outer cong (λ P → ∃[ x ] P x) lifts the agreement of families to agreement of their joins. The universal case is the dual with ∀[ x ] P x and ⇒.

  relativize-correct (φ ∨̇ ψ)  γ = cong₂ _⊔_ (relativize-correct φ γ) (relativize-correct ψ γ)
  relativize-correct (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (relativize-correct φ γ) (relativize-correct ψ γ)
  relativize-correct ⊥̇        γ = refl
  relativize-correct (∃̇ φ)    γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    cong (λ q → (x ∈ˢ A) ⊓ q) (relativize-correct φ (x ∷ γ))))

The two already bounded clauses mirror the previous pair. Here relativize c kept the original bound term t, and ⊨ᴬ also guards the quantifier by ⟦ t ⟧ γ, so the guard never changes; only the body's satisfaction must be converted via the induction hypothesis at x ∷ γ, and the same funExt, inner cong, and outer cong (λ P → ∃[ x ] P x) or cong (λ P → ∀[ x ] P x) pattern applies. Note that the bound term is still evaluated in the original environment γ, matching the standard semantics of bounded quantification exactly.

  relativize-correct (∀̇ φ)    γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    cong (λ q → (x ∈ˢ A) ⇒ q) (relativize-correct φ (x ∷ γ))))
  relativize-correct (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⇒ q) (relativize-correct φ (x ∷ γ))))
  relativize-correct (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →

All ten cases are handled, and the recursion is on φ, so the proof is complete for every formula and environment. This closes the chapter's argument: relativization is a purely syntactic transformation whose output is Δ₀, and whose standard meaning in any proposition-valued ZF structure is quantification restricted to the chosen set. Later chapters can therefore relativize a definability condition to a set A, work with a Δ₀ formula, and read its satisfaction off from quantification inside A, all backed by this one induction.

    cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⊓ q) (relativize-correct φ (x ∷ γ))))

Recap

relativize produces a Δ₀ formula, Δ₀-relativize records that complexity bound, and relativize-correct identifies its meaning with quantification inside the chosen set. Together these give the standard set-theoretic device of restricting an arbitrary formula to a set: syntactically by bounding quantifiers with a constant naming the set, and semantically by the one induction proved here. Downstream, the Δ₀ certificate feeds absoluteness arguments, and the correctness path lets satisfaction of the relativized formula be replaced by bounded quantification over A wherever definability is analyzed.