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.

{-# 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 ρ.

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.

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.

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.

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.

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.

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 ρ?

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.

  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.

  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.

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

              (γ : 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.

             (γ : 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.

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

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

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