pith. sign in

arxiv: 2605.16985 · v1 · pith:BVSMKMZAnew · submitted 2026-05-16 · 💻 cs.LO

On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Piotr Bacik , Joris Nieuwveld , Jo\"el Ouaknine , Mihir Vahanwala , Madhavan Venkatesh , Emil Rugaard Wieser This is my paper

Pith reviewed 2026-05-19 18:47 UTC · model grok-4.3

classification 💻 cs.LO
keywords Presburger arithmeticdecidabilityDiophantine equationsalgebraic curvesmonadic predicatesvariable-bounded theoriesexpansions of arithmetic
0
0 comments X

The pith

The first-order theory of single-variable Presburger arithmetic expanded by perfect fixed powers or degree-at-most-three polynomials is decidable.

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

Presburger arithmetic is the first-order theory of the integers under addition. Adding monadic predicates for sets defined by polynomials makes the full multi-variable theory undecidable. The paper shows that restricting to single-variable formulas restores decidability in two cases. For predicates selecting perfect fixed powers, the decision problem reduces to the solvability of hyperelliptic Diophantine equations. For predicates given by polynomials of degree three or lower, decidability follows from the low genus of the associated algebraic curves. The authors also establish hardness results once the single-variable bound or the degree bound is lifted, by encoding longstanding open Diophantine problems.

Core claim

In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves.

What carries the argument

Reduction of satisfiability in the single-variable expanded structure to solvability of hyperelliptic Diophantine equations or to the genus of algebraic curves produced by the polynomial predicates.

If this is right

  • The single-variable theory remains decidable when the predicates are the sets of squares, cubes, or any fixed perfect powers, assuming the corresponding Diophantine equations are solvable.
  • Polynomial predicates of degree at most three produce decidable theories because the curves they define have genus low enough for known decision procedures to apply.
  • Allowing two or more variables immediately permits encodings of open Diophantine problems and yields hardness.
  • The same hardness appears as soon as polynomial predicates of degree four or higher are admitted even in the single-variable case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Results from Diophantine geometry can be imported wholesale to obtain new decidable fragments of arithmetic.
  • The boundary between degree three and four may mark a sharp transition whose precise location could be tested by examining specific degree-four predicates.
  • Similar genus or reduction arguments might apply to other monadic predicates beyond polynomials, such as exponential ones, if analogous algebraic objects can be defined.

Load-bearing premise

That decidability of the logical theory transfers directly from the solvability of the associated hyperelliptic Diophantine equations or from the low genus of the algebraic curves.

What would settle it

A concrete hyperelliptic Diophantine equation tied to a perfect fixed power predicate for which solvability is undecidable would falsify the positive result for that family.

read the original abstract

We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form $2n^3-5n+3$, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability ofthe corresponding theory follows from the solvability of hyperellipticDiophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper studies expansions of Presburger arithmetic by monadic predicates defined by polynomials (e.g., perfect powers or cubic polynomials). It focuses on the single-variable fragments and claims positive decidability results: for fixed perfect powers, decidability follows from solvability of hyperelliptic Diophantine equations; for polynomials of degree at most three, decidability follows from the low genus of the associated algebraic curves. Hardness results are obtained by encoding open Diophantine problems once the single-variable or degree restrictions are lifted.

