💻 computer science

On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

This paper establishes the decidability of single-variable expansions of Presburger arithmetic for perfect fixed powers and cubic polynomials by leveraging results on hyperelliptic Diophantine equations and low-genus algebraic curves, while demonstrating that lifting these restrictions leads to undecidability through encodings of open Diophantine problems.

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

Published 2026-05-19

📖 5 min read🧠 Deep dive

CC BY 4.0

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

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a detective trying to solve a massive puzzle. The puzzle is a set of mathematical rules about whole numbers (like 1, 2, 3, -5, etc.). Your goal is to determine if a specific statement about these numbers is true or false.

In the world of math, this is called Presburger Arithmetic. It's like a game with strict rules: you can add, subtract, compare sizes, and check if numbers are even or odd. For a long time, we knew this game was "solvable" (decidable)—meaning there's a guaranteed method to answer any question you ask, even if it takes a long time.

However, the paper you're asking about explores what happens when we add new, tricky rules to this game. Specifically, we add rules about polynomials (mathematical expressions like $x^2$ , $x^3$ , or $2n^3 - 5n + 3$ ).

The Big Problem: The "Too Many Variables" Trap

The authors explain that if you let the puzzle get too complicated—specifically, if you allow many different numbers (variables) to interact with these new polynomial rules—the game becomes unsolvable. It's like trying to find a needle in a haystack that keeps growing forever; no computer, no matter how powerful, can guarantee an answer.

This is because these new rules are powerful enough to encode the famous "Hilbert's Tenth Problem," which was proven impossible to solve in general.

The Solution: The "One-Variable" Shortcut

The authors' main discovery is a clever workaround. They ask: What if we limit the game to use only one variable at a time?

Imagine you are trying to find a specific number $x$ that satisfies a list of conditions. Even though the conditions involve complex shapes (polynomials), if you are only looking for one number, the problem becomes solvable again.

The paper proves that for single-variable puzzles, we can decide the answer in two specific scenarios:

The "Perfect Power" Case:
Imagine you are looking for numbers that are perfect squares ($1, 4, 9, 16...$), perfect cubes ($1, 8, 27...$), or any fixed power. The authors show that if your puzzle only involves these "perfect power" shapes, you can solve it. They use deep math about "hyperelliptic equations" (fancy curves) to prove that the solutions are either finite or follow a predictable pattern that a computer can check.
The "Low-Shape" Case:
Imagine the shapes are limited to simple curves: lines (degree 1), parabolas (degree 2), or cubic curves (degree 3). The authors prove that if your puzzle only uses these simple shapes, it is also solvable. They rely on the fact that these shapes don't get "twisted" enough to create an infinite, unsolvable mess.

How They Do It: The "Density" Trick

The authors use a brilliant strategy to handle "negative" rules (e.g., "Find a number that is NOT a perfect square").

The Positive Rules: First, they find all the numbers that fit the "positive" rules (e.g., numbers that are perfect squares). Sometimes there are infinitely many.
The Negative Rules: Then, they apply the "negative" rules. They prove that even if you have to exclude numbers, the numbers you exclude are so sparse (like finding a few specific grains of sand on a beach) that they don't wipe out the entire beach.
The Conclusion: If the "positive" list is infinite, and the "negative" rules only remove a tiny, insignificant fraction of it, then there are still infinitely many numbers left. The computer can say, "Yes, a solution exists!" without needing to find the exact number.

Real-World Examples from the Paper

The authors show that this logic can solve famous historical math riddles, provided they are phrased as single-variable puzzles:

Fermat's Triangular Numbers: Proving there is no triangular number (like 1, 3, 6, 10) larger than 1 that is also a perfect cube.
Fibonacci Cubes: Proving that 8 is the largest cube in the Fibonacci sequence.
Catalan's Conjecture: Checking if 9 and 8 are the only perfect powers with a difference of exactly 1.

The Limit: When Two Variables Break the Game

The paper also draws a hard line. If you allow two variables (looking for two numbers, $x$ and $y$ , that work together), the game becomes unsolvable again, even if you only use perfect squares.

They illustrate this with the "Perfect Euler Brick" problem: Can you build a rectangular box where all sides and all diagonals are whole numbers? This is a 3-variable problem. The authors show that if we could solve our single-variable game for two variables, we could solve this brick problem. Since the brick problem is still an unsolved mystery after 300 years, our two-variable game must also be unsolvable.

Summary

The Good News: If you restrict your math puzzles to one variable and use either "perfect powers" or "simple curves" (up to degree 3), you can always write a computer program to tell you if a solution exists.
The Bad News: As soon as you add a second variable or use more complex curves, the puzzle becomes impossible to solve in general.
The Method: They use a mix of ancient number theory (Diophantine equations) and modern geometry to prove that the "good" puzzles have patterns we can exploit, while the "bad" ones are too chaotic.

This paper doesn't build a new app or cure a disease; it simply maps the boundaries of what is computable in the world of numbers, showing us exactly where the "magic" of solvability ends and the "chaos" of the unknown begins.

Technical Summary: On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

