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