Significance. If the reductions are made explicit and correct, the results are significant for delineating the boundary between decidable and undecidable fragments of Presburger expansions with non-linear predicates. The work usefully connects logical decidability questions to effective methods in Diophantine geometry (Baker's method for hyperelliptic equations and genus-based techniques such as Chabauty or Mordell-Weil for low-genus curves). Credit is due for identifying these specific families where known number-theoretic tools yield logical decidability.

major comments (1)
  1. Abstract (paragraph beginning 'In the case of single-variable theories'): The central claim that decidability 'follows from' the solvability of hyperelliptic Diophantine equations (for perfect fixed powers) or from low-genus curve methods (for degree ≤3 polynomials) is load-bearing, yet the provided text gives no explicit reduction steps, quantifier-elimination argument, or proof sketch showing how the logical theory reduces to the Diophantine decision procedure. Without these details the transfer cannot be verified and the claim remains unconfirmed.
minor comments (1)
  1. Abstract: typographical errors include 'decidability ofthe' (missing space) and 'hyperellipticDiophantine' (missing space).

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading and for recognizing the significance of connecting logical decidability with effective Diophantine methods. We address the single major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: Abstract (paragraph beginning 'In the case of single-variable theories'): The central claim that decidability 'follows from' the solvability of hyperelliptic Diophantine equations (for perfect fixed powers) or from low-genus curve methods (for degree ≤3 polynomials) is load-bearing, yet the provided text gives no explicit reduction steps, quantifier-elimination argument, or proof sketch showing how the logical theory reduces to the Diophantine decision procedure. Without these details the transfer cannot be verified and the claim remains unconfirmed.

    Authors: We agree that the abstract statement is concise and does not itself contain the reduction details. The body of the manuscript (Sections 3 and 4) supplies the explicit arguments: single-variable sentences over fixed-power predicates are rewritten, via quantifier elimination in Presburger arithmetic, as the existence of integer solutions to hyperelliptic equations, which are then decided using Baker's effective bounds; for degree-at-most-three predicates the associated curves have genus 0 or 1, so integer-point search reduces to the Mordell–Weil theorem or Chabauty’s method. To address the referee’s concern directly, we will add a short paragraph to the introduction (and a parenthetical sentence to the abstract) that outlines these two reduction steps and points to the relevant sections. This is a partial revision: the technical content is already present, but its visibility from the abstract will be improved. revision: partial

Circularity Check

0 steps flagged

No significant circularity; results transfer from external Diophantine geometry

full rationale

The paper's central positive results for single-variable theories explicitly reduce decidability to the solvability of hyperelliptic Diophantine equations (for perfect powers) and to the low genus of algebraic curves (for degree ≤3 polynomials). These are standard external results from number theory (Baker's method, Chabauty, Mordell-Weil) rather than parameters, definitions, or self-citations internal to the paper. The abstract states the transfer directly without any fitted-input renaming, self-definitional loop, or load-bearing self-citation chain. The derivation is therefore self-contained against external benchmarks, with no step that reduces by construction to the paper's own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on standard background facts from logic and number theory rather than new free parameters or invented entities.

axioms (2)
  • standard math Presburger arithmetic (integer addition) is decidable
    Well-known result invoked as the base theory being expanded.
  • domain assumption Solvability of hyperelliptic Diophantine equations is decidable in the relevant cases
    External number-theoretic fact used to obtain the logical decidability result.

