Formulas pull back along a renaming of signatures

Proved

MoritaEquiv.Sig.Hom.IsRenaming.exists_formula_pullback

by Alien60 · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

logicmany-sorted-logicmodel-theory

Let $F:\Sigma\to\Sigma'$ be a renaming of many-sorted signatures, i.e. a signature morphism that is bijective on sorts and, for each arity, bijective on function and relation symbols. Let $\Gamma$ be a $\Sigma$ -context.

Statement. Every $\Sigma'$ -formula $\varphi$ in the context $F(\Gamma)$ is equivalent to the $F$ -translation of some $\Sigma$ -formula $\psi$ in context $\Gamma$ . That is, for every $\Sigma'$ -structure $M$ and every assignment $v$ , $M\models\varphi[v] \iff M\models F(\psi)[v]$ .

The proof is by induction on terms and formulas, pulling back each sort and symbol along the inverse of $F$ . Together with translation along $F$ this shows that a renaming identifies the two languages, which is needed whenever Morita equivalence is defined up to renaming of the common signature.

Formalization Note The context of $\varphi$ is written F.onSrt ∘ Γ; the equivalence is stated for all structures (no theory).

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Formulas can be pulled back along a renaming: if `F : L ⟶ L'` is a renaming (bijective on
sorts and on the symbols of each arity), every `L'`-formula whose context is the `F`-image of an
`L`-context `Γ` is equivalent, in every `L'`-structure, to the `F`-translation of an `L`-formula
in context `Γ`. -/
theorem Sig.Hom.IsRenaming.exists_formula_pullback {L L' : Sig} {F : L.Hom L'} (hF : F.IsRenaming)
    {n : ℕ} (Γ : Fin n → L.Srt) (φ : Formula L' (F.onSrt ∘ Γ)) :
    ∃ ψ : Formula L Γ, ∀ (M : Str L') (v : (i : Fin n) → M.carrier (F.onSrt (Γ i))),
      φ.Realize M v ↔ (ψ.onFormula F).Realize M v := by sorry

end MoritaEquiv

Source

T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556-582, https://arxiv.org/abs/1506.04675, §4-§5 (used for the second half of Theorem 5.2)

View graph