---
title: "Variable renaming"
module: FOL.Manipulation.Renaming
lang: en
site: "Bedrock"
description: "Variable renaming"
stage: "First-order logic"
reading_order: 13
canonical: https://bedrock.institute/en/FOL.Manipulation.Renaming.html
html: FOL.Manipulation.Renaming.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/Renaming.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Semantics]
routes: [fol-operations]
translations: [https://bedrock.institute/zh/FOL.Manipulation.Renaming.md, https://bedrock.institute/ja/FOL.Manipulation.Renaming.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Variable renaming

A map between finite variable contexts acts on terms and formulas by renaming free variables while leaving constants fixed. The accompanying agreement relation on environments gives one semantic theorem that covers weakening, exchange, and contraction.

The syntax chapter pointed out an absence: no substitution, no weakening. The quantifier clauses take bodies in an extended context directly, so the classical apparatus for moving variables around is unnecessary. What little variable motion the book does need is covered by one device: **renaming**, a map `ρ : Fin n → Fin m` pushed through a formula, with a single correctness theorem that handles weakening, exchange, and contraction in one stroke.

Suppose a formula has its free variables indexed by `n` slots, and we want to view it in a context of `m` slots. A map `ρ : Fin n → Fin m` tells us where each variable goes, and renaming applies it to every free variable of the formula. The only complication is the quantifiers: their bodies live in a context with one extra slot, so `ρ` must be extended beneath each binder in a way that leaves the bound variable alone.

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

module FOL.Manipulation.Renaming where

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

One correctness theorem then measures renaming: under a suitable relation between the old and new environments, the renamed formula denotes the same proposition as the original. Since the proposition is computed in an arbitrary proposition-valued set-theoretic structure, the theorem has exactly the generality of satisfaction itself, and the usual structural rules of sequent practice, weakening, exchange, and contraction, all fall out as particular choices of `ρ`.

```agda
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
```

## The syntactic layer

`renameTm` and `renameFo` push a map `Fin n → Fin m` through the syntax. Beneath a binder, `liftρ` fixes the newly bound variable and shifts the old variables through the given map.

Take a formula with a free variable under a bounded quantifier, say `∀̇∈ x₀ (var 1 ∈̇ var 0)` in a context of two slots: the bound variable is slot 0 of the body, and slot 1 of the body is the free variable 0 of the outside. A renaming `ρ : Fin n → Fin m` moves the outside variables; under the binder we need a map on `Fin (suc n) → Fin (suc m)` that sends the bound slot 0 to slot 0 and sends each old slot `suc i` to `suc (ρ i)`. That extension is `liftρ ρ`, and it guarantees the bound variable is never disturbed.

```agda
liftρ : ∀ {n m} → (Fin n → Fin m) → Fin (suc n) → Fin (suc m)
liftρ ρ zero    = zero
liftρ ρ (suc i) = suc (ρ i)
```

With the lifting in hand, renaming extends to terms and then to formulas by structural recursion. The type of `renameTm` states the whole idea: a term with `n` free-variable slots becomes a term with `m` slots. A constant `con k` names no free variable at all, so it passes through unchanged; constants belong to the alphabet, not to the context, and their interpretation is a separate matter. The only other term form is a variable, where `ρ` finally acts.

```agda
renameTm : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Term K n → Term K m
renameTm ρ (con k) = con k
```

For formulas the pattern continues: `renameFo` has the same shape, turning a formula over `n` slots into one over `m`. The atomic clauses rename their term arguments, so in our example `var 1 ∈̇ var 0` under the outer map becomes `var (ρ 1) ∈̇ var (ρ 0)` as far as the outside slots are concerned. The propositional connectives and falsity carry no variables of their own and are rebuilt recursively from the renamed subformulas.

```agda
renameTm ρ (var i) = var (ρ i)

renameFo : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Formula K n → Formula K m
renameFo ρ (t ∈̇ u)  = renameTm ρ t ∈̇ renameTm ρ u
renameFo ρ (t ≐ u)  = renameTm ρ t ≐ renameTm ρ u
renameFo ρ (φ ∧̇ ψ)  = renameFo ρ φ ∧̇ renameFo ρ ψ
```

The plain quantifiers are the first place where the recursive call changes: since the body lives in the extended context, the call passes `liftρ ρ` rather than `ρ`. This is exactly the discipline we described for the example: the bound slot stays at zero, and the outside renaming reaches the body only in shifted form.

```agda
renameFo ρ (φ ∨̇ ψ)  = renameFo ρ φ ∨̇ renameFo ρ ψ
renameFo ρ (φ ⇒̇ ψ)  = renameFo ρ φ ⇒̇ renameFo ρ ψ
renameFo ρ ⊥̇        = ⊥̇
renameFo ρ (∃̇ φ)    = ∃̇ renameFo (liftρ ρ) φ
renameFo ρ (∀̇ φ)    = ∀̇ renameFo (liftρ ρ) φ
```

The bounded quantifiers use both maps at once, and our example sits exactly here. For `∀̇∈ t φ`, the bound `t` lives in the outer context and is renamed with `ρ`, while the body `φ` is renamed with `liftρ ρ`. So `∀̇∈ x₀ (var 1 ∈̇ var 0)` under `ρ` becomes `∀̇∈ (renamed bound) (var (suc (ρ 0)) ∈̇ var 0)`: the reference to free variable 0 follows the renaming through its shift, and the bound occurrence of slot 0 is untouched. The syntactic layer is now complete; the next section asks whether the result means the same as what we started with.

```agda
renameFo ρ (∀̇∈ t φ) = ∀̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)
renameFo ρ (∃̇∈ t φ) = ∃̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)
```

## The semantic layer

`Agrees ρ γ δ` says that the two environments assign equal values to variables related by `ρ`. This condition survives extension beneath a binder, and structural induction then proves equal term denotations and equal satisfaction for renamed formulas.

Syntax alone cannot say whether a renaming preserves meaning; we need to compare environments. An environment is a vector of elements of the structure's carrier, of length matching the context: `γ : S ^ m` for the big context, `δ : S ^ n` for the small one. The question becomes: when do `γ` and `δ` count as the same assignment from the point of view of `ρ`?

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

  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝒮
```

The answer is the relation `Agrees ρ γ δ`: for every index `i` of the small context, `δ` at `i` and `γ` at `ρ i` must be equal elements, the equality being a path in the carrier. Note the direction of the lookup: `ρ` goes from the small context to the big one, so `δ` assigns to `i` exactly what `γ` assigns to `ρ i`. In our running example with `n = 2`, agreement on the variable `1` of the body reads `lookup (ρ 0) γ ≡ lookup 1 δ`, that is, the big environment must match the small one at the image position.

```agda
  open Sem using ( _^_ )
  open Sem.At K ι using ( _⊨_; ⟦_⟧ )

  Agrees : ∀ {n m} → (Fin n → Fin m) → S ^ m → S ^ n → Type ℓ
  Agrees ρ γ δ = ∀ i → lookup (ρ i) γ ≡ lookup i δ
```

The correctness theorem: a renamed formula in the big environment means the same as the original in the small one. Terms first, then the usual induction, every case a congruence, the binder cases stepping through `agrees∷`. Weakening (inserting an unused variable), exchange, and contraction are all instances, obtained by choosing `ρ`.

The theorem will go by induction on the formula, so agreement must survive the step under a quantifier. It does: if both environments are extended with the same element `x` at position zero, then `x ∷ γ` and `x ∷ δ` agree under `liftρ ρ`. At index zero both sides read `x` by computation, and at index `suc i` the demand reduces to the old `ag i`. This lemma `agrees∷` is the semantic counterpart of the syntactic lifting.

```agda
  agrees∷ : ∀ {n m} {ρ : Fin n → Fin m} {γ : S ^ m} {δ : S ^ n}
            (x : S) → Agrees ρ γ δ → Agrees (liftρ ρ) (x ∷ γ) (x ∷ δ)
  agrees∷ x ag zero    = refl
  agrees∷ x ag (suc i) = ag i
```

Everything now rests on the two theorems. For terms: evaluating `renameTm ρ t` in the big environment `γ` gives a path to evaluating `t` in the small environment `δ`, provided `γ` and `δ` agree under `ρ`. For formulas the analogous statement compares propositions of satisfaction. The hypothesis `Agrees ρ γ δ` is what makes the claim substantive: without any relation between the environments, no equality of denotations could hold.

```agda
  ⟦⟧-rename : ∀ {n m} (ρ : Fin n → Fin m) (t : Term K n)
```

The term proof is short because there is so little to a term. A constant denotes `ι k` independently of the environment, so the two evaluations are the same by `refl`. A variable `var i` denotes `lookup i δ` on the small side and `lookup (ρ i) γ` on the big side, and agreement at index `i` is exactly the path between them, so `ag i` closes the case. The real content is one level up, in the formula theorem.

```agda
              (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
            → ⟦ renameTm ρ t ⟧ γ ≡ ⟦ t ⟧ δ
  ⟦⟧-rename ρ (con k) γ δ ag = refl
  ⟦⟧-rename ρ (var i) γ δ ag = ag i

  ⊨-rename : ∀ {n m} (ρ : Fin n → Fin m) (φ : Formula K n)
```

The formula theorem states a path between two propositions: `γ ⊨ renameFo ρ φ` on the big side, `δ ⊨ φ` on the small side. Consider first the bounded quantifier of our example, whose body contains no further binder; the other cases follow the same two patterns, congruence or recursion, which we describe here. For an atomic formula, the term theorem gives paths between the denotations of the renamed and original terms, and `cong₂` transports those paths through membership or equality of sets. Likewise each connective case applies `cong₂` to the corresponding logical operation, and falsity needs only `refl`.

```agda
             (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
           → (γ ⊨ renameFo ρ φ) ≡ (δ ⊨ φ)
  ⊨-rename ρ (t ∈̇ u)  γ δ ag = cong₂ _∈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (t ≐ u)  γ δ ag = cong₂ _≈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (φ ∧̇ ψ)  γ δ ag = cong₂ _⊓_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
```

Under the unbounded existential `∃̇ φ`, satisfaction quantifies over all candidate elements `x` of the carrier, so the proof must show that the functions of `x` on the two sides are pointwise equal, which is where `funExt` enters. At each `x` the two environments are the extensions `x ∷ γ` and `x ∷ δ`, and by `agrees∷ x ag` they agree under `liftρ ρ`, which is precisely the induction hypothesis at the smaller formula. This is the point of the whole design: agreement was built to survive extension, so the recursive call goes through unchanged.

```agda
  ⊨-rename ρ (φ ∨̇ ψ)  γ δ ag = cong₂ _⊔_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ (φ ⇒̇ ψ)  γ δ ag = cong₂ _⇒_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ ⊥̇        γ δ ag = refl
  ⊨-rename ρ (∃̇ φ)    γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))
```

The unbounded universal `∀̇ φ` is the dual, using `∀[ x ] P x` in place of `∃[ x ] P x` with the same `funExt` and `agrees∷` steps. The bounded universal `∀̇∈ t φ` combines the two ingredients: satisfaction is `∀[ x ] P x` over `x` of the implication from `x ∈ˢ ⟦ t ⟧ γ` to the body's satisfaction. The bound contributes a `cong` through `x ∈ˢ_` fed by the term theorem, and the body contributes the recursive call at `liftρ ρ`; `cong₂ _⇒_` welds them into the required path between implications.

```agda
  ⊨-rename ρ (∀̇ φ)    γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))
  ⊨-rename ρ (∀̇∈ t φ) γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))
```

The bounded existential `∃̇∈ t φ` closes the induction in the mirror image: `∃[ x ] P x over `x`, the renamed bound `x ∈ˢ ⟦ t ⟧ γ` joined to the body satisfaction by `⊓`, and the same recursive call through `agrees∷`. Notice what was never used: injectivity of `ρ`. The theorem is stated for an arbitrary map `Fin n → Fin m`, so collapsing two variables onto one, as in contraction, is as admissible as spacing them out, as in weakening, or reordering them, as in exchange.

```agda
  ⊨-rename ρ (∃̇∈ t φ) γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))
```

## Recap

Variable renaming consists of the syntactic maps, environment agreement, and the theorem `⊨-rename`. Choosing the context map specializes this single interface to weakening, exchange, or contraction.