Model Theory

Motivation: categoricity transfer beyond first-order logic

A class of structures is categorical in a cardinal $\lambda$ if it has exactly one model of size $\lambda$ up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with $H(K)=\beth_{(2^{\mathrm{LS}(K)})^+}$ (the Hanf number for existence of arbitrarily large models), categoricity in some $\lambda\ge H(K)$ should imply categoricity in every $\mu\ge H(K)$. Deciding which form holds is a central question in non-elementary model theory.

Timeline

• 1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
• 1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
• 1990 — Hart and Shelah show categoricity in $L_{\omega_1,\omega}$ can stop at $\aleph_k$ while holding for $\aleph_0,\dots,\aleph_{k-1}$, using finite-support group constructions (Israel J. Math. 1990).
• 1999 — Shelah proves categoricity transfer for AECs with amalgamation and records $H(K)$ as the existence bound (APAL 1999).
• 2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
• 2017 — Vasey proves downward transfer from a successor cardinal $\ge H(K)$ under amalgamation and tameness (APAL 2017).
• 2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
• 2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
• 2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
• 2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with $\mathrm{LS}(K)=\aleph_0$, categorical on a tail but with two nonisomorphic models at $H(K)=\beth_{\omega_2}$; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Work with relational structures in a finitary relational language $L$ (a set of relation symbols, each with a finite arity). An abstract elementary class is a class $K$ of $L$-structures with a relation $M\preceq_K N$ ("strong substructure") such that: $\preceq_K$ is a partial order on $K$ refining substructure; $K$ and $\preceq_K$ are closed under isomorphism; coherence holds ($M_0\subseteq M_1$, $M_0\preceq_K M_2$, $M_1\preceq_K M_2$ imply $M_0\preceq_K M_1$); unions of $\preceq_K$-chains are in $K$, are $\preceq_K$-extensions of each member, and are $\preceq_K$-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number $\mathrm{LS}(K)\ge\aleph_0+|L|$, the least $\theta$ such that every subset $A$ of a model $M$ lies in some $N\preceq_K M$ with $|N|\le|A|+\theta$.

$K$ is categorical in $\mu$ if it has a model of size $\mu$ and any two models of size $\mu$ are isomorphic. The beth numbers are $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits. CH is $2^{\aleph_0}=\aleph_1$.

Formalization targets

Goal: the CH counterexample (Theorem 1.1)

Assume CH. There is a countable finitary relational language $L$ and an AEC $K$ in $L$ such that

$$\mathrm{LS}(K)=\aleph_0,\qquad \beth_{\omega_2}=H(K)=\beth_{(2^{\aleph_0})^+},$$

$K$ has two nonisomorphic models of cardinality $\beth_{\omega_2}$, and, with $\Lambda=\beth_{(2^{\aleph_1})^+}$,

$$K\ \text{is categorical in every cardinal } \mu\ge\Lambda .$$

Hence $\Lambda^+>H(K)$ is a categoricity cardinal from which downward transfer to $H(K)$ fails, while eventual categoricity holds for this $K$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.

Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.

Difficulty

Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound $\beth_{\omega_2}$ while categoricity holds on a tail, with $\mathrm{LS}(K)=\aleph_0$. One must build two nonisomorphic models at $\beth_{\omega_2}$ and simultaneously rule out any two nonisomorphic models above $\Lambda$, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.

Formalization scope

• Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; $L:\mathbb N\to$ Type with $\Sigma_n L_n$ countable.
• ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
• HasLSNumber ℵ₀ asserts both that $\aleph_0$ is a Löwenheim–Skolem bound and that it is the least one.
• hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
• Categorical μ includes existence of a model of size $\mu$; TwoModels asks for two nonisomorphic models of the given size.
• CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.

Selected references

• M. Morley, Categoricity in power, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0175782-0
• K. Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Nat. Acad. Sci. USA (1938). https://doi.org/10.1073/pnas.24.12.556
• B. Hart and S. Shelah, Categoricity over P for first order T or categoricity for φ∈L_{ω1ω} can stop at ℵ_k while holding for ℵ_0,…,ℵ_{k−1}, Israel J. Math. (1990). https://doi.org/10.1007/BF02807869
• S. Shelah, Categoricity for abstract classes with amalgamation, Ann. Pure Appl. Logic (1999). https://doi.org/10.1016/S0168-0072(98)00016-5
• S. Vasey, Downward categoricity from a successor inside a good frame, Ann. Pure Appl. Logic (2017). https://doi.org/10.1016/j.apal.2016.10.003
• W. Boney and S. Vasey, A survey on tame abstract elementary classes, 2017. https://arxiv.org/abs/1512.00060
• A. Kolesnikov and C. Lambie-Hanson, The Hanf number for amalgamation of coloring classes, J. Symb. Logic (2016). https://doi.org/10.1017/jsl.2015.48
• J. Šaroch and J. Trlifaj, Deconstructible abstract elementary classes of modules and categoricity, Bull. London Math. Soc. (2024). https://doi.org/10.1112/blms.13172
• C. Espíndola, A complete classification of categoricity spectra of accessible categories with directed colimits, preprint, 2023. https://arxiv.org/abs/2301.13167
• OpenAI, A CH obstruction to a prescribed categoricity threshold, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf

Motivation

When are two scientific theories "the same theory in different words"? Philosophers of science have used two formal criteria. Definitional equivalence (Glymour) is strict: it requires a common definitional extension and therefore cannot relate theories with different numbers of sorts. Categorical equivalence (Halvorson, Weatherall) is liberal: it asks only that the categories of models be equivalent. It has been applied to classical mechanics, electromagnetism and Newtonian gravitation (Weatherall 2016; survey in Weatherall 2019).

Barrett and Halvorson (2016) proposed Morita equivalence as a syntactic criterion between these two. It allows definitions of new sorts (products, coproducts, subsorts, quotients) in addition to the usual definitions of new predicates and function symbols. Their main results place the new criterion strictly between the other two:

• Morita equivalence implies categorical equivalence (their Theorem 5.1).
• The converse fails (their Theorem 5.2).

This mission formalizes that comparison: the semantic core of Morita extensions, the implication, the separating example, and the paper's motivating "two kinds of things" example.

Setting

A signature $\Sigma$ (Sig) consists of a type of sorts, function symbols $f : \sigma_1\times\dots\times\sigma_m\to\sigma$ and predicate symbols $p\subseteq\sigma_1\times\dots\times\sigma_m$. Formulas (Formula L Γ) are built in a typed context $\Gamma$ from $\bot$, $=$, predicates, $\to$ and $\forall$. A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory $T$ is a set of formulas in context, each read as its universal closure; a model of $T$ is a structure satisfying them all.

The category $\mathrm{Mod}(T)$ (Model T) has the models of $T$ as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories $T_1,T_2$ are categorically equivalent (CategoricallyEquivalent) if $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$.

A Morita extension of a $\Sigma$-theory $T$ (MoritaData L T) adds to $\Sigma$:

• new sorts, each with its defining symbols:
  • a product $\sigma$ of $\sigma_1,\sigma_2$, with projections $\pi_1,\pi_2$;
  • a coproduct, with injections $\rho_1,\rho_2$;
  • a subsort cut out by a $\Sigma$-formula $\varphi(x)$, with an injection $i$;
  • a quotient by a $\Sigma$-formula $\varphi(x_1,x_2)$, with a projection $\varepsilon$;
• new predicates and function symbols, each explicitly defined by a $\Sigma$-formula.

Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension $T^+$ (D.ext) is $T$ together with these axioms. Each definition must satisfy its admissibility condition in every model of $T$:

Definition	Condition
subsort	$\exists x\,\varphi(x)$
quotient	$\varphi$ is an equivalence relation
function symbol	$\forall x\,\exists!y\,\varphi(x,y)$

The reduct gives a functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (D.proj).

$T_1$ and $T_2$ are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ and $T_2\rightsquigarrow T_2'$ (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.

Formalization targets

Goal: Morita equivalence implies categorical equivalence

$$T_1 \text{ Morita equivalent to } T_2 \;\Longrightarrow\; \mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2).$$

Milestones

1. Unique expansion. Every model $M$ of $T$ has an expansion $N\models T^+$ with $\Pi N\cong M$, and any two such expansions are isomorphic.
2. $\Pi$ is faithful.
3. $\Pi$ is full.
4. Conservativity. For every $\Sigma$-formula $\alpha$: $T\models\alpha$ iff $T^+\models\alpha$.
5. Translation. Every $\Sigma^+$-formula whose free variables all have old sorts is $T^+$-equivalent to a $\Sigma$-formula.
6. Two kinds of things. $T_1=\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ over one sort is Morita equivalent to the empty theory over two sorts.
7. Separating example, first half. $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\}$, over one sort and countably many unary predicates, are categorically equivalent.
8. Separating example, second half. These two theories are not Morita equivalent.

