REVIEW 3 major objections 6 minor 1 cited by
Taking model-complete cores
T0 review · 3 major / 6 minor · reviewed 2026-08-03 · deepseek-v4-flash
Pith's one-line read Taking a model-complete core preserves the model-theoretic tameness of a theory: stability, NIP, simplicity, NSOP, and strong minimality all pass from a theory to its core companion.
desk verdict Preservation of dividing lines under core companions is the solid core; the (Q;<) non-closure chain hinges on an unproved same-author classification and the abstract overclaims the trace-definability result. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central working notion is the core companion S of a first-order theory T: the unique, when it exists, model-complete core theory with the same h-universal (universal-negative) consequences as T, meaning models of the two theories map homomorphically to each other. Because S is a model-complete core, every formula modulo S is existential positive, and existential positive formulas are preserved by homomorphisms; this is what allows formulas and their obstructions to be pushed from S into T. The proof engine is the positivisation of patterned properties: a scheme converting any property defined by omitting a combinatorial pattern in formulas into a positive-logic counterpart, so that the p
What would settle it
Check the cited classification directly: search for an automorphism-invariant equivalence relation on increasing d-tuples in Q^d that is not determined by fixing a subset of coordinates. If such a relation exists for some d, then the reduction lemma for interpretations in (Q;<) fails, and the non-interpretability results for (Q;<,S,T), the generic permutation, and the dense local order all break. Alternatively, find an omega-categorical structure in Lachlan's class that is not homomorphically equivalent to any structure interpretable over equality; that would refute Conjecture 5.5 and hence Co
Extended reading notes
Core claim
In the paper's own terms, the central discovery is that core companionship preserves essentially all mainstream dividing lines of model theory. Given a complete theory T with core companion S, T and S have the same universal-negative consequences, and S is a model-complete core theory, so every S-formula is equivalent to an existential positive formula. Any model-theoretic property that can be expressed as omitting a combinatorial pattern—stability, NIP, tree properties, SOP_n—can be 'positivised', and a formula exhibits the positivised pattern in S exactly when it exhibits the original pattern in T; hence NP passes from T to S. Independently, a homomorphism from a monster model of S to a mo
Load-bearing premise
The non-interpretability proofs over (Q;<) rest on a classification, cited without proof, saying that every automorphism-invariant equivalence relation on increasing d-tuples in Q^d is of the form S ⊆ (u=v) for a fixed set S of coordinates; if that classification fails, the proofs that structures such as the generic permutation are not interpretable in (Q;<) collapse, as does the separate abstract claim about trace definability of Lachlan's class, whose proof is missing from
Editorial extensions
If this is right
- If T is stable, NIP, simple, NSOP, NSOP_n, superstable, monadically stable, monadically NIP, or strongly minimal, then its core companion has the same property.
- The core companion of T is trace definable in T, so any property preserved under trace definability—including finite U-rank, finite Morley rank, finite dp-rank, and strong dependence—transfers to the core.
- For omega-categorical structures, where core companions always exist, every tame omega-categorical structure has a tame model-complete core, which is the case relevant to constraint satisfaction and orbit-finite computation.
- The hierarchy I((Q;=)) is strictly contained in MI((Q;=)), which is contained in Lachlan's class D, which is strictly contained in I((Q;<)); the final inclusion into E also holds, and D is closed under taking cores.
- The classes of structures interpretable over equality and over (Q;<) are not closed under taking cores; for (Q;<) this already fails for model companions, witnessed by the generic permutation.
Reading between the lines
- If Conjecture 5.4 is true, the model-complete core operation inverts equality-interpretation on Lachlan's class: every omega-stable finitely homogeneous reduct would be homomorphically equivalent to a structure interpretable over equality, and trace minimality for that class would follow as a strengthening the paper does not fully spell out.
- The trace-definability result suggests a practical strategy beyond the paper's explicit statements: any model-theoretic property preserved under trace definability can be verified on the core companion, which is often structurally simpler, even when no pattern-omission proof is available.
- The group-theoretic non-interpretability method—comparing involutions and kernels of finite covering maps—could plausibly be adapted to other homogeneous graphs whose cores arise as finite covers, since the four-fold fibres in the equality example are likely not the only possible obstruction.
- A direct test of Conjecture 4.45 would be to search for an omega-categorical structure not interpretable in (Q;<) with unlabelled growth slower than the betweenness reduct of the dense local order; the paper explicitly leaves that gap open.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies the model-complete core companion operation for first-order theories. Its main positive result, Theorem 3.1, asserts that if a complete first-order theory T has a core companion S, then S inherits a long list of model-theoretic tameness properties: stability, NIP, simplicity, NSOP, NTP2, NSOP_n, λ-stability, superstability, monadic stability/NIP, total transcendence, strong minimality, k-NIP, strong dependence, and finite U-rank. The proof machinery consists of three transfer methods: a positivization of patterned properties (Subsection 3.2), type-counting over parameter sets (Subsection 3.3), and trace definability of the core companion (Subsection 3.6). The paper then gives negative results: the class of structures interpretable over equality is not closed under taking model-complete cores (Corollary 4.21), and the class of structures interpretable over (Q;<) is not closed under taking model companions or model-complete cores (Corollary 4.38 and surrounding results); in particular (Q;<) does not interpret the generic permutation, (Q;<,S,T), or S(2). The final section introduces Lachlan's class D, conjectures that D equals the class of model-complete cores of structures interpretable over equality, and relates this conjecture to trace definability.
Significance. If the results are fully correct, this is a substantial contribution. The preservation theorem for patterned properties gives a uniform explanation of why so many dividing lines survive passage to the core companion, and the trace-definability transfer (Lemma 3.46) is a useful new tool. The non-closure results answer natural questions and the construction involving finite covers of the Johnson graph is elegant. The paper also makes progress on a conjecture of Walsberg, provided the conditional statement in Section 5 can be made unconditional. However, a significant part of the negative results over (Q;<) currently rests on an unproved classification result from a same-author preprint, and the abstract overstates the status of the trace-definability result for Lachlan's class. These issues need to be resolved before the paper can be accepted.
major comments (3)
- [Abstract and §5] The proof of Lemma 4.25 is entirely dependent on [BB25, Corollary 25], quoted as a black box: every Aut(Q^d)-invariant equivalence relation on increasing tuples is of the form {(u,v) : S ⊆ (u=v)}. This classification is not proved in the present paper and is taken from a same-author arXiv preprint. Lemma 4.25 is then the foundation for Theorem 4.37 and hence for Corollary 4.38 (non-closure of I((Q;<)) under model companions) and for Corollaries 4.40, 4.41, and 4.44 (non-interpretability of the generic permutation, S(2), and its betweenness reduct), as well as for the inclusion MI((Q;<)) ⊆ E in Theorem 6.1. If Corollary 25 of [BB25] is false, or if it carries an additional hidden hypothesis, these results collapse. Please include a proof of this classification in an appendix or replace the reference by a published, peer-reviewed source; otherwise the non-closure claims over (Q;<) should b
- [Conjecture 5.4 equivalence] The abstract states: 'To support our conjecture we prove that all structures in Lachlan's class are trace definable in (N;=), confirming a conjecture of Walsberg.' This is not what the full text proves. In Section 5, after Conjecture 5.4, the text only says that a positive answer to Conjecture 5.4 would imply a positive answer to Walsberg's question; no unconditional proof of trace definability for all of Lachlan's class is given. The abstract and the introduction should be corrected to say that trace definability is a consequence of Conjecture 5.4, not an independently proved theorem.
- [§4.2, Remark 4.22] The reduction in Lemma 5.6 and Proposition 5.7 shows the equivalence of Conjectures 5.4 and 5.5. This is fine. However, the sentence 'Note that a positive answer to Conjecture 5.4 would imply a positive answer to Walsberg's question' appears in the text only after stating Conjecture 5.4. If the authors intend trace definability of Lachlan's class as a contribution, it must be either proved or clearly marked as conditional. As written, this is a missing support passage that should be corrected in revision.
minor comments (6)
- [§3.5, Lemma 3.41 proof] In the induction step of Lemma 3.41, the sentence 'if MR(ϕ(x,a))≥α in S, then MR(ϕ(x,f(a)))≥α in S' should read '...in T' for the second occurrence; otherwise the proof is circular.
- [§4.3, Theorem 4.37 proof] The proof refers to 'Theorem 4.35' when it should refer to 'Lemma 4.35'. Please correct the cross-reference.
- [§4.2, Remark 4.22] Remark 4.22 says 'We mention without proof that both X and Y are finitely homogenizable'. Since this fact is not used in the main argument, this is acceptable, but if it is mentioned it should be marked as 'not used in this paper' or given a reference with a proof.
- [§3.2, Definition 3.16] The letter Q is used both for the rationals and for the set of cardinality pairs in Definition 3.16. This is harmless, but the notation clash could be avoided to improve readability.
- [§4.2.4, Lemma 4.19] The proof of Lemma 4.19 uses the classical Schreier–Ulam theorem. It would be helpful to state the precise form being used, since the statement 'every proper closed normal subgroup of Sym(Q) is trivial' is the key ingredient.
- [§5, Theorem 5.2] The implication (3)⇒(1) relies on Macpherson's theorem that finitely homogeneous relational structures cannot interpret an infinite group. This is a substantial external result and should be cited with the exact theorem number in [Mac91], so the reader can verify the translation to the present setting.
Circularity Check
No circular derivation: the preservation theorem is self-contained; the (Q;<) non-closure results rest on a same-author classification ([BB25, Cor. 25]) that is a load-bearing dependency but not a logical circle.
full rationale
The central preservation theorem (Thm 3.1) is derived from the definitions rather than assumed: patterned properties transfer because a core companion S and T have the same h-universal consequences (Lemma 3.19), and in a model-complete core every formula is equivalent to an existential positive formula (Lemma 3.21); type-counting uses the positive-type bijection (Lemma 3.25); monadic, Morley-rank, and trace-definability arguments are explicit homomorphism transfers. No fitted parameter is renamed as a prediction and no theorem is equal to its input by construction. The negative results are also explicit counterexamples with independent group-theoretic proofs (e.g., involutions in Aut(Y), Lemma 4.18; the Sym(Q)-subgroup obstruction, Lemma 4.19). The only load-bearing same-author dependency is Lemma 4.25, which invokes [BB25, Cor. 25] to force every Aut(Q^d)-invariant equivalence relation on increasing tuples to be of the form {(u,v): S ⊆ (u=v)}. This is a parameter-free classification whose assumptions do not include the target non-closure statements; under the hard rules it is independent support, so it does not constitute circularity. It is, however, a missing in-paper proof and should be weighed as a soundness/dependency concern. Separately, the abstract's claim that "we prove that all structures in Lachlan's class are trace definable in (N;=)" is not substantiated in Section 5, which only states that a positive answer to Conjecture 5.4 would imply Walsberg's trace-minimality question; this is an overclaim/omitted proof, not circularity. Overall: no circular step found; score 2 reflects the load-bearing same-author citation and the abstract overclaim rather than any definitional or fitted-input collapse.
Assumptions & free parameters
assumptions (5)
- domain assumption Pattern framework of [Bai24]: OP, IP, SOP, k-TP, k-TP2, SOP1–3 are patterned properties (Fact 3.14).
- domain assumption [BB25, Corollary 25]: every Aut(Q^d)-invariant equivalence relation on increasing tuples is {(u,v) : S ⊆ (u = v)}.
- standard math Schreier–Ulam: every proper closed normal subgroup of Sym(Q) is trivial.
- standard math Engeler–Svenonius–Ryll-Nardzewski and standard monster-model conventions.
- domain assumption Core companions exist for omega-categorical theories and correspond to homomorphic equivalence [Bod07, BHM12].
Cite this review
Pith. "Pith review of Taking model-complete cores." pith.science (2026). https://pith.science/paper/B7ZK7PQI
@misc{pith2026251221278,
author = {Pith},
title = {Pith review of: Taking model-complete cores},
year = {2026},
howpublished = {\url{https://pith.science/paper/B7ZK7PQI}},
note = {Machine review of arXiv:2512.21278}
}
abstract
A first-order theory $T$ is a model-complete core theory if every first-order formula is equivalent modulo $T$ to an existential positive formula; a core companion of a theory $T$ is a model-complete core theory $S$ such that every model of $T$ maps homomorphically to a model of $S$ and vice-versa. Whilst core companions may not exist in general, if they exist, they are unique. Moreover, $\omega$-categorical theories always have a core companion, which is also $\omega$-categorical. We show that many model-theoretic properties, such as stability, $\mathrm{NIP}$, simplicity, and $\mathrm{NSOP}_k$ for ${k\in\mathbb{N}_{>0}}$, are preserved by moving to the core companion of a complete theory. On the other hand, we show that the classes of theories of structures interpretable over $({\mathbb N};=)$ and over $({\mathbb Q};<)$ are both not closed under taking core companions. The first class is contained in the class of theories of $\omega$-stable first-order reducts of finitely homogeneous relational structures, which was studied by Lachlan in the 80's. We conjecture the two classes to be equal. To support our conjecture we prove that all structures in Lachlan's class are trace definable in $(\mathbb{N}; =)$, confirming a conjecture of Walsberg.
Figures
Forward citations
Cited by 1 Pith paper
-
Set-defined graph classes: $\chi$-boundedness meets tropical algebra
Full set-defined classes are polynomially χ-bounded iff they avoid high-chromatic shift graphs, decidable via tropical feasibility dual to mean-payoff games.
Reference graph
Works this paper leans on
-
[4]
Preprint arXiv:1204.3258. [Bod20] Manuel Bodirsky. Complexity of infinite-domain constraint satisfaction. Submitted for publication in the LNL Series, Cambridge University Press,
-
[5]
PhD the- sis, Technische Universit¨ at Dresden, Dresden, 2022.https://nbn-resolving.org/urn:nbn:de:bsz: 14-qucosa2-774379
[Bod22] Bertalan Bodor.CSP dichotomy forω-categorical monadically stable structures. PhD the- sis, Technische Universit¨ at Dresden, Dresden, 2022.https://nbn-resolving.org/urn:nbn:de:bsz: 14-qucosa2-774379. [Bod24] Bertalan Bodor. Classification ofω-categorical monadically stable structures.The Journal of Symbolic Logic, 89(2):460–495,
2022
-
[10]
Trace definability.arXiv preprint arXiv:2504.05566, 2025
[Wal25] Erik Walsberg. Trace definability.arXiv preprint arXiv:2504.05566, 2025
arXiv 2025
-
[1985]
On computability and tractability for infinite sets
[BT18] Miko laj Boja´ nczyk and Szymon Toru´ nczyk. On computability and tractability for infinite sets. InPro- ceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Oxford, UK, July 09-12, 2018, pages 145–154,
2018
-
[1996]
Definable groups for dependent and 2-dependent theories.arXiv preprint math/0703045,
[She07] Saharon Shelah. Definable groups for dependent and 2-dependent theories.arXiv preprint math/0703045,
-
[2000]
Notes on trace equivalence.arXiv preprint arXiv:2101.12194,
[Wal21] Erik Walsberg. Notes on trace equivalence.arXiv preprint arXiv:2101.12194,
-
[2014]
Turing machines with atoms
[BKaLT13] Miko laj Boja´ nczyk, Bartek Klin, S lawomir Lasota, and Szymon Toru´ nczyk. Turing machines with atoms. In28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, pages 183–192,
2013
-
[2021]
Structures preserved by primitive actions ofS ω.arXiv preprint arXiv:2501.03789,
[BB25] Manuel Bodirsky and Bertalan Bodor. Structures preserved by primitive actions ofS ω.arXiv preprint arXiv:2501.03789,
Show all 10 references
-
[2024]
Structures with not too fast unlabelled growth.arXiv preprint arXiv:2507.16985,
[Bod25] Bertalan Bodor. Structures with not too fast unlabelled growth.arXiv preprint arXiv:2507.16985,
-
[2025]
[BBH25] Bertalan Bodor, Samuel Braunfeld, and James E. Hanson. Labelled growth rates ofω-categorical struc- tures and applications in choiceless set theory.arXiv preprint arXiv:2509.12656,
Reviewed August 3, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.