pith-pipeline@v0.9.0 · 5707 in / 1362 out tokens · 42606 ms · 2026-05-19T18:47:29.306572+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages

  1. [2]

    Starchak , editor =

    Alessio Mansutti and Mikhail R. Starchak , editor =. One-Parametric. 50th International Symposium on Mathematical Foundations of Computer Science,. 2025 , url =. doi:10.4230/LIPICS.MFCS.2025.72 , timestamp =

    work page doi:10.4230/lipics.mfcs.2025.72 2025

  2. [4]

    The Complexity of

    Michael Benedikt and Dmitry Chistikov and Alessio Mansutti , editor =. The Complexity of. 50th International Colloquium on Automata, Languages, and Programming,. 2023 , url =. doi:10.4230/LIPICS.ICALP.2023.112 , timestamp =

    work page doi:10.4230/lipics.icalp.2023.112 2023

  3. [5]

    The American Mathematical Monthly , volume =

    Paulo Ribenboim , title =. The American Mathematical Monthly , volume =. 1996 , publisher =

    work page 1996

  4. [6]

    Primary cyclotomic units and a proof of

    Mih. Primary cyclotomic units and a proof of. Journal für die reine und angewandte Mathematik , doi =

    work page

  5. [7]

    Classical and modular approaches to exponential

    Bugeaud, Yann and Mignotte, Maurice and Siksek, Samir , journal=. Classical and modular approaches to exponential. 2006 , volume=

    work page 2006

  6. [8]

    The Fibonacci Quarterly , volume=

    Advanced problems and solutions , author=. The Fibonacci Quarterly , volume=. 1972 , publisher=

    work page 1972

  7. [9]

    Number Theory: Fermat's dream , series=

    Kato, Kazuya and Kurokawa, Nobushige and Sait. Number Theory: Fermat's dream , series=. 2000 , publisher=

    work page 2000

  8. [10]

    CoRR , volume =

    Christian Ikenmeyer and Igor Pak , title =. CoRR , volume =. 2022 , url =. doi:10.48550/ARXIV.2204.13149 , eprinttype =. 2204.13149 , timestamp =

    work page doi:10.48550/arxiv.2204.13149 2022

  9. [11]

    2023 , publisher=

    Fragments of first-order logic , author=. 2023 , publisher=

    work page 2023

  10. [12]

    On Logics with Two Variables , journal =

    Erich Gr. On Logics with Two Variables , journal =. 1999 , url =

    work page 1999

  11. [13]

    On the decision problem for two-variable first-order logic , journal =

    Erich Gr. On the decision problem for two-variable first-order logic , journal =. 1997 , url =

    work page 1997

  12. [14]

    The Bulletin of Symbolic Logic , volume =

    Martin Grohe , title =. The Bulletin of Symbolic Logic , volume =. 1998 , url =

    work page 1998

  13. [15]

    1997 , isbn =

    Martin Otto , title =. 1997 , isbn =

    work page 1997

  14. [16]

    On decidable extensions of

    Point, Fran. On decidable extensions of. The Journal of Symbolic Logic , volume=. 2000 , publisher=

    work page 2000

  15. [17]

    A tribute to Maurice Boffa, Special Issue of Belgian Mathematical Society , pages=

    A survey of arithmetical definability , author=. A tribute to Maurice Boffa, Special Issue of Belgian Mathematical Society , pages=. 2002 , publisher=

    work page 2002

  16. [18]

    Christoph Haase , title =

    work page

  17. [19]

    Thue, Axel , journal =

    work page

  18. [20]

    arXiv preprint arXiv:2408.11653 , year=

    Alp. arXiv preprint arXiv:2408.11653 , year=

    work page arXiv

  19. [21]

    1983 , publisher=

    Faltings, Gerd , journal=. 1983 , publisher=

    work page 1983

  20. [22]

    Siegel, Carl Ludwig , title =. Abh. Preuss. Akad. Wiss. Phys.-Math. Kl. , year =

    work page

  21. [23]

    Mathematika , volume =

    Baker, Alan , title =. Mathematika , volume =. doi:https://doi.org/10.1112/S0025579300002588 , year =

    work page doi:10.1112/s0025579300002588

  22. [24]

    and DAVENPORT, H

    BAKER, A. and DAVENPORT, H. , title =. The Quarterly Journal of Mathematics , volume =. 1969 , month =. doi:10.1093/qmath/20.1.129 , url =

    work page doi:10.1093/qmath/20.1.129 1969

  23. [25]

    , title =

    Pinch, R.G.E. , title =. Mathematical Proceedings of the Cambridge Philosophical Society , volume =

    work page

  24. [26]

    Szalay, László , journal =

    work page

  25. [27]

    The American Mathematical Monthly , volume =

    Paul-Jean Cahen and Jean-Luc Chabert , title =. The American Mathematical Monthly , volume =. 2016 , publisher =. doi:10.4169/amer.math.monthly.123.4.311 , URL =

    work page doi:10.4169/amer.math.monthly.123.4.311 2016

  26. [28]

    and Pheidas, T

    Pasten, H. and Pheidas, T. and Vidaux, X. , doi =. Journal of Mathematical Sciences , number =. 2010 , bdsk-url-1 =

    work page 2010

  27. [29]

    Theory of Computing , volume =

    Lovett, Shachar , title =. Theory of Computing , volume =. 2011 , pages =. doi:10.4086/toc.2011.v007a013 , publisher =

    work page doi:10.4086/toc.2011.v007a013 2011

  28. [30]

    Jones , journal =

    James P. Jones , journal =

    work page

  29. [31]

    Science China Mathematics , number =

    Sun, Zhi-Wei , doi =. Science China Mathematics , number =. 2021 , bdsk-url-1 =

    work page 2021

  30. [32]

    and Williams, Hugh C

    Jacobson Jr., Michael J. and Williams, Hugh C. , year=

    work page

  31. [33]

    2412.16740 , archivePrefix=

    Stanley Yao Xiao , year=. 2412.16740 , archivePrefix=

    work page arXiv

  32. [34]

    Lang, Serge , isbn =

    work page

  33. [35]

    and Jones, Josephine M

    Jones, Gareth A. and Jones, Josephine M. , title =. 1998 , series =

    work page 1998

  34. [36]

    Journal of Number Theory , doi =

    Pasten, Hector , year =. Journal of Number Theory , doi =

    work page

  35. [37]

    Positive existential definability of multiplication from addition and the range of a polynomial , volume =

    Pasten, Hector and Vidaux, Xavier , year =. Positive existential definability of multiplication from addition and the range of a polynomial , volume =. Israel Journal of Mathematics , doi =

    work page

  36. [38]

    Yann Bugeaud, Kálmán Győry , journal =

    work page

  37. [39]

    , date =

    Kiss, P. , date =. On common terms of linear recurrences , url =. Acta Mathematica Academiae Scientiarum Hungarica , number =. 1982 , bdsk-url-1 =. doi:10.1007/BF01897310 , id =

    work page doi:10.1007/bf01897310 1982

  38. [40]

    Effective solution of two simultaneous

    Tzanakis, Nikos , journal=. Effective solution of two simultaneous

    work page

  39. [41]

    , title=

    Anglin, W.S. , title=

    work page

  40. [42]

    Journal of Number Theory , doi =

    Cipu, Mihai and Maurice, Mignotte , year =. Journal of Number Theory , doi =

    work page

  41. [43]

    2002 , issn =

    Solving Genus Zero Diophantine Equations with at Most Two Infinite Valuations , journal =. 2002 , issn =. doi:https://doi.org/10.1006/jsco.2001.0515 , url =

    work page doi:10.1006/jsco.2001.0515 2002

  42. [44]

    2013 , publisher=

    Diophantine geometry: an introduction , author=. 2013 , publisher=

    work page 2013

  43. [45]

    Journal of Symbolic Computation , volume =

    On the. Journal of Symbolic Computation , volume =. 2000 , issn =. doi:https://doi.org/10.1006/jsco.2000.0420 , url =

    work page doi:10.1006/jsco.2000.0420 2000

  44. [46]

    Mathematical Proceedings of the Cambridge Philosophical Society , author=

    Bounds for the solutions of the hyperelliptic equation , volume=. Mathematical Proceedings of the Cambridge Philosophical Society , author=. 1969 , pages=. doi:10.1017/S0305004100044418 , number=

    work page doi:10.1017/s0305004100044418 1969

  45. [47]

    Diophantine definability of infinite discrete nonarchimedean sets and

    Bjorn Poonen and Alexandra Shlapentokh , pages =. Diophantine definability of infinite discrete nonarchimedean sets and. Journal für die reine und angewandte Mathematik , doi =. 2005 , lastchecked =

    work page 2005

  46. [48]

    Decidability for

    Philipp Hieronymi and Dun Ma and Reed Oei and Luke Schaeffer and Christian Schulz and Jeffrey Shallit , url =. Decidability for. 2024 , month =. doi:10.46298/lmcs-20(3:12)2024 , journal =

    work page doi:10.46298/lmcs-20(3:12)2024 2024

  47. [49]

    2022 , issn =

    How to prove that a sequence is not automatic , journal =. 2022 , issn =. doi:https://doi.org/10.1016/j.exmath.2021.08.001 , url =

    work page doi:10.1016/j.exmath.2021.08.001 2022

  48. [50]

    Bilu, Yuri and Tichy, Robert , journal =

    work page

  49. [51]

    1986 , publisher=

    Plane Algebraic Curves , author=. 1986 , publisher=

    work page 1986

  50. [52]

    Algorithmic Algebra and Number Theory: Selected Papers From a Conference Held at the University of Heidelberg in October 1997 , pages=

    Primary decomposition: algorithms and comparisons , author=. Algorithmic Algebra and Number Theory: Selected Papers From a Conference Held at the University of Heidelberg in October 1997 , pages=. 1999 , organization=

    work page 1997

  51. [53]

    The number of integral points on arcs and ovals , author=

    work page

  52. [54]

    , title =

    Pila, J. , title =. International Mathematics Research Notices , volume =. 1996 , month =. doi:10.1155/S1073792896000554 , url =

    work page doi:10.1155/s1073792896000554 1996

  53. [55]

    2008 , publisher=

    Rational algebraic curves: a computer algebra approach , author=. 2008 , publisher=

    work page 2008

  54. [56]

    and Lewis, D

    Davenport, H. and Lewis, D. and Schinzel, A , journal =. Polynomials of certain special types , url =

    work page

  55. [57]

    Logical theories of one-place functions on the set of natural numbers , volume =

    Semenov, Alexei , year =. Logical theories of one-place functions on the set of natural numbers , volume =. Mathematics of the USSR-Izvestiya , doi =

    work page

  56. [58]

    , title =

    Chistikov, Dmitry and Mansutti, Alessio and Starchak, Mikhail R. , title =. 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024) , pages =. 2024 , volume =. doi:10.4230/LIPIcs.ICALP.2024.132 , annote =

    work page doi:10.4230/lipics.icalp.2024.132 2024

  57. [59]

    Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) , year=

    Toghrul Karimov and Florian Luca and Joris Nieuwveld and Joël Ouaknine and James Worrell , title =. Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) , year=. doi:10.1137/1.9781611978322.89 , URL =

    work page doi:10.1137/1.9781611978322.89 2025

  58. [60]

    Kane and Pravesh K

    Hieronymi, Philipp and Schulz, Christian , title =. 2022 , isbn =. doi:10.1145/3519935.3519958 , booktitle =

    work page doi:10.1145/3519935.3519958 2022

  59. [61]

    Comptes Rendus de l'Acad

    Fatou, Pierre , title =. Comptes Rendus de l'Acad. 1904 , volume =

    work page 1904

  60. [62]

    2011 , publisher=

    Noncommutative rational series with applications , author=. 2011 , publisher=

    work page 2011

  61. [63]

    and Schmidt, Wolfgang M

    Schlickewei, Hans P. and Schmidt, Wolfgang M. , journal =. Linear equations in members of recurrence sequences , url =

    work page