Constant relabelling

A first-order formula carries constant symbols from some domain K, but the symbols themselves are inert: only the interpretation function decides what they denote. This chapter studies what happens when a function f : K → K' renames every constant symbol, an action written mapFo f. Two questions are answered. First, does the meaning survive the renaming, in the precise sense that satisfaction under ι after renaming coincides with satisfaction under the composite interpretation ι ∘ f before renaming? Second, does the syntactic classification of a formula in the Lévy hierarchy survive, so that the Δ₀ witness, and more generally the Σₙ/Πₙ witness, can be transported along f? Both answers are yes, and both proofs are structural, mirroring the constructors of the syntax.

Take a formula over a constant domain K and rename its constants along a function f : K → K'. What the formula says then depends on which interpretation reads it: the target interpretation ι : K' → S, applied to the renamed formula, or the composite ι ∘ f, applied to the original. The semantic half of this chapter asks whether these two readings always agree, and the syntactic half asks whether a formula's classification in the Lévy hierarchy survives the renaming. Both are proved by structural induction, mirroring the constructors of the syntax.

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

module FOL.Manipulation.Relabelling where

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

The action under study is written mapTm f on terms and mapFo f on formulas: a function f : K → K' relabels each constant con k to con (f k) and leaves every variable untouched. Because it acts on constants only, every connective and every quantifier, bounded or unbounded, keeps its exact position, which is the reason the Lévy classification should survive. The classification itself is given by inductive witnesses: an inhabitant of Δ₀ φ is explicit data certifying that every quantifier in φ is bounded, one constructor per permitted shape, and Σₙ k φ and Πₙ k φ record the alternating unbounded blocks.

open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo; embed )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈

On the semantic side, a structure 𝒮 with carrier S reads a formula over K through an interpretation ι : K → S, yielding a satisfaction relation _⊨_ and term evaluation ⟦_⟧. The two readings to be compared therefore share the same syntax but differ in interpretation, and the proofs below keep them apart by carrying both side by side.

  ; Σₙ; σ-Δ₀; σ-Π; σ-∃; Πₙ; π-Δ₀; π-Σ; π-∀ )
import FOL.Semantics
import Cubical.Data.Empty as Empty

Meaning level

Renaming constants is a purely syntactic operation, so one must check that it does not disturb meaning. The precise statement is a commutation: for any map of constant domains f : K → K' and any interpretation ι : K' → S of the target domain, evaluating a relabelled formula under ι gives the same proposition as evaluating the original formula under the composite interpretation ι ∘ f. The proof runs by structural induction, with the base case supplied by term evaluation and the congruence lemmas of the proposition universe doing the rest.

Fix a proposition-valued ZF structure 𝒮 with domain S, a relabelling f : K → K', and an interpretation ι : K' → S of the target domain. The composite ι ∘ f is an equally good interpretation of the source domain, so we have two readings of the same formulas: the renamed formula under ι, and the original under ι ∘ f. The commutation problem is whether these readings give equal propositions.

module _ {ℓ} (𝒮 : ZFStructure ℓ) where

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

  module _ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K') (ι : K' → S) where

The atomic case already shows why the two readings must agree. Consider the formula t ∈̇ u: the first reading evaluates it as ⟦ mapTm f t ⟧ γ ∈ˢ ⟦ mapTm f u ⟧ γ, the second as ⟦ t ⟧∘ γ ∈ˢ ⟦ u ⟧∘ γ. The term lemma ⟦⟧-map gives ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ for every term, and both of its cases hold by refl: a relabelled constant con (f k) evaluates to ι (f k), which is exactly what the composite reading computes, and a variable ignores constants altogether.

    open At K' ι using ( _⊨_; ⟦_⟧ )
    open At K (λ k → ι (f k)) using () renaming ( _⊨_ to _⊨∘_ ; ⟦_⟧ to ⟦_⟧∘ )

    ⟦⟧-map : ∀ {n} (t : Term K n) (γ : S ^ n)
           → ⟦ mapTm f t ⟧ γ ≡ ⟦ t ⟧∘ γ
    ⟦⟧-map (con k) γ = refl

The satisfaction lemma ⊨-map lifts this agreement from terms to formulas, as paths in the proposition universe: (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ). For the atomic case t ∈̇ u, the two term paths from ⟦⟧-map are fed into the membership relation by cong₂ _∈ˢ_, producing the path between the two readings of the statement. Equality atoms work identically through ≈ˢ.

    ⟦⟧-map (var i) γ = refl

    ⊨-map : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ mapFo f φ) ≡ (γ ⊨∘ φ)
    ⊨-map (t ∈̇ u)  γ = cong₂ _∈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)
    ⊨-map (t ≐ u)  γ = cong₂ _≈ˢ_ (⟦⟧-map t γ) (⟦⟧-map u γ)

The propositional connectives are handled by congruence as well, because the structure interprets them by the corresponding logical operations: a path between the two readings of φ and one between the readings of ψ combine into a path for φ ∧̇ ψ through ⊓, and similarly for disjunction and implication. Falsity ⊥̇ contains no constants at all, so its two readings are the same value and the path is refl.

    ⊨-map (φ ∧̇ ψ)  γ = cong₂ _⊓_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ∨̇ ψ)  γ = cong₂ _⊔_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (⊨-map φ γ) (⊨-map ψ γ)
    ⊨-map ⊥̇        γ = refl

Quantifiers add one element x at the front of the environment. For an unbounded quantifier, the induction hypothesis gives a path for every x : S; function extensionality combines these pointwise paths, and cong transports the corresponding existential or universal quantification.

    ⊨-map (∃̇ φ)    γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))
    ⊨-map (∀̇ φ)    γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → ⊨-map φ (x ∷ γ)))

A bounded quantifier has one further component: ⟦⟧-map identifies the interpretation of its bounding term, while the induction hypothesis identifies the body. Congruence for implication or conjunction then combines the bound with the body before the outer quantifier is transported.

    ⊨-map (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))
    ⊨-map (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
      cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-map t γ)) (⊨-map φ (x ∷ γ))))

The commutation lemma already contains the parameter-free case, and the corollary below merely reads it off. A parameter-free formula is one whose constant domain is the empty type ⊥*; there are no constant symbols to interpret, so it can be embedded into formulas over any domain K by embed, and the two readings of its meaning must agree whatever K and ι are.

The inner module fixes an arbitrary target domain K and interpretation ι : K → S, then opens the satisfaction relation twice: once normally for formulas over K, and once under the name _⊨∅_ for formulas over the empty constant domain, where the interpretation is the function λ b → ι (Empty.rec* b). That function is legitimate because Empty.rec* is the eliminator of the empty type: an element of ⊥* would let one produce an element of any type, including S, so the interpretation never actually needs a value.

  module _ {ℓe ℓc} {K : Type ℓc} (ι : K → S) where

    open At K ι using ( _⊨_ )
    open At (⊥* {ℓe}) (λ b → ι (Empty.rec* b)) using () renaming ( _⊨_ to _⊨∅_ )

    embed-⊨ : ∀ {n} (φ : Formula (⊥* {ℓe}) n) (γ : S ^ n)
            → (γ ⊨ embed φ) ≡ (γ ⊨∅ φ)

The corollary embed-⊨ is then a direct instance of ⊨-map, with f taken to be the empty eliminator Empty.rec* viewed as a function ⊥* → K: for every parameter-free formula φ and environment γ, satisfaction of embed φ under ι is a path to satisfaction of φ in the ∅-marked reading. In words, embedding a parameter-free formula into a richer constant domain cannot change what it says.

    embed-⊨ = ⊨-map Empty.rec* ι

Levy witness level

Meaning is only half of the story. The Lévy hierarchy classifies formulas by quantifier structure, and this classification is represented by inductive witnesses: Δ₀ φ is explicit data certifying that every quantifier in φ is bounded, and Σₙ k φ / Πₙ k φ record the alternating unbounded blocks. Since relabelling replaces constant symbols but leaves every connective and quantifier, bounded or not, exactly where it was, the witnesses should survive, and mapΔ₀ shows this at the Δ₀ level before the mutual induction extends it upward.

Relabelling replaces each constant symbol but leaves every quantifier, bounded or not, exactly where it was, so a formula's quantifier shape is invariant under mapFo f. A Lévy witness records exactly that shape, so it should transport along any f. The type of mapΔ₀ states this at the base level: from a Δ₀ witness for φ it produces a Δ₀ witness for mapFo f φ. The atomic cases are immediate: a witness δ-∈ for t ∈̇ u carries no arguments, because an atomic formula has no quantifiers to bound, and mapFo f sends the formula to another atomic formula of the same shape, so δ-∈ again certifies it; the same holds for ≐.

mapΔ₀ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
        {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (mapFo f φ)
mapΔ₀ f δ-∈ = δ-∈
mapΔ₀ f δ-≐ = δ-≐
mapΔ₀ f (δ-∧ c d) = δ-∧ (mapΔ₀ f c) (mapΔ₀ f d)

The remaining constructors of Δ₀ are the connectives, falsity, and the bounded quantifiers. Each packages witnesses for its subformulas, and each recursive call transports a structurally smaller witness, with the constructor rebuilding the package over the renamed formula. Crucially, Δ₀ has no constructor for the unbounded quantifiers ∃̇ and ∀̇, only for the bounded ∀̇∈ and ∃̇∈, and those two cases recurse exactly like the connectives. Since mapFo f never turns a bounded quantifier into an unbounded one, every witness input has a case, which is what makes the definition total.

mapΔ₀ f (δ-∨ c d) = δ-∨ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f (δ-⇒ c d) = δ-⇒ (mapΔ₀ f c) (mapΔ₀ f d)
mapΔ₀ f δ-⊥ = δ-⊥
mapΔ₀ f (δ-∀∈ c) = δ-∀∈ (mapΔ₀ f c)
mapΔ₀ f (δ-∃∈ c) = δ-∃∈ (mapΔ₀ f c)

The Δ₀ level is the base of an inductively defined hierarchy: a Σₙ witness is either a Δ₀ witness, or a Π witness one level down, or a witness for an unbounded existential block, and dually for Πₙ. Because Σₙ and Πₙ are defined in terms of each other, the relabelling lemma for both must be proved at once, in a mutual block.

Above Δ₀, a Σₙ witness is either a Δ₀ witness, a Π witness one level down, or a witness for a block of unbounded existentials, and dually for Πₙ. The two forms are defined in terms of each other, so their transport lemmas are proved at once in a mutual block, with the same shape as mapΔ₀: from a Σₙ (respectively Πₙ) witness for φ, produce one for mapFo f φ at the same level k. A witness σ-Δ₀ d wraps a Δ₀ witness, and mapΔ₀ f d transports it at the leaves. A witness σ-Π p records a turn of the alternation, and is handled by calling the Π lemma, which is exactly why the two proofs must be mutually recursive.

mutual
  mapΣₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Σₙ k φ → Σₙ k (mapFo f φ)
  mapΣₙ f (σ-Δ₀ d) = σ-Δ₀ (mapΔ₀ f d)
  mapΣₙ f (σ-Π p)  = σ-Π (mapΠₙ f p)

The remaining Σ case σ-∃ s handles a block of unbounded existentials: the block stays a block under mapFo f, so the sub-witness s is transported by a recursive call to mapΣₙ itself. The Π side is the exact dual, with π-Δ₀ delegating to mapΔ₀ and π-Σ calling mapΣₙ for the alternation.

  mapΣₙ f (σ-∃ s)  = σ-∃ (mapΣₙ f s)

  mapΠₙ : ∀ {ℓc ℓd} {K : Type ℓc} {K' : Type ℓd} (f : K → K')
          {k n} {φ : Formula K n} → Πₙ k φ → Πₙ k (mapFo f φ)
  mapΠₙ f (π-Δ₀ d) = π-Δ₀ (mapΔ₀ f d)
  mapΠₙ f (π-Σ s)  = π-Σ (mapΣₙ f s)

The final case π-∀ p mirrors σ-Π, transporting the alternation within the Π side. Termination is not an additional argument here but a structural fact: each recursive call is applied to a structurally smaller component of the witness, with mapΔ₀ at the leaves of both recursions. The result is a single transport principle for the whole finite Lévy hierarchy: a formula's grade, as recorded by its inductive witness, is invariant under relabelling of constants.

  mapΠₙ f (π-∀ p)  = π-∀ (mapΠₙ f p)

Recap

This chapter established two invariance properties of the relabelling action mapFo f. Semantically, ⊨-map says that renaming constants commutes with satisfaction, in the precise sense that evaluating under ι after renaming equals evaluating under ι ∘ f before; the parameter-free embedding embed-⊨ follows as the special case where the source domain is empty. Syntactically, mapΔ₀, mapΣₙ and mapΠₙ say that the Lévy witnesses, which certify a formula's quantifier structure, can be transported along any relabelling. Together these mean that a formula can be moved between constant domains while both its meaning and its complexity witness move with it, which is what later chapters rely on when shifting between the empty domain and the domains of the constructible hierarchy.