Document Open Access Logo

On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Authors Piotr Bacik , Joris Nieuwveld , Joël Ouaknine , Mihir Vahanwala , Madhavan Venkatesh , Emil Rugaard Wieser

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.7.pdf
  • Filesize: 0.82 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Presburger arithmetic
  • Diophantine equations
  • decidability
  • Büchi’s conjecture

Metrics

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³-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 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. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.

Cite As Get BibTex

Piotr Bacik, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, Madhavan Venkatesh, and Emil Rugaard Wieser. On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.7

Author Details

Piotr Bacik
  • University of Oxford, UK
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Joris Nieuwveld
  • University of Oxford, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Mihir Vahanwala
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Madhavan Venkatesh
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Emil Rugaard Wieser
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

P. Bacik is supported by EPSRC grant EP/X033813/1. P. Bacik, J. Ouaknine, M. Vahanwala, M. Venkatesh, and E. R. Wieser are supported by ERC grant DynAMiCs (101167561) and DFG grant 389792660 as part of https://perspicuous-computing.science. J. Nieuwveld is supported by the Glasstone Benefaction, University of Oxford [Violette and Samuel Glasstone Research Fellowships in Science 2025].

Acknowledgements

J. Ouaknine is also affiliated with Keble College, Oxford as https://www.emmy.network/ Fellow.

References

  1. Alan Baker. Bounds for the solutions of the hyperelliptic equation. Mathematical Proceedings of the Cambridge Philosophical Society, 65(2):439-444, 1969. URL: https://doi.org/10.1017/S0305004100044418.
  2. Alan Baker. Transcendental Number Theory. Cambridge Mathematical Library. Cambridge University Press, 1975. 1994 Reprinted Edition. Google Scholar
  3. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, Paderborn, Germany, July 10-14, 2023, LIPIcs, pages 112:1-112:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.112.
  4. Jean Berstel and Christophe Reutenauer. Noncommutative rational series with applications, volume 137. Cambridge University Press, 2011. Google Scholar
  5. Alexis Bès. A survey of arithmetical definability. A tribute to Maurice Boffa, Special Issue of Belgian Mathematical Society, pages 1-54, 2002. Google Scholar
  6. Yann Bugeaud, Maurice Mignotte, and Samir Siksek. Classical and modular approaches to exponential Diophantine equations I. Fibonacci and Lucas perfect powers. Annals of Mathematics, 163(3):969-1018, 2006. Google Scholar
  7. Paul-Jean Cahen and Jean-Luc Chabert. What you should know about integer-valued polynomials. The American Mathematical Monthly, 123(4):311-337, 2016. URL: https://doi.org/10.4169/amer.math.monthly.123.4.311.
  8. Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer linear-exponential programming in NP by quantifier elimination. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, LIPIcs, pages 132:1-132:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.132.
  9. Pierre Fatou. Sur les séries entières à coefficients entiers. Comptes Rendus de l'Académie des Sciences, Paris, 138(130):342-344, 1904. Google Scholar
  10. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3(1):53-69, 1997. URL: https://doi.org/10.2307/421196.
  11. Erich Grädel and Martin Otto. On logics with two variables. Theoretical Computer Science, 224(1-2):73-113, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00308-9.
  12. Martin Grohe. Finite variable logics in descriptive complexity theory. The Bulletin of Symbolic Logic, 4(4):345-398, 1998. URL: https://doi.org/10.2307/420954.
  13. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  14. Philipp Hieronymi and Christian Schulz. A strong version of Cobham’s theorem. In Stefano Leonardi and Anupam Gupta, editors, STOC '22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 1172-1179. ACM, 2022. URL: https://doi.org/10.1145/3519935.3519958.
  15. Michael J. Jacobson Jr. and Hugh C. Williams. Solving the Pell equation. Springer, New York, 2009. Google Scholar
  16. Gareth A. Jones and Josephine M. Jones. Elementary Number Theory. Springer Undergraduate Mathematics Series. Springer London, 1998. Google Scholar
  17. James P. Jones. Universal Diophantine Equation. The Journal of Symbolic Logic, 47(3):549-571, 1982. URL: https://doi.org/10.2307/2273588.
  18. Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, and James Worrell. On the Decidability of Presburger Arithmetic Expanded with Powers. In Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 2755-2778, 2025. URL: https://doi.org/10.1137/1.9781611978322.89.
  19. Kazuya Kato, Nobushige Kurokawa, and Takeshi Saitō. Number Theory: Fermat’s dream, volume 186 of Translations of Mathematical Monographs; Iwanami Series in Modern Mathematics. American Mathematical Society, 2000. Google Scholar
  20. Alessio Mansutti and Mikhail R. Starchak. One-parametric Presburger arithmetic has quantifier elimination. In Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025, Warsaw, Poland, August 25-29, 2025, LIPIcs, pages 72:1-72:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.72.
  21. Preda Mihăilescu. Primary cyclotomic units and a proof of Catalan’s conjecture. Journal für die reine und angewandte Mathematik, 2004(572):167-195, 2004. URL: https://doi.org/10.1515/crll.2004.048.
  22. Martin Otto. Bounded variable logics and counting - a study in finite models, volume 9 of Lecture Notes in Logic. Springer, 1997. Google Scholar
  23. Hector Pasten and Xavier Vidaux. Positive existential definability of multiplication from addition and the range of a polynomial. Israel Journal of Mathematics, 216:273-306, 2016. URL: https://doi.org/10.1007/s11856-016-1410-x.
  24. Françoise Point. On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers. The Journal of Symbolic Logic, 65(3):1347-1374, 2000. URL: https://doi.org/10.2307/2586704.
  25. Dimitrios Poulakis and Evaggelos Voskos. On the Practical Solution of Genus Zero Diophantine Equations. Journal of Symbolic Computation, 30(5):573-582, 2000. URL: https://doi.org/10.1006/jsco.2000.0420.
  26. Ian Pratt-Hartmann. Fragments of first-order logic, volume 56 of Oxford Logic Guides. Oxford University Press, 2023. Google Scholar
  27. Paulo Ribenboim. Catalan’s conjecture. The American Mathematical Monthly, 103(7):529-538, 1996. Google Scholar
  28. Hans P. Schlickewei and Wolfgang M. Schmidt. Linear equations in members of recurrence sequences. Annali della Scuola Normale Superiore di Pisa - Classe di Scienze, 20(2):219-246, 1993. URL: http://eudml.org/doc/84147.
  29. Zhi-Wei Sun. Further results on Hilbert’s Tenth Problem. Science China Mathematics, 64(2):281-306, 2021. URL: https://doi.org/10.1007/s11425-020-1813-5.
  30. László Szalay. On the resolution of simultaneous Pell equations. Annales Mathematicae et Informaticae, 34:77-87, 2007. URL: http://eudml.org/doc/128842.
  31. Nikos Tzanakis. Effective solution of two simultaneous Pell equations by the elliptic logarithm method. Acta Arithmetica, 103(2):119-135, 2002. Google Scholar
  32. Raymond E. Whitney. Advanced problems and solutions. The Fibonacci Quarterly, 10(4):417-422, 1972. Google Scholar
  33. Stanley Yao Xiao. Hilbert’s tenth problem for systems of diagonal quadratic forms, and Büchi’s problem, 2025. URL: https://arxiv.org/abs/2412.16740.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact