Pith. sign in

REVIEW 2 major objections 2 minor 29 references

Tightness and solidity in fragments of Peano Arithmetic

T0 review · 2 major / 2 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read For every n, there is a recursively enumerable solid theory strictly between IΣ_n and PA — so Peano Arithmetic is not the minimal solid theory, and solidity does not force full induction.

desk verdict Resolves Enayat's question for PA in the non-trivial sense; the core arguments look sound, though a few delegated proofs and abstract overstatements need referee attention. read the letter →

arxiv 2512.09120 v2 pith:RPMJAXJY submitted 2025-12-09 math.LO

Piotr Gruza , Leszek Aleksander Ko{l}odziejczyk , Mateusz {L}e{l}yk This is my paper · ORCID
classification math.LO MSC 03F3003C62
keywords PeanoArithmeticsoliditytightnessbi-interpretabilityflexibleformulascompositionaltruthretract-disjointnessfragmentsof
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper answers an open question about Peano Arithmetic: do the well-known solid theories PA, ZF, and Z₂ have proper solid subtheories? It proves that for every n there is a recursively enumerable solid subtheory of PA that contains the fragment IΣ_n plus exponentiation but does not prove the next fragment BΣ_{n+1}. The construction makes a theory that says either full PA holds or else we are in a specially built pointwise-definable model of IΣ_n plus negation of BΣ_{n+1}, and this exceptional model is bi-interpretable with the compositional truth theory CT[PA]. The paper also produces refinements that fail to interpret PA, remain below PA even after adjoining all true Π_k sentences, and separate tightness from neatness and from semantical tightness. Taken together, these results rule out characterizing PA as a minimal solid theory in the ordering of logical implication.

What carries the argument

A flexible formula is a formula ξ(x) over a theory T such that for every formula φ(x) in a specified class, the theory T plus ∀x(ξ(x)↔φ(x)) is consistent; the paper uses a hierarchy of such formulas whose consistency is itself provable from Con(T) inside IΔ₀+exp. This lets the construction define the truth predicate P on the shortest definable cut of the pointwise definable model, making that cut a model of CT[PA]. The second central object is the pair of interpretations K_n and N_n witnessing a bi-interpretation between IT(n) and CT[PA], and the third is the retract-disjointness of the family of iterated truth theories CT_k[PA], which prevents mixed PA-versus-IT cases in the disjunctive the

What would settle it

Check whether IΔ₀+exp really proves the 'moreover' statement of Theorem 3.6(a) for the particular Σ₁-flexible formula ξ_n, or build inside a model of CT[PA] the formalized Henkin construction for the theory U from Proposition 4.7 and see whether the leftmost path and the Σ_{n+1}-definable substructure are definable as claimed; a counterexample at either point would remove the proof of Con(U) and with it the bi-interpretability that drives solidity.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that solidity is not a monopoly of full induction: for every n there exists an r.e. theory T_n with IΣ_n + exp contained in T_n and T_n a proper subtheory of PA, such that whenever a model M of T_n has a model N of T_n as a retraction, N is M-definably isomorphic to the identity interpretation. Solidity here means exactly this internalized categoricity property: any retraction between models is definably trivial. The engine is a pair of mutually inverse interpretations: one builds, inside the standard model of compositional truth, a Henkin model H for a complete extension of IΣ_{n+1} together with a Σ₁-flexible formula ξ_n; the Σ_{n+1}-defin

Load-bearing premise

The construction stands on the claim that the flexible-formula theorem's 'moreover' clause — Con(T) implies Con(T + ∀x(ξ(x)↔φ(x))) provably in IΔ₀+exp — holds (Theorem 3.6(a), proved by reference to a cited text), and on Proposition 4.7's assertion that the Henkin-model construction and the bi-interpretability of IT(n) with CT[PA] formalize inside CT[PA]; if either internal provability is weaker than stated, the proof that IT(n) is solid collapses.

Editorial extensions

If this is right

  • Solidity of a theory does not imply that the theory proves full induction: for every n, IΣ_n + exp can be extended to a solid theory that refutes BΣ_{n+1}.
  • There are proper solid subtheories of PA that are strictly weaker in interpretability strength: they do not interpret PA, so PA is not minimal solid even in the coarser order of interpretability.
  • The solidity-without-PA phenomenon survives the addition of arbitrary true Π_k sentences: for each fixed k, the strengthened theory T^F_n + Th_{Π_k}(N) still fails to prove PA.
  • Tightness and neatness are genuinely different properties for strong r.e. subtheories of PA: there are tight-but-not-neat theories arbitrarily high below PA.
  • The four categoricity-like properties are not collapsed: there are sequential r.e. theories separating neatness from semantical tightness and producing a tight theory that is neither neat nor semantically tight, and Z₂ itself has a proper solid subtheory containing ACA′.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the template 'either the full scheme holds, or else we are in a truth-theoretically tagged exceptional model' should transport to higher levels of second-order arithmetic, giving arbitrarily strong proper solid subtheories of Z₂ at levels such as Π¹₁-CA; the paper explicitly leaves the Π¹₂-CA level open.
  • Editorial inference: the obstruction to interpretability exploited in Section 4.3 looks like a general principle — a theory obtained by gluing infinitely many pairwise inconsistent solid components cannot generally convert model-by-model interpretations into one uniform interpretation; a precise formulation could yield a new criterion for non-interpretability of stronger theories.
  • Editorial inference: if the paper's final open question receives a negative answer — that is, if every reasonably strong solid subtheory of PA has a model that interprets a model of PA — then a weakened form of PA-minimality could survive inside the model-interpretation order even though the implication order and the interpretability order both fail.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 2 minor

Summary. The paper studies tightness, neatness, solidity, and semantic tightness for first-order theories, focusing on fragments of PA. The main result is a positive answer to Enayat's question for PA: for every n there is an r.e. solid proper subtheory of PA containing IΣ_n+exp but not BΣ_{n+1}. Refinements give solid subtheories that do not interpret PA and solid subtheories that remain below PA after adding all true Π_k sentences. The paper also separates tightness from neatness, and neatness from semantic tightness, and gives a solid proper subtheory of Z_2 extending ACA′. The proofs use flexible formulas, pointwise definable models, iterated Tarskian truth theories, and formalized versions of metamathematical constructions.

Significance. If the central arguments are correct, this is a substantial contribution: it refutes the natural conjecture that solidity characterizes full induction and shows that PA is not minimal solid in the interpretability order either. The paper also provides the first nontrivial separations between tightness-like properties for sequential theories. The constructions are explicit and the paper is careful in defining the auxiliary theories IT(n), TD_n, TF_n, and S_n and in verifying their properties. The main proofs are detailed, though two load-bearing formalizations are delegated to references or described as routine.

major comments (2)
  1. [Theorem 3.6(a)] The 'moreover' clause of Theorem 3.6(a) is load-bearing: it is used in Corollary 3.7 and in Proposition 4.7 to prove that CT[PA] proves Con(U), which drives the bi-interpretability of IT(n) and CT[PA] and hence the solidity proof. The proof of this clause is not given; the text says only 'as in [21]'. Lindström's argument may prove the existence of a flexible formula, but it is not clear that it proves the additional formalized statement '%Con(T) → ∀φ(FormΣk(φ) → Con(T+∀x(ξ(x)↔φ(x))))% is provable in IΔ0+exp' at the stated strength. Please supply a full proof or a precise citation with the exact statement, because the internal least-witness argument for IΔ0+exp is nontrivial and the paper's later claims depend on it.
  2. [Proposition 4.7] The proof of Proposition 4.7 is summarized as 'a somewhat routine verification' that CT[PA] is strong enough to formalize the construction of the Henkin model and the pointwise definable substructure, and then to verify axioms (ii)–(v) of IT(n). This is not routine in a weak base: the consistency of the theory U and the definability of the leftmost path in CT[PA], the preservation of Σ_{n+1}-elementarity, and the verification that δ_n is the shortest definable cut all need to be checked in detail. Since Proposition 4.7 is used to establish the bi-interpretability of IT(n) with CT[PA] and hence Lemma 4.5 and the retract-disjointness arguments, the sketch should be expanded into a complete proof.
minor comments (2)
  1. [Corollary 4.16] In the proof of Corollary 4.16, the text states 'PA⊢Con(IΣ_n), whereas IΔ0+exp+∃xξ_n(x)⊢¬Con(IΣ_n) by Corollary 3.7'. But ξ_n is chosen to be Σ_1-flexible over IΣ_{n+1}, so Corollary 3.7 gives ¬Con(IΣ_{n+1}), not ¬Con(IΣ_n). The argument still works if Con(IΣ_{n+1}) is used, since PA proves the consistency of IΣ_{n+1}; this is a local index error that should be corrected.
  2. [Section 5.2, Lemma 5.5] In the proof of Lemma 5.5, the sentence 'J_n is the shortest initial segment of H which contains all the finite iterations ...' is somewhat terse; a pointer to the explicit definition of J_n in Section 5.2 would help the reader verify that N_n indeed isolates the standard cut.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the solid/tight/neat theories are constructed explicitly and their target properties are proved afterward; delegated proofs are proof gaps, not definitional reductions.

full rationale

The derivation chain is self-contained in the sense relevant to circularity. Theorem 4.1 defines T_n by an explicit case split: BΣ_{n+1}→IΣ_k on one side and ¬BΣ_{n+1}→φ for φ∈IT(n) on the other. IT(n) is axiomatized by properties of the constructed model K (IΣ_n+exp+¬BΣ_{n+1}, shortest definable cut, N_n⊨CT[PA], and isomorphism statements), but solidity is not among the axioms. Solidity is then proved by a genuine four-case analysis using Lemma 4.5 and Lemma 4.6. Lemma 4.5 is derived from Lemma 3.9, whose proof is given in the text, together with axioms (ii) and (iv); it does not reduce to assuming solidity. Lemma 4.6 is proved by a Tarski truth-definability argument. The refinements in Theorems 4.15 and 4.22 similarly use retract-disjointness established via bi-interpretation and CT_n[PA] solidity, with Corollary 3.10 proved as a special case of Lemma 3.9 rather than merely cited. No fitted parameter is relabeled as a prediction: the theories ITD(n), ITF(n), S_n, U are defined with stated axioms and then verified to possess the target properties; the properties are not built into the definitions by renaming. The genuine weaknesses are delegated proofs: the formalized 'moreover' clause of Theorem 3.6(a) is said to be 'as in [21]', and Proposition 4.7's verification is called 'somewhat routine'. These are omissions of proof and a correctness risk if the formalization needs more than IΔ0+exp, but they are not circularity: the target solidity/tightness conclusions are not assumed in the inputs. Self-citations to [6], [5], and [20] are either non-load-bearing or accompanied by proofs in the present paper.

Assumptions & free parameters 0 free parameters · 9 assumptions · 0 invented entities

Pure mathematics; no fitted parameters, no data. The central claim rests on imported background results (solidity of PA [4], flexible formulas [22]/[21], fragment model theory [12], arithmetized completeness [16], CARD scheme [17]) and the paper's own constructions (IT(n), ITD(n), ITF(n), IS(n), U, T = PA + p(c)), all of which are proved in the text. The most delicate imports are the internal provability clauses of flexible formulas (Theorem 3.6) and the formalization of the Henkin construction inside CT[PA] (Prop 4.7), which the paper partially delegates. No invented entities: all new objects come with existence proofs inside the paper; the flexible formulas and interpretations are constructed, not postulated.

assumptions (9)
  • domain assumption Solidity of PA (Enayat [4]): any retraction between models of PA collapses to definable isomorphism.
    External benchmark used in the case analyses of Thm 4.1 (case 1°), Thm 5.2, Thm 5.8, Thm 5.11. Imported, not reproven.
  • domain assumption Enayat–Łełyk [6]: all CTn[PA] are solid (reproven here in generalized form as Lemma 3.9 / Corollary 3.10).
    Self-cited (Łełyk is a co-author of [6]); the paper supplies its own proof of the needed generalization, so the reliance is internal.
  • standard math Theorem 3.6 (flexible formulas, Montagna [22]/Lindström [21]): Σk-flexible formulas exist with internal provability clauses; proof of part (a) delegated, part (b) proven in text.
    The existence of ξn, ζn with the 'moreover' clauses; the strongest load-bearing external import.
  • standard math Tarski's undefinability of truth: no LPA formula with parameters defines satisfaction in a model of PA.
    Used in Lemma 4.6, Lemma 4.11 and Prop 6.1 for retract-disjointness; classical.
  • standard math Ehrenfeucht's Lemma: in a model of PA, if b is definable from a and b ≠ a, then tp(a) ≠ tp(b).
    Crucial in Theorem 5.11 to force ι^{-1}(d)=c; cited to [3]/[18].
  • domain assumption Standard model-theoretic facts for fragments: K_{n+1}(M) ≼_{Σ_{n+1}} M; existence of models of IΣn + ¬BΣn+1 and BΣn + ¬IΣn; IΣ_{n+1} ⊢ BΣ_{n+1}.
    Foundations of the intended models of IT(n) and IS(n); cited to Hájek–Pudlák [12, Ch. IV.1(d)].
  • domain assumption Arithmetized completeness theorem (leftmost Henkin path) formalizes in CT[PA] (Kaye [16, Thm 13.13]); Proposition 4.7's formalization is a 'routine verification'.
    Enables Kn as an interpretation of IT(n) in CT[PA]; the paper flags this as routine rather than writing it out.
  • domain assumption Cardinality scheme theorem (Kaye [17], Theorem 5.3): BΣn + exp + ¬IΣn ⊢ CARD.
    Used in Theorem 5.2's mixed-case contradiction; external.
  • domain assumption CTn[PA] ⊢ Σ_{n+2}-RFN(IΣn+1) and CT[PA] ⊢ Con(IΣn+1) (used in Prop 4.7 and Lemma 4.25).
    Complexity bounds for the flexibility formalizations in truth theories; stated without proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Tightness and solidity in fragments of Peano Arithmetic." pith.science (2026). https://pith.science/paper/RPMJAXJY

@misc{pith2026251209120,
  author       = {Pith},
  title        = {Pith review of: Tightness and solidity in fragments of Peano Arithmetic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RPMJAXJY}},
  note         = {Machine review of arXiv:2512.09120}
}
abstract

It was shown by Visser that Peano Arithmetic has the property that any two bi-interpretable extensions of it (in the same language) are equivalent. Enayat proposed to refer to this property of a theory as \emph{tightness} and to carry out a more systematic study of tightness and its stronger variants that he called neatness and solidity. Enayat proved that not only $\mathsf{PA}$, but also $\mathsf{ZF}$ and $\mathsf{Z}_2$ are solid. On the other hand, it was shown in later work by a number of authors that many natural proper fragments of those theories are not even tight. Enayat asked whether there is a proper solid subtheory of the theories listed above. We answer that question in the case of $\mathsf{PA}$ by proving that for every $n$, there exist both a solid theory and a tight but not neat theory strictly between $\mathsf{I}\Sigma_n$ and $\mathsf{PA}$. Moreover, the solid subtheories of $\mathsf{PA}$ can be required to be unable to interpret $\mathsf{PA}$. We also provide simple examples of proper solid subtheories of $\mathsf{ZF}$ and $\mathsf{Z}_2$, as well as further separations between properties related to tightness, including an example of a sequential theory that is neat but not semantically tight in the sense of Freire and Hamkins.

Figures

Figures reproduced from arXiv: 2512.09120 by the authors.

Figure 4.1
Figure 4.1. Construction of the model (N, Th(N))Kn of IT(n). The solid horizontal lines represent (N, Th(N))Kn , which is the pointwise Σn+1-definable substructure of the Henkin structure H. The dashed horizontal lines represent the rest of H. • Consider a canonically defined binary tree whose paths correspond to complete con￾sistent henkinized extensions of the theory IΣn+1 ∪ {ξn(k) : k ∈ Th(N)} ∪ {¬ξn(k) : k ∈ N \ Th(N)}. (4)… view at source ↗
Figure 4.2
Figure 4.2. The proof of Lemma 4.5. The solid arrows represent isomorphisms given directly [PITH_FULL_IMAGE:figures/full_fig_p020_4_2.png] view at source ↗
Figure 5.1
Figure 5.1. Construction of the model N Jn of IS(n). The solid horizontal lines represent N Jn , which is a nonstandard Σn+1-elementary initial segment J of the Henkin structure H. The dashed horizontal lines represent the rest of H. interpretation of N in our model. In fact, we will reuse the name Nn for that inverse in￾terpretation, because it will essentially do the same job as before – pick out the smallest definable cut of… view at source ↗
Figures from the paper (1 more)
Figure 5.2
Figure 5.2. Figure 5.2: The proof of Lemma 5.6. The horizontal solid arrow represents an isomorphism [PITH_FULL_IMAGE:figures/full_fig_p035_5_2.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 1 linked inside Pith

  1. [21]

    Association for Symbolic Logic, Urbana, IL; A K Peters, Ltd., Natick, MA, second edition, 2003

    Per Lindström.Aspects of incompleteness, volume 10 ofLecture Notes in Logic. Association for Symbolic Logic, Urbana, IL; A K Peters, Ltd., Natick, MA, second edition, 2003

    2003

  2. [1]

    Quasi-finitely axiomatizable totally categorical theories.Ann

    Gisela Ahlbrandt and Martin Ziegler. Quasi-finitely axiomatizable totally categorical theories.Ann. Pure Appl. Logic, 30(1):63–82, 1986

    1986

  3. [2]

    Reflection principles and provability algebras in formal arithmetic

    Lev Beklemishev. Reflection principles and provability algebras in formal arithmetic. Russian Math. Surveys, 60(2):197–268, 2005

    2005

  4. [3]

    Discernible elements in models for Peano arithmetic.J

    Andrzej Ehrenfeucht. Discernible elements in models for Peano arithmetic.J. Symb. Log., 38:291–292, 1973

    1973

  5. [4]

    Variations on a Visserian theme

    Ali Enayat. Variations on a Visserian theme. InA tribute to Albert Visser, volume 30 ofTributes, pages 99–110. College Publications, London, 2016

    2016

  6. [5]

    Completions of restricted complexity I, weak arithmetical theories

    Ali Enayat, Mateusz Łełyk, and Albert Visser. Completions of restricted complexity I, weak arithmetical theories. Preprint, available at arXiv:2508.14758, 2025

    arXiv 2025

  7. [6]

    Categoricity-like properties in the first order realm

    Ali Enayat and Mateusz Łełyk. Categoricity-like properties in the first order realm. J. Phil. Math., 1:63–98, 2024

    2024

  8. [7]

    Arithmetization of metamathematics in a general setting.Fund

    Solomon Feferman. Arithmetization of metamathematics in a general setting.Fund. Math., 49:35–92, 1960/61

    1960

Show all 29 references
  1. [8]

    Bi-interpretation in weak set theories

    Alfredo Roque Freire and Joel David Hamkins. Bi-interpretation in weak set theories. J. Symb. Log., 86(2):609–634, 2021

    2021

  2. [9]

    Williams

    Alfredo Roque Freire and Kameryn J. Williams. Non-tightness in class theory and second-order arithmetic.J. Symb. Log., 90(2):627–654, 2025

    2025

  3. [10]

    When bi-interpretability implies synonymy

    Harvey Friedman and Albert Visser. When bi-interpretability implies synonymy. Review of Symbolic Logic, pages 1–20, forthcoming

  4. [11]

    Separationsbetweendefinitenesspropertiesforsequentialtheories[work- ing title]

    PiotrGruza. Separationsbetweendefinitenesspropertiesforsequentialtheories[work- ing title]. in preparation

  5. [12]

    Perspectives in Mathematical Logic

    PetrHájekandPavelPudlák.Metamathematics of first-order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1998. Second printing

    1998

  6. [13]

    Cambridge University Press, Cambridge, 2011

    Volker Halbach.Axiomatic theories of truth. Cambridge University Press, Cambridge, 2011

    2011

  7. [14]

    Cambridge University Press, Cambridge, 1993

    Wilfrid Hodges.Model theory, volume 42 ofEncyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1993

    1993

  8. [15]

    Sequence encoding without induction.Math

    Emil Jeřábek. Sequence encoding without induction.Math. Log. Q., 58(3):244–248, 2012. 42

    2012

  9. [16]

    The Clarendon Press, Oxford University Press, New York, 1991

    Richard Kaye.Models of Peano Arithmetic, volume 15 ofOxford Logic Guides. The Clarendon Press, Oxford University Press, New York, 1991. Oxford Science Publica- tions

    1991

  10. [17]

    The theory ofκ-like models of arithmetic.Notre Dame J

    Richard Kaye. The theory ofκ-like models of arithmetic.Notre Dame J. Formal Logic, 36(4):547–559, 1995

    1995

  11. [18]

    Kossak and J

    R. Kossak and J. Schmerl.The Structure of Models of Peano Arithmetic. Oxford University Press, 2006

    2006

  12. [19]

    Flexible

    Saul A. Kripke. “Flexible” predicates of formal number theory.Proc. Amer. Math. Soc., 13:647–650, 1962

    1962

  13. [20]

    Universal properties of truth.J

    Mateusz Łełyk and Bartosz Wcisło. Universal properties of truth.J. Math. Log.,

  14. [22]

    Relatively precomplete numerations and arithmetic.J

    Franco Montagna. Relatively precomplete numerations and arithmetic.J. Philos. Logic, 11(4):419–430, 1982

    1982

  15. [23]

    A generalization of the incompleteness theorem.Fund

    Andrzej Mostowski. A generalization of the incompleteness theorem.Fund. Math., 49:205–232, 1960/61

    1960

  16. [24]

    How to escape Tennenbaum’s theorem

    Fedor Pakhomov. How to escape Tennenbaum’s theorem. Preprint, available at arXiv:2209.00967, 2022

    2022 arXiv

  17. [25]

    Some prime elements in the lattice of interpretability types.Trans

    Pavel Pudlák. Some prime elements in the lattice of interpretability types.Trans. Amer. Math. Soc., 280(1):255–275, 1983

    1983

  18. [26]

    An inside view ofEXP; or, The closed fragment of the provability logic ofI∆ 0 + Ω1 with a propositional constant forEXP.J

    Albert Visser. An inside view ofEXP; or, The closed fragment of the provability logic ofI∆ 0 + Ω1 with a propositional constant forEXP.J. Symb. Log., 57(1):131–165, 1992

    1992

  19. [27]

    Categories of theories and interpretations

    Albert Visser. Categories of theories and interpretations. InLogic in Tehran, vol- ume 26 ofLect. Notes Log., pages 284–341. Assoc. Symbol. Logic, La Jolla, CA, 2006

    2006

  20. [28]

    The small-is-very-small principle.MLQ Math

    Albert Visser. The small-is-very-small principle.MLQ Math. Log. Q., 65(4):453–478, 2019

    2019

  21. [29]

    A. J. Wilkie. On schemes axiomatizing arithmetic. InProceedings of the International Congress of Mathematicians, Vol. 1, 2 (Berkeley, Calif., 1986), pages 331–337. Amer. Math. Soc., Providence, RI, 1987. 43

    1986

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.