Problem Statement
Presburger arithmetic, the first-order theory of integers with addition and order, is decidable. However, its expansion by non-linear predicates, such as the set of perfect squares ( $Z^2$ ) or general polynomial images, is known to be undecidable in the general case. This undecidability stems from the ability to encode multiplication within these theories. While the decidability of the existential fragment of such expansions remains a major open problem (e.g., Büchi's conjecture regarding perfect squares), this paper investigates a different avenue for recovering decidability: restricting the number of variables.

The authors focus on variable-bounded expansions of Presburger arithmetic with families of monadic polynomial predicates. Specifically, they examine fragments where the number of distinct variables is bounded by a constant $k$ (denoted as $FO_k$ , $\exists FO_k$ , and $SMT_k$ ). The central challenge is that even for a single variable ( $k=1$ ), the decidability of whether two polynomial predicates intersect (e.g., $f(u) = g(v)$ ) is a severely restricted instance of Hilbert's tenth problem, which is generally open.

Methodology
The paper employs a combination of number-theoretic, algebraic-geometric, and measure-theoretic techniques to analyze the solution sets of constraints within these bounded-variable fragments.

Pre-processing and Reduction: The decision procedure begins by reducing arbitrary sentences to a satisfiability problem involving a conjunction of constraints. These constraints include linear inequalities ( $x > c$ ), modular arithmetic ( $x \equiv_m c$ ), and polynomial predicates of the form $R(ax+b)$ or their negations $\neg R(ax+b)$ . The authors utilize the Chinese Remainder Theorem to consolidate modular constraints and perform case analysis to eliminate bounded intervals, reducing the problem to determining the satisfiability of constraints over an unbounded domain.
Handling Positive Constraints: The core of the methodology involves characterizing the solution sets of systems of positive polynomial constraints.
- For fixed powers (e.g., $Z_k = \{n^k\}$ ), the authors leverage results on hyperelliptic Diophantine equations. They show that the intersection of two such constraints yields a finite set (if degrees are high enough) or a set parametrized by linear recurrence sequences (LRS) if the degrees are 2.
- For general polynomials of degree at most 3, the analysis relies on the genus of the resulting algebraic curves. Systems involving cubic polynomials often lead to curves of genus 1 (elliptic curves) or higher, which have finitely many integer points by Siegel's theorem or Baker's bounds. Systems involving quadratic polynomials relate to Pell equations, whose solutions form reversible LRS.
Handling Negative Constraints (Density Arguments): A crucial insight is that when the solution set to positive constraints is infinite, the set of solutions violating a negative constraint (i.e., satisfying the positive version of the negated predicate) has relative density zero within the original solution set.
- For polynomial images, the growth rate of the image is polynomial, whereas the "forbidden" set (if it arises from a different polynomial) often grows at a different rate or is sparse.
- In cases where the solution set is an LRS, the authors prove that the indices of the "forbidden" solutions form arithmetic progressions. This allows for an effective check to determine if any solutions remain after excluding the null-density subset.
Redundancy and Coalescence: The authors define notions of "redundant" and "similar" constraints. Redundant constraints can be discarded, while similar constraints can be coalesced into a single constraint using $p$ -adic valuations and the Chinese Remainder Theorem, simplifying the system before applying the density arguments.

Key Contributions and Results

The paper establishes two primary decidability results for single-variable theories ( $k=1$ ):

Decidability with Fixed Powers: The theory $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$ is decidable. This result relies on the solvability of hyperelliptic Diophantine equations ( $w^k - nz^j = N$ ) and the fact that systems of such equations have finitely many solutions or solutions parametrized by LRS.
Decidability with Low-Degree Polynomials: The theory $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$ is decidable, where each $R_i$ corresponds to the image of an integer-valued polynomial of degree at most 3. This result utilizes the low genus of the associated algebraic curves (genus 0 or 1) and the structure of solutions to simultaneous Pell equations.

Undecidability Results
To delineate the boundaries of these positive results, the paper provides undecidability proofs when the variable bound is lifted or specific predicates are combined:

The existential fragment $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$ is undecidable. This is shown by encoding the negation of Büchi's conjecture, which allows for the definition of multiplication using a limited number of variables.
Using Jones's universal Diophantine equations and Xiao's recent proof of Büchi's conjecture, the authors establish that theories with significantly higher variable counts (e.g., $SMT_{600}$ or $SMT_{2200}$ with $Z^2$ ) are undecidable.

Significance
The paper's significance lies in identifying precise boundaries where decidability can be recovered in non-linear expansions of Presburger arithmetic. By restricting the number of variables to one, the authors demonstrate that deep results from Diophantine geometry (such as the finiteness of integer points on curves of genus $\ge 2$ ) and the theory of linear recurrence sequences are sufficient to construct decision procedures.

The work highlights a dichotomy: while general non-linear expansions are undecidable, and even the existential fragment with two variables and perfect squares is undecidable, the single-variable case remains tractable for broad families of predicates. The authors note that extending these results to two or three variables is obstructed by famous open problems, such as the existence of perfect Euler bricks (requiring 3 variables and $Z^2$ ) and the sum-of-three-cubes problem (requiring 2 variables and $Z^3$ ). Thus, the paper provides a rigorous framework for understanding the computational complexity of arithmetic theories constrained by variable bounds.