Removing the nonforking-existence hypothesis from the no-Ehrenfeucht theorem for NSOP₁ theories

A theorem of Kim (2019) states that a countable complete NSOP₁ theory satisfying nonforking existence, with no finite tuple of own preweight ω, has either exactly one or infinitely many countable models — extending the classical Lachlan–Herwig–Kim line of results on countable models of stable and simple theories to the NSOP₁ theories, a strict enlargement of the simple theories and the largest class in this hierarchy for which an independence calculus generalizing forking — Kim-independence — is known. The source paper conjectured that every NSOP₁ theory satisfies nonforking existence, so that the hypothesis would be unnecessary. That conjecture has since been refuted: Mutchnik (2024) constructed an NSOP₁ theory without the existence axiom, while Kim–Kim–Lee (2025) proved that the Kim-forking analogue of existence does hold in all NSOP₁ theories — so the conjecture fails only in its classical forking reading. This leaves open the source paper's second question, which is the subject of this problem: does Kim's theorem hold for arbitrary countable NSOP₁ theories, with no independence-theoretic hypothesis at all? An affirmative answer extends the weight/preweight mechanism to the entire NSOP₁ class; a negative answer produces the first known Ehrenfeucht theory without the strict order property, refuting Conjecture 1 of the Pillay–Tanović survey (2026).

Background

For a complete theory $T$ in a countable language, $I(\omega,T)$ denotes the number of nonisomorphic countable models of $T$. It is a classical fact that $I(\omega,T)$ is never 2, that every finite value $n>2$ is realized by some theory, and that the only possible infinite values are $\aleph_0$, $\aleph_1$ and $2^{\aleph_0}$; theories with $1<I(\omega,T)<\omega$ are called Ehrenfeucht theories, after Ehrenfeucht's example with exactly 3 countable models. Every known Ehrenfeucht theory has the strict order property (SOP): some formula defines a partial order with infinite chains on a power of a model. Whether this is necessary is Conjecture 1 of the Pillay–Tanović survey — every Ehrenfeucht theory has the strict order property — and it is a central open problem of the countable-models program, adjacent to Vaught's conjecture (the assertion that $I(\omega,T)$ is always either at most countable or equal to $2^{\aleph_0}$).

The dividing lines: a complete theory is stable (no formula linearly orders an infinite sequence of tuples, so that few types are realized over any set of parameters), simple (forking satisfies the full independence calculus, a broad generalization of stability), or NSOP₁ according to which combinatorial properties it avoids; each class contains the previous one strictly, and NSOP₁ — which strictly contains the simple theories — is the largest class in this hierarchy for which a general independence calculus, Kim-independence, is known. NSOP₁ is defined by avoiding SOP₁: $T$ has SOP₁ if some formula $\varphi(x,y)$ has parameters $(c_\eta)_{\eta\in 2^{<\omega}}$ such that every branch $\{\varphi(x,c_{\beta\upharpoonright n}):n<\omega\}$ is consistent, while $\{\varphi(x,c_{\alpha^\frown 1}),\varphi(x,c_\gamma)\}$ is inconsistent whenever $\alpha^\frown 0\unlhd\gamma$. All simple theories are NSOP₁, but NSOP₁ also contains unstable theories.

Independence notions. In stable and simple theories the canonical independence relation is forking: a formula $\varphi(x,b)$ divides over a set $A$ if some $A$-indiscernible sequence starting with $b$ makes $\{\varphi(x,b_i)\}_{i<\omega}$ inconsistent, and forking is the finite-disjunction closure. The existence axiom says that no complete type $p(x)\in S(A)$ forks over its own domain $A$ — equivalently, every type has a global nonforking extension. All stable and all simple theories satisfy existence. In NSOP₁ theories the correct analogue is Kim-independence $\downarrow^K$ (Kaplan–Ramsey): a formula Kim-divides over a model $M$ if some Morley sequence over $M$ — an $M$-indiscernible sequence $(b_i)$ with $b_i\downarrow_M b_{<i}$ for all $i$ — witnesses the inconsistency; Kim-forking is again the finite-disjunction closure. Over models, $\downarrow^K$ satisfies symmetry, the independence theorem and Kim's lemma in every NSOP₁ theory (Kaplan–Ramsey), and is transitive (Kaplan–Ramsey 2021). Dobrowolski–Kim–Ramsey extended the whole theory over arbitrary sets — Kim's lemma for Kim-dividing over sets, symmetry, extension, the chain condition, and the equality of Kim-dividing and Kim-forking — but only under the existence axiom. In NSOP₁ theories without existence these results do not apply.

