Separating example: the two theories are not Morita equivalent

Proved

MoritaEquiv.thm52_not_morita

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

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

The theories $T_1,T_2$ of the separating example are not Morita equivalent: no two finite chains of Morita extensions starting at $T_1$ and $T_2$ end in logically equivalent theories over a common signature (up to renaming).

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 5.2 (second half): the categorically equivalent theories
`Thm52.T1` and `Thm52.T2` are not Morita equivalent. Hence categorical equivalence does not
entail Morita equivalence. -/
theorem thm52_not_morita : ¬ MoritaEquivalent Thm52.T1 Thm52.T2 := 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), §5, Theorem 5.2 (second half of the proof)

Read-back

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

Over one sort and unary predicates $p_0,p_1,p_2,\dots$ , let $T_1=\{\exists x\,\forall y\,(y=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$ . Then $T_1$ and $T_2$ are not Morita equivalent: there are no finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ , $T_2\rightsquigarrow T_2'$ and signature map $F$ from the signature of $T_1'$ to that of $T_2'$ , bijective on sorts and on symbols of each profile, such that a structure is a model of $T_2'$ iff its $F$ -reduct is a model of $T_1'$ .

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