Milestones 1–3 together say that $\Pi$ is an equivalence of categories. Milestones 6–8 are not needed for the goal; they record the paper's examples, which show that Morita equivalence relates theories with different numbers of sorts and is strictly stronger than categorical equivalence.

Significance

The result itself. The goal makes Morita equivalence a syntactic sufficient condition for categorical equivalence: an explicit dictionary of definitions yields an equivalence of model categories. Milestone 8 shows the converse fails, so categorical equivalence is strictly weaker. Milestone 6 shows that Morita equivalence, unlike definitional equivalence, can relate theories with different numbers of sorts. Together these locate the criterion that later philosophy-of-physics work uses to compare formulations with different ontologies, such as different numbers of kinds of objects.

Formalizing it. The results are proved on paper and, as far as is known, have no machine-checked proofs. Mathlib's ModelTheory library is single-sorted, so none of this is available there. The mission produces a reusable many-sorted first-order logic with:

• syntax, semantics and signature maps;
• elementary embeddings and the category of models;
• Morita extensions with their reduct functors.

The paper's arguments for conservativity and translation are informal in places; for example, the translation in the appendix uses coding of new-sorted variables. A formal proof fixes these details.

Difficulty

The obvious route to the goal composes the reduct functors along the chains. The work lies in showing that each reduct is an equivalence when the arrows are elementary embeddings.

• Fullness. An elementary embedding of reducts extends uniquely to the new sorts. Showing that the extension is again elementary requires the translation of Milestone 5: every $\Sigma^+$-formula has to be pulled back to a $\Sigma$-formula, including formulas that quantify over the new sorts.
• Coproduct and quotient sorts. Quantifiers over these sorts must be eliminated in favour of quantifiers over the old sorts.

For Milestone 8 the difficulty is reversed. One must rule out every pair of chains, including chains that introduce arbitrary new sorts. The paper's proof argues with a single common Morita extension. The definition, however, allows chains, and the paper notes that a chain need not collapse to a single extension. The argument must therefore be run through conservativity and translation along each chain.

Formalization scope

• Self-contained logic. Signatures have dependent arities (Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.
• Theories. A theory is a Set (Axiom L), each axiom being a formula in context read as its universal closure. Because sorts are nonempty, this agrees with the sentence version.
• Nonempty sorts. Every structure has nonempty carriers. This is the paper's convention, and without it Milestone 6 is false: the empty theory over two sorts would have models with an empty sort.
• Morita extensions are built, not recognized. MoritaData L T lists the new sorts and symbols and their defining $\Sigma$-formulas. The signature $\Sigma^+$ (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of $T$. Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.
• A common signature up to renaming. MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of $T_2'$ iff its F-reduct is a model of $T_1'$.
• Universes. Models live in Type.
• Separating example. The paper writes $T_2$ with fresh symbols $q_i$; here $T_1$ and $T_2$ share the signature with predicates $p_i$, which only renames symbols.
• No trivialization. None of the targets holds vacuously: Morita extensions require genuine admissibility proofs, and the arrows are elementary embeddings, not arbitrary maps. Milestone 6 needs explicit chains and an explicit renaming, with arity casts.

A complete development will need:

• the substitution and weakening lemmas for de Bruijn formulas;
• the realization of signature maps;
• the construction of expansions;
• a translation function from $\Sigma^+$-formulas to $\Sigma$-formulas.

These pieces are reusable for any later work on interpretations or theoretical equivalence. Alternative proofs of Milestone 8, for example by counting finitely axiomatized subtheories, are welcome.

Selected references

• T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556–582. arXiv:1506.04675. Source of all targets: §3–§5 and the appendix; Example 4 and Theorems 4.1–4.3, 5.1, 5.2.
• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. arXiv:1411.5757.
• J. O. Weatherall, Theoretical Equivalence in Physics, Philos. Compass 14 (2019). arXiv:1810.08192.
• H. Halvorson, The Logic in Philosophy of Science, Cambridge University Press, 2019. doi:10.1017/9781316275603.