Own preweight. Following Kim (2019), with Kim-forking over sets as defined by Dobrowolski–Kim–Ramsey (which applies verbatim in any theory), a finite tuple $c$ has own preweight $\omega$ if there is a sequence $(b_i)_{i<\omega}$ of realizations of $\operatorname{tp}(c)$ such that $b_i\downarrow^K_\emptyset b_{<i}$ for every $i$ and $\operatorname{tp}(c/b_i)$ Kim-forks over $\emptyset$ for every $i$: the tuple Kim-forks with countably many mutually Kim-independent conjugates of itself. Under the existence axiom, symmetry of $\downarrow^K$ makes this equivalent to the formulation $b_i\not\downarrow^K_\emptyset c$ used in some accounts. Note that Kim-dividing over $\emptyset$ is witnessed by nonforking Morley sequences over $\emptyset$, so in a theory where no such sequences exist, no formula Kim-divides over $\emptyset$ and no tuple has own preweight $\omega$; the notion is therefore sensitive to exactly the material whose existence the existence axiom guarantees.

The no-Ehrenfeucht lineage. Lachlan (1973) proved there is no superstable Ehrenfeucht theory (superstability is a strong form of stability in which forking extensions are controlled by a well-founded rank); Pillay (1983) gave a short forking-based account of Lachlan's proof and proved the same conclusion for the 'normal' stable theories; Herwig (1995) established the corresponding necessary condition for all countable stable theories — a countable stable theory with $1<I(\omega,T)<\omega$ must contain a type of own preweight $\omega$ — which does not settle the stable case, since stable theories can have such types (Herwig also constructed a small stable theory — small meaning that only countably many complete types over the empty set are realized — with one), and whether a countable stable theory can be Ehrenfeucht remains open (Pillay–Tanović 2026); Kim (1999) proved the same necessary condition for simple theories, and since no tuple in a supersimple theory (the simple-theory analogue of superstability) has own preweight $\omega$, a countable supersimple theory with finitely many countable models is $\aleph_0$-categorical, that is, has exactly one countable model up to isomorphism. Kim (2019), the source of this problem, extended the result to NSOP₁ theories with nonforking existence: a countable complete NSOP₁ theory with existence and no tuple of own preweight $\omega$ has either exactly one or infinitely many countable models. The proof first translates asymmetries of isolation and semi-isolation between conjugate tuples into Kim-forking (a type is isolated when a single formula implies it, and semi-isolated over the empty set when it contains a formula implying the corresponding type over the empty set; Proposition 2.3 and Corollary 2.6 of the paper) and then builds the witnessing sequence; at every step it uses the Dobrowolski–Kim–Ramsey package over arbitrary sets (extension, symmetry, Kim's lemma, the chain condition for $\downarrow^K$), all of which is proved only under the existence axiom.

The post-2024 landscape. Mutchnik (2024) constructed, from $\omega$-stable free pseudoplanes (the theory of undirected cycle-free graphs in which every vertex has infinite degree; $\omega$-stability is the strongest of the classical stability conditions), an NSOP₁ (indeed NSOP) theory $T_6^\exists$ that does not satisfy the existence axiom, answering Question 6.6 of Dobrowolski–Kim–Ramsey negatively; in $T_6^\exists$, nonforking Morley sequences over $\emptyset$ exist in one sort but not the other, and Mutchnik shows that, despite the failure of existence, the natural algebraic-closure-based independence relation of $T_6^\exists$ still coincides with Dobrowolski–Kim–Ramsey's $\downarrow^K$ and still satisfies symmetry and the independence theorem over sets. Kim–Kim–Lee (2025) proved that Kim-forking satisfies existence in all NSOP₁ theories — the failure of existence can never be witnessed by Morley sequences — and thereby defined a new notion of dividing by $\downarrow^K$-Morley sequences, which agrees with Kim-dividing exactly in theories with existence. These developments supply new tools precisely at the point where the source paper's hypothesis was used, but neither addresses the source's second question.

Problem Statement

Let $T$ be a complete first-order theory in a countable language. Assume only that $T$ is NSOP₁ (no SOP₁, as defined in the background); in particular, $T$ is not assumed to satisfy the existence axiom for forking, nor any other independence-theoretic hypothesis.

Question: if $1<I(\omega,T)<\omega$ — that is, if $T$ has more than one but only finitely many countable models up to isomorphism — must $T$ contain a finite tuple of own preweight $\omega$? Here a finite tuple $c$ has own preweight $\omega$, following the source paper's Definition 1.13, if there is a sequence $(b_i)_{i<\omega}$ of realizations of $\operatorname{tp}(c)$ such that $b_i\downarrow^K_\emptyset b_{<i}$ and $\operatorname{tp}(c/b_i)$ Kim-forks over $\emptyset$ for every $i<\omega$, where Kim-dividing and Kim-forking over $\emptyset$ are the notions of Dobrowolski–Kim–Ramsey as used by Kim (2019) (Kim-dividing is witnessed by nonforking Morley sequences over $\emptyset$; this definition applies verbatim in any theory, with or without existence).

