Translation of Σ⁺-formulas with old-sorted free variables

Proved

MoritaEquiv.translation

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

category-theorydefinabilitymany-sorted-logicmodel-theorymorita-equivalencephilosophy-of-sciencetheoretical-equivalence

Throughout: many-sorted first-order logic with nonempty sorts; $\mathrm{Mod}(T)$ has the models of $T$ as objects and elementary embeddings as arrows; $D$ is a Morita extension of the $\Sigma$ -theory $T$ (new product, coproduct, subsort and quotient sorts and explicitly defined symbols, with admissibility in every model of $T$ ), $T^+$ the extended theory and $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ the reduct functor. Every $\Sigma^+$ -formula $\varphi$ whose context consists of old sorts is $T^+$ -equivalent to (the image of) some $\Sigma$ -formula $\psi$ in the same context.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 4.3 / Corollary 4.1 (case of free variables of old sorts):
if `T⁺` is a Morita extension of `T`, every `Σ⁺`-formula `φ` whose free variables all have sorts
in `Σ` is `T⁺`-equivalent to (the image of) a `Σ`-formula `ψ` in the same variables. -/
theorem translation {L : Sig} {T : Theory L} (D : MoritaData L T) {n : ℕ} (Γ : Fin n → L.Srt)
    (φ : Formula D.sig (D.incl.onSrt ∘ Γ)) :
    ∃ ψ : Formula L Γ, ∀ (N : Model D.ext) (v : (i : Fin n) → N.str.carrier (D.incl.onSrt (Γ i))),
      φ.Realize N.str v ↔ (ψ.onFormula D.incl).Realize N.str 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 (numbering as in arXiv v1), §4.2, Theorem 4.3 and Corollary 4.1 (proof in the appendix)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\Sigma$ be a signature, $T$ a $\Sigma$ -theory, $D$ a Morita extension datum over $T$ with extended signature $\Sigma^+$ , extended theory $T^+$ and reduct functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (sorts nonempty; arrows are elementary embeddings). For every context $\Gamma$ of old sorts and every $\Sigma^+$ -formula $\varphi$ in context $\Gamma$ , there is a $\Sigma$ -formula $\psi$ in context $\Gamma$ such that for every model $N$ of $T^+$ and every assignment $v$ of $\Gamma$ in $N$ : $N\models\varphi[v]\iff N\models\psi[v]$ (with $\psi$ read in $\Sigma^+$ via the inclusion).

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph