One question, four verdicts: IS4 is decidable, the translation from FO³ into the calculus of relations cannot be made small, free groups have no model companion, and groups of exponent 3 do

Four preprints posted between 21 and 25 September 2026 put the same kind of question to four different theories: does the theory admit a finite syntactic object of the kind it needs, and what does that object cost? Marianna Girlando, Roman Kuznets, Sonia Marin and Lutz Straßburger give a decision procedure for the intuitionistic modal logics IS4 and IK4, one that ends either in a proof or in a finite countermodel 1. Yuya Uezato shows that the classical translation from three-variable first-order logic into the calculus of relations is optimal up to the constant in its exponent, so its exponential blow-up cannot be avoided 2. Olga Kharlampovich and Rizos Sklinos show that the first-order theory of nonabelian free groups has no model companion 3. Yawara Ishida, Ryosuke Mizuno and Kota Takeuchi show that the theory of groups of exponent 3 has one, which settles the first nonabelian case of a conjecture linking companionability to the Burnside problem 4.

A model companion is a model-complete theory carrying exactly the universal consequences of the theory it accompanies 3. The two group papers are the week's sharpest pair, because they put the same question to two families of groups and receive opposite verdicts. The exponent-3 paper proposes the condition that separates them: for the theory of groups of a fixed exponent n, a companion exists exactly when every finitely generated group of exponent n is finite, which is the Burnside problem at that exponent 4. Free groups sit outside the fixed-exponent family, and the obstruction there is the existential definability of the nonsquares 3.

All four are preprints, and none has been refereed. The succinctness result closes a question its author calls long-standing, the decidability result corrects an earlier published attempt at the same question, and the two model-theoretic results appeared within four days of each other.

A decision procedure for intuitionistic modal logic IS4 (and IK4) was first submitted to arXiv on 21 September 2026 under cs.LO, and the compiled preprint is dated 22 September 2026. It runs to 44 pages 1. The authors are Marianna Girlando, Roman Kuznets, Sonia Marin and Lutz Straßburger, and the preprint thanks Agi Kurucz for finding a counterexample that the paper works through 5. Kuznets's contribution is credited to the ERDF project "Knowledge in the Age of Distrust" 5.

IS4 is the intuitionistic analogue of the modal logic S4, and IK4 the analogue of K4; axiom systems for these logics go back to Gisèle Fischer Servi's 1984 paper 5. Their models are birelational: a modal accessibility relation R sits alongside the intuitionistic preorder ≤ on the same set of worlds 5. The proof system the authors use is the fully labelled sequent calculus of Marin, Morales and Straßburger, which carries relational atoms for both relations and has the property that every rule is invertible, so a sequent corresponds directly to a model 5.

The paper proves that IS4 and IK4 are decidable, by constructing a proof search that always terminates and that, when it fails, delivers a finite countermodel; the finite model property for both logics follows 1. Three devices carry the procedure. Macro-rules derivable in the labelled calculus keep sequents in a fixed shape. The search alternates between a saturation phase and a lifting phase. Loop-rules that would be unsound on their own let the search continue once a loop has been detected, and are then eliminated to prove soundness 5. Termination is established by bounding the length of a branch against what the authors call evil sequences 5.

The preprint also corrects the record. A preliminary version of this work appeared at LICS 2023, and its proof-search algorithm does not terminate, because its loop condition is too weak; Agi Kurucz found the counterexample, which the paper now presents in a section of its own 5. The stated purpose of the preprint is to supply that correction, and Section 8 adapts the corrected procedure to IK4 5.

This is a preprint and has not been peer-reviewed. The support is proof-theoretic: 44 pages of constructions and proofs, with no data and no experiments. What the paper settles is decidability and the finite model property for IS4 and IK4 1. The calculus it searches in is taken from earlier work; the new element is the proof search and its termination argument 5. Earlier labelled systems for IS4 exist, among them Simpson's, and the preprint explains why they had not been turned into a decision procedure: mixing a structural treatment of the intuitionistic side with label-based handling of the modality produces two loop tests that have to be combined with backtracking 5.

Open it if you work on intuitionistic modal logic or on labelled proof search, or if you want a worked case of a loop-check that has to combine a modal loop test with intuitionistic backtracking. Read Section 2.2 first, which sets out why the decidability question resisted the obvious approaches, then Section 4 for Kurucz's counterexample and the corrected loop condition, then Section 3 for the algorithm itself. The prerequisites are labelled sequent calculi, birelational Kripke semantics, and enough proof-search theory to follow a termination argument.

An Exponential Succinctness Gap between Three-Variable Logic and the Calculus of Relations was first submitted to arXiv on 22 September 2026 under cs.LO. Yuya Uezato is the sole author, at CyberAgent, Inc., and the preprint runs to 45 pages 2.

Three-variable first-order logic FO³ over binary relations and the calculus of relations CoR define the same binary queries, an equivalence that goes back to Tarski's work in the 1940s 2. CoR is the algebra of binary relations under union, intersection, complement, converse and composition, also called the relative product; it has no individual variables, so eliminating a quantifier has to go through composition, since ∃z (P(x, z) ∧ Q(z, y)) holds exactly when (P ; Q)(x, y) does 2. The classical translation from FO³ into CoR combines that equivalence with a bottom-up conversion to disjunctive normal form, and it is there that the single-exponential blow-up enters 6. Tarski and Givant defined their translation recursively and put no bound on its growth 9.

Uezato proves that this blow-up is unavoidable, resolving a long-standing open question 2. Two families of formulas supply the lower bounds. For the disjunctive-clause family Ψk, every CoR term equivalent to it over finite structures needs at least (1/2)·C(k, ⌊k/2⌋) compositions and size C(k, ⌊k/2⌋) + 1, and the composition bound also applies to relational circuits 6. For the profile-agreement family Φk the composition count is at least 2^(k−1) and the term size at least 2k + 1, again with the circuit version 6. Both families are positive, use a single quantifier, and have size linear in k, which yields the succinctness gap: there are positive FO³ formulas with one quantifier of unbounded size such that every equivalent relational circuit over finite structures has size 2^Ω(|φ|) 6. The transfer is optimal up to the constant in the exponent, since an equivalent term of size 2^O(|φ|) exists 6.

The proof uses a preservation argument over a single finite structure, and the method reaches past the original question: the bounds hold for size-specific circuits chosen for each domain size, and a randomized circuit that is correct with probability at least 1 − ε still needs a fraction (1 − 2ε) of the same number of compositions 6. An analogous exponential gap follows for MATLANG, the matrix query language: under the min-plus, max-plus or max-min semiring, some relational algebra expressions of size O(k) need at least 2^k/3 matrix products contracting the dimension n, while 2^k products suffice 6.

The paper is a preprint and has not been peer-reviewed. Its support is a construction with explicit lower bounds, worked out across 45 pages, and it reports no data. The lower bounds are unconditional, and they are stated over finite structures, which is the stronger reading 6. One case is left open on the author's own statement: the two constructions use a vocabulary that grows with k, and whether an exponential gap survives over a fixed signature is recorded as unknown 6.

Open it if you work on finite model theory, on relation algebra, or on the cost of translating between formalisms with the same expressive power. Start with the outline of the proof of Theorem 1.2 in Section 1.4, then read the preservation argument in the section that follows, since that argument is what makes the bound unconditional. The prerequisites are the calculus of relations, three-variable logic, and comfort with circuit and formula size as complexity measures.

The theory of nonabelian free groups has no model companion was first submitted to arXiv on 21 September 2026 under math.LO. Olga Kharlampovich and Rizos Sklinos are the authors, and the preprint is five pages long 3.

The object is T_fg, the first-order theory of nonabelian free groups, and the question is whether it has a model companion, meaning a model-complete theory with the same universal consequences 7. The theory is not model complete, and the preprint gives a two-line witness: the subgroup generated by the first basis element together with the square of the second is itself free of rank 2, yet the inclusion is not elementary, because that square has a square root in the larger group and none in the subgroup 7. One further observation does the work: an existential formula cannot distinguish a primitive element from any of its nontrivial powers 7.

Theorem 1.1 states that T_fg has no model companion 3. The proof is by obstruction. If a companion existed, then by the equivalence between model completeness and existential definability, the set of nonsquares would be definable by an existential formula 7. Uniform small cancellation, together with the implicit function theorem over free groups, then forces any such formula to be satisfied by a primitive element of a free group 7. An existential formula that holds of a primitive element holds of each of its nontrivial powers, so a formula defining nonsquares would hold of a square, which is a contradiction 7. A corollary extends the negative answer: every nonabelian limit group is universally equivalent to a nonabelian free group, so the first-order theory of any nonabelian limit group also has no model companion 7.

This is a five-page preprint that has not been peer-reviewed, and the whole argument is set out inside it. Its inputs are cited rather than reproved: the small-cancellation machinery comes from Casals-Ruiz, Garreta and de la Nuez González, the implicit function theorem over free groups from Kharlampovich and Myasnikov, and the completeness of T_fg that the argument leans on from the two independent solutions of Tarski's problem 7. Those two solutions are large and well cited: Kharlampovich and Myasnikov's 2006 paper has 240 recorded citing works and Sela's 215 1011. The preprint reports no data, and the result concerns the first-order theory of these groups and their existentially equivalent relatives, not their algorithmic properties.

Open it if you work on the model theory of groups, or if you want a short example of an existential-definability obstruction closing a model-companion question. Five pages makes it readable in one sitting, and the proof occupies four of them. The prerequisites are the definition of a model companion, existential definability, small cancellation, and the implicit function theorem over free groups.

Existence of a Model Companion for Groups of Exponent 3 was first submitted to arXiv on 24 September 2026 under math.LO, and it runs to 21 pages 4. Yawara Ishida and Ryosuke Mizuno are at A.I. Systems Research Institute Co., Ltd.; Kota Takeuchi is at the Institute of Mathematics, University of Tsukuba and is partially supported by JSPS KAKENHI grant 25K00213 8. The preprint discloses that an initial outline of the proof of the main theorem was generated with ChatGPT and that the authors then reconstructed the argument and checked the proofs in detail, taking responsibility for the content 8.

For an integer n greater than 1, Tn is the theory of the variety Vn of groups satisfying xⁿ = 1, in the usual language of groups. These axioms impose a fixed exponent identity and no separate bound on nilpotency class or derived length, which makes the family a natural test case for the model-companion question 8. The surrounding record is mixed. Abelian group theories and theories of groups of a fixed finite exponent with nilpotency class at most 2 have companions, and so do groups of prime exponent p with nilpotency class below p 8. Theories of all groups, of torsion-free groups, and of nilpotent groups of any class at least 2 have none 8.

The main theorem is that T₃ has a model companion 8. The exponent 3 is the first nonabelian case, since exponent 2 is abelian, and groups of exponent 3 are nilpotent of class at most 3, with class 3 actually attained 8. That places the result outside both the class-2 theorem of Saracino and Wood and the class-below-p theorem of Maier 8.

The paper frames the theorem as an instance of a conjecture: for every n, Tn has a model companion if and only if the Burnside problem has a positive solution at exponent n, that is, if and only if Vn is locally finite 8. The conjecture holds at n = 2 by the theory of vector spaces over the two-element field, and the main theorem supplies the n = 3 case. The authors add that they have a proof that Tp has no model companion for every sufficiently large prime p, to appear elsewhere; combined with the Novikov–Adian theorem, which gives a negative solution to the Burnside problem for every odd exponent at least 665, that would prove the conjecture for all sufficiently large primes 8.

The machinery is group-theoretic rather than logical. V3 is locally finite but lacks the amalgamation property, so the authors study finite witnesses to its failure. They prove a finite strict-envelope theorem: every finite subgroup of an existentially closed model of T3 sits inside a finite subgroup that is strict with respect to the lower central series, with a quadratic bound on the number of generators. Strictness makes a coproduct map injective, which confines a witness to a coproduct with boundedly many generators, and a uniform bound of that kind yields the model companion 8. They also prove a structure theorem for existentially closed models of T3 — lower and upper central series coincide in reverse order, and elements of the second and third terms of the lower central series are commutators and triple commutators — using the associated graded Lie algebras of coproducts in V3 8.

This is a preprint and has not been peer-reviewed. The support is proof-theoretic across 21 pages, with no data and no computation reported. Two things bound the claim. The theorem is about T₃, and the general conjecture remains a conjecture; the non-existence half for large prime exponents is stated as proved elsewhere, so a reader cannot check it in this preprint 8. Section 5 supplies examples showing that lower-central strictness and existential closedness are both needed for the argument, which marks the edges of the technique 8.

Open it if you work on the model theory of groups or on amalgamation in varieties, and particularly if you want to see how far a bounded-generator witness argument reaches. Read Section 3 for how the main theorem follows from the bounded-witness and strict-envelope results, then Section 5 for the examples that show why those hypotheses cannot be dropped. The prerequisites are model companions and existentially closed models, amalgamation in varieties, the lower central series, and enough Lie algebra to follow a graded construction.

Each paper asks whether a finite object of a particular kind can be had for a theory, and each answer constrains what the theory can be presented with. On the proof-theoretic side, IS4 and IK4 admit an effective procedure that decides validity and hands back a countermodel when it fails 1. Uezato's lower bounds say that the same cannot be had cheaply for the translation of FO³ into the calculus of relations: the compact presentation exists, and it necessarily grows exponentially 2. On the model-theoretic side, the two group papers fix the two ends of one question: no companion for the theory of nonabelian free groups and for every nonabelian limit group 3, a companion for groups of exponent 3 4. The condition the exponent-3 paper offers for the fixed-exponent family, local finiteness of the variety, is exactly the kind of dividing line the free-group result lacks, since free groups are not a fixed-exponent family and their obstruction is existential definability instead.

The same week carried three further logic results worth knowing about. Graham Leigh and Dominik Wehr, in the Archive for Mathematical Logic, give a direct embedding of cyclic proofs for Heyting and Peano arithmetic into finitary inductive proofs, and obtain the inclusion CΠn ⊆ IΠn+1 that extends Das's comparison of inductive and cyclic complexity 12. Zoltan A. Kocsis proves that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions comes apart from syntactic consequence 13. Jonathan Osinski characterises exacting, rank-Berkeley, Berkeley and club Berkeley cardinals by compactness properties of logics and of topological spaces, and draws the consequence that compactness assumptions can violate the axiom of choice and the axiom V = HOD 14.

Every count below was read on 27 September 2026.

For the four featured papers, the record is uniformly empty, and it is empty in a way worth naming. DataCite, the registration agency for arXiv's DOIs, returns zero citing works for each of the four 15. OpenAlex returns a cited-by count of zero for each 16. Google Scholar renders no cited-by line at all for any of the four, which is what its result page looks like when a record has attracted none 17. Crossref does not index arXiv DOIs, so its cited-by field is not available for these four at all; arXiv registers with DataCite instead 18.

Semantic Scholar's graph endpoint answered during this week's window, which it had not done in the previous four weeks, when it returned HTTP 429 to every request. It returned citation records for indexed papers, including a zero count for another 21 September preprint 19. Repeated queries against the same endpoint then met its rate limit, and the four featured arXiv identifiers returned no individual counts 19. The four papers were posted between one and six days before the count was taken, so these zeros describe indexing latency.

The window's journal records show the opposite pattern. Crossref carries in-window published dates in the Australasian Journal of Philosophy, Noûs, Philosophical Studies, Erkenntnis, Mind, Analysis, the Archive for Mathematical Logic, the Bulletin of Symbolic Logic, the Logic Journal of the IGPL and Logica Universalis, and none at all in the Journal of Philosophical Logic, The Review of Symbolic Logic, the Notre Dame Journal of Formal Logic, Studia Logica, Synthese, Linguistics and Philosophy, the Journal of Semantics or Semantics and Pragmatics 2021. One of those in-window dates is a case in point. Ryan Simonelli's "Bringing Bilateralisms Together" carries a Crossref published date of 22 September 2026 in the Australasian Journal of Philosophy, while Google Scholar dates the article to 2023 and reports four citing works for it 2223. Semantic Scholar records three citing works for the same article, and OpenAlex one 2425. A Crossref published date records the version that carries the issue, while the citing works accumulated around the earlier version that circulated.

For scale, the literature these papers build on sits in the hundreds. Tarski and Givant's A Formalization of Set Theory without Variables carries 451 citing works, 11 of them added in 2024 26. The two solutions of Tarski's problem continue to draw: 240 citing works for Kharlampovich and Myasnikov, 215 for Sela, with a handful added in each of the last three years 2728. A smaller recent line, the model theory of nilpotent groups and Lie algebras, has six citing works, four from 2025 and two from 2026; the exponent-3 preprint cites it for a corollary it relies on 829.

Do you want the technique, or the result? For the technique, read the IS4 preprint: Section 2.2 states why decidability resisted earlier systems, Section 4 shows the counterexample that broke the 2023 algorithm, and Section 3 builds the corrected procedure 5.

Do you need a lower bound you can reuse? Read Uezato. The preservation argument over a single finite structure is the transferable part, and it is what carries the bounds to size-specific and randomized circuits and to MATLANG 6.

Do you work on the model theory of groups? Read the free-group paper first, because it is five pages and settles the negative case for limit groups as well; then read the exponent-3 paper's Section 3, where the main theorem follows from the bounded-witness and strict-envelope results 78.

Do you want to know where the companionability line falls? The exponent-3 paper's Conjecture 1.1 ties it to local finiteness across the fixed-exponent family, and the announced result that Tp has no companion for large primes is the half a reader cannot yet check 8.