One point must be made explicit. The own-preweight clause is fixed here with the forking clause oriented as "$\operatorname{tp}(c/b_i)$ Kim-forks over $\emptyset$" (the reading adopted above); an alternative orientation found in some accounts renders it as "$\operatorname{tp}(b_i/c)$ Kim-forks over $\emptyset$", equivalently $b_i\not\downarrow^K_\emptyset c$. Under the existence axiom the two readings coincide, by symmetry of Kim-independence over sets (Dobrowolski–Kim–Ramsey); without it they are not known to coincide, and this problem deliberately removes it. The question is posed in the first reading, and both an affirmative proof and a counterexample are judged in that same reading.

Equivalently: is the main theorem of Kim (2019) — a countable complete NSOP₁ theory with nonforking existence and no tuple of own preweight $\omega$ has exactly one or infinitely many countable models — still true with the nonforking-existence hypothesis deleted?

An affirmative answer extends the Lachlan–Herwig–Kim no-Ehrenfeucht phenomenon to the entire class of countable NSOP₁ theories. A negative answer must exhibit one explicit countable complete NSOP₁ theory with $1<I(\omega,T)<\omega$ and no tuple of own preweight $\omega$; any such counterexample necessarily fails the existence axiom (otherwise it contradicts Kim's theorem) and, being NSOP₁ and hence without the strict order property, would be the first known Ehrenfeucht theory without SOP — refuting Conjecture 1 of Pillay–Tanović (2026).

The problem asks the unconditional statement: a proof may not assume the existence axiom nor any conjectural substitute (such as an affirmative answer to Mutchnik's Question 4.4), and a counterexample may not leave hypotheses undischarged.

References

1. Byunghan Kim. On the number of countable models of a countable NSOP₁ theory without weight ω. The Journal of Symbolic Logic 84(3):1168–1175 (2019). DOI 10.1017/jsl.2019.47. https://doi.org/10.1017/jsl.2019.47
2. A. H. Lachlan. On the number of countable models of a countable superstable theory. In: Logic, Methodology and Philosophy of Science IV (Proceedings of the Fourth International Congress, Bucharest, 1971), Studies in Logic and the Foundations of Mathematics 74, North-Holland, pp. 45–56 (1973). DOI 10.1016/S0049-237X(09)70347-7. https://doi.org/10.1016/S0049-237X(09)70347-7
3. Anand Pillay. Countable models of stable theories. Proceedings of the American Mathematical Society 89(4):666–672 (1983). DOI 10.1090/S0002-9939-1983-0718994-3. https://doi.org/10.1090/S0002-9939-1983-0718994-3
4. Bernhard Herwig. Weight ω in stable theories with few types. The Journal of Symbolic Logic 60(2):353–373 (1995). DOI 10.2307/2275836. https://doi.org/10.2307/2275836
5. Byunghan Kim. On the number of countable models of a countable supersimple theory. Journal of the London Mathematical Society 60(3):641–645 (1999). DOI 10.1112/S0024610799008054. https://doi.org/10.1112/S0024610799008054
6. Itay Kaplan, Nicholas Ramsey. On Kim-independence. Journal of the European Mathematical Society 22(5):1423–1474 (2020). DOI 10.4171/jems/948. https://doi.org/10.4171/jems/948
7. Jan Dobrowolski, Byunghan Kim, Nicholas Ramsey. Independence over arbitrary sets in NSOP₁ theories. Annals of Pure and Applied Logic 173(2):103058 (2022). DOI 10.1016/j.apal.2021.103058. https://doi.org/10.1016/j.apal.2021.103058 (arXiv:1909.08368)
8. Itay Kaplan, Nicholas Ramsey. Transitivity of Kim-independence. Advances in Mathematics 379:107573 (2021). DOI 10.1016/j.aim.2021.107573. https://doi.org/10.1016/j.aim.2021.107573 (arXiv:1901.07026)
9. Artem Chernikov, Byunghan Kim, Nicholas Ramsey. Transitivity, lowness, and ranks in NSOP₁ theories. The Journal of Symbolic Logic 88(3):919–946 (2023). DOI 10.1017/jsl.2023.36. https://doi.org/10.1017/jsl.2023.36 (arXiv:2006.10486)
10. Byunghan Kim, Joonhee Kim, Hyoyoon Lee. Existence in NSOP₁ theories. The Journal of Symbolic Logic, published online 13 October 2025, pp. 1–15. DOI 10.1017/jsl.2025.10154. https://doi.org/10.1017/jsl.2025.10154 (arXiv:2405.13741)
11. Scott Mutchnik. An NSOP₁ theory without the existence axiom. Preprint, arXiv:2407.13082 (2024). https://arxiv.org/abs/2407.13082
12. Anand Pillay, Predrag Tanović. The number of countable models of first-order theories. Preprint, arXiv:2508.06854 (v1 August 2025; v2 of 15 August 2026). https://arxiv.org/abs/2508.06854 (survey, §3.1 states Conjecture 1 and the known no-Ehrenfeucht classes)
13. Alberto Miguel-Gómez. On stable Kim-forking and rosy theories. Preprint, arXiv:2503.23936 (2025). https://arxiv.org/abs/2503.23936 (adjacent result: under the stable Kim-forking conjecture, every NSOP₁ rosy theory is simple)