---
title: "Constant relabelling"
module: FOL.Manipulation.Relabelling
lang: en
site: "Bedrock"
description: "Constant relabelling"
stage: "First-order logic"
reading_order: 14
canonical: https://bedrock.institute/en/FOL.Manipulation.Relabelling.html
html: FOL.Manipulation.Relabelling.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/Relabelling.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.LevyHierarchy, FOL.Semantics]
routes: [fol-operations]
translations: [https://bedrock.institute/zh/FOL.Manipulation.Relabelling.md, https://bedrock.institute/ja/FOL.Manipulation.Relabelling.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

```agda
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.

```agda
  ; Σₙ; σ-Δ₀; σ-Π; σ-∃; Πₙ; π-Δ₀; π-Σ; π-∀ )
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.

```agda
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.

```agda
    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 `≈ˢ`.

```agda
    ⟦⟧-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`.

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

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

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

```agda
  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.

```agda
    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 `≐`.

```agda
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.

```agda
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.

```agda
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.

```agda
  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.

```agda
  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.