Separating example: the two theories are categorically equivalent

Proved

MoritaEquiv.thm52_categorical

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

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

Over one sort and unary predicates $p_0,p_1,\dots$ , the theories $T_1=\{\exists^{=1}x\,(x=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$ have equivalent categories of models.

Preamble

import Mathlib
import Definitions.Def_MoritaEquiv_defs

open CategoryTheory

Formal statement

namespace MoritaEquiv

/-- Barrett–Halvorson, Theorem 5.2 (first half): the theories `T₁ = {∃=1 x (x = x)}` and
`T₂ = T₁ ∪ {∀y (q₀ y → qᵢ y) : i ∈ ℕ}` over one sort and countably many unary predicates have
equivalent categories of models (both are discrete with `2^ℵ₀` isomorphism classes). -/
theorem thm52_categorical : CategoricallyEquivalent 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 (first 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 the categories $\mathrm{Mod}(T_1)$ and $\mathrm{Mod}(T_2)$ (models in nonempty carriers, arrows elementary embeddings) are equivalent.

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