Two kinds of things: one sort with p, q vs two sorts

Proved

MoritaEquiv.example4_morita

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

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

The one-sorted theory $\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ is Morita equivalent to the empty theory in the signature with two sorts and no symbols.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Examples 1 and 4: "there are two kinds of things", said with two
predicates `p, q` partitioning one sort (`Ex1.T1`) or with two sorts and no axioms (`Ex1.T2`).
The theories are not definitionally equivalent (different sorts) but are Morita equivalent. -/
theorem example4_morita : MoritaEquivalent Ex1.T1 Ex1.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), §3, Example 1 and §4.3, Example 4

Read-back

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

Let $T_1$ be the theory over one sort with unary predicates $p,q$ and axioms $\exists x\,p(x)$ , $\exists x\,q(x)$ , $\forall x\,(p(x)\vee q(x))$ , $\forall x\,\neg(p(x)\wedge q(x))$ , and $T_2=\varnothing$ over two sorts with no function or relation symbols (all sorts of all structures nonempty). Then $T_1$ and $T_2$ are Morita equivalent: there are finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ , $T_2\rightsquigarrow T_2'$ and a 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