On existential Büchi arithmetic in two coprime bases

Technical Summary: On Existential Büchi Arithmetic in Two Coprime Bases

Problem Statement
The paper addresses the decidability of the existential fragment of first-order logic over the integers, expanded with order, addition, and two Büchi predicates, denoted as $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$. Here, $V_z(x, y)$ holds if and only if $y$ is the largest power of $z$ dividing $x$.

The context is established by Villemaire (1992), who proved that the full first-order theory $\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ is undecidable when $\alpha$ and $\beta$ are multiplicatively independent, as the structure can encode multiplication. Subsequent research by Hieronymi and Schulz (2021) showed that replacing the Büchi predicates with weaker power predicates ($\alpha^\mathbb{N}, \beta^\mathbb{N}$) also yields an undecidable theory. However, Karimov et al. (2025) demonstrated that the existential fragment of the theory with power predicates is decidable for multiplicatively independent bases.

The open problem addressed in this paper is whether the existential fragment remains decidable when the predicates are the stronger Büchi predicates ($V_\alpha, V_\beta$) rather than simple power sets. The author settles this question specifically for the case where the bases $\alpha$ and $\beta$ are coprime.

Methodology
The proof proceeds via a quantifier-elimination argument that transforms an existential formula into a system of linear inequalities and modular constraints involving powers of $\alpha$ and $\beta$. The methodology relies on several key mathematical tools and structural reductions:

1. Reduction to Systems of Inequalities:
   The author first reduces the existential formula to a system involving "pure power variables" ($z^n$) and "linear power variables" ($x \cdot z^n$). This system consists of linear inequalities ($Ax > v$) and modular constraints, some with constant moduli and others with variable moduli (of the form $d \cdot z^n$).

2. Structural Decomposition (Levels and Bottom Family):
   To manage the complexity of the variables, the author partitions the variables into "levels" based on their relative magnitudes. Variables on the same level have ratios bounded by a constant, while variables on different levels can have arbitrarily large ratios.

   • Levels: Defined via the recession cone of the polyhedron $Ax > v$.
   • Bottom Family: A subset of variables (specifically those with "small coefficients") that are treated together. The author defines a "bottom family" such that the projection of the polyhedron onto these variables is not "thin" (i.e., not bounded in a specific linear direction).

3. Iterative Reduction and Normalization:
   The core of the algorithm involves reducing the system to satisfy a specific list of properties (Properties 1–4c). These properties ensure:

   • Variables are ordered strictly ($x_1 > \dots > x_t > 0$).
   • The polyhedron is not thin.
   • Modular constraints with variable moduli are handled such that the modulus base is not in the bottom family.
   • Orthogonal subspaces of levels satisfy specific non-degeneracy conditions regarding the exponential bases.

   Achieving these properties involves applying Baker's theorem (on linear forms in logarithms) to bound exponents and Kronecker's theorem on Diophantine approximation to ensure density of ratios.

4. Handling Modular Constraints:
   A critical technical contribution is the handling of modular constraints with variable moduli ($x \equiv c \pmod{z^n}$). The author utilizes Lemma 33, which relies on the coprimality of $\alpha$ and $\beta$. This lemma states that the set of residues $\{\beta^n \pmod{\alpha^m}\}$ stabilizes in structure for large $m$. This allows the author to "blow up" the exponents, effectively converting variable modulus constraints into constant modulus constraints (or constraints with fixed periodicity) by scaling the variables.

5. Quantifier Elimination:
   Once the system is normalized and the moduli are fixed (or reduced to constant cases), the author applies a lifting argument. They show that if the system is satisfiable, there exists a solution where the variables outside the bottom family are sufficiently large. The remaining variables (in the bottom family) are treated as linear integers within specific modular classes. By eliminating these linear variables, the system is reduced to a strictly smaller set of variables, eventually leading to a quantifier-free decision.

Key Contributions and Results

• Main Theorem: The paper proves that for coprime integers $\alpha, \beta \ge 2$, the existential fragment $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$ is decidable.
• Generalization of Prior Work: This result extends the decidability result of Karimov et al. (which applied to power predicates $\alpha^\mathbb{N}, \beta^\mathbb{N}$) to the more expressive Büchi predicates $V_\alpha, V_\beta$, under the stronger condition of coprimality.
• Technical Lemmas: The paper provides specific lemmas (e.g., Lemma 33) describing the structure of powers modulo powers of coprime bases, which are essential for the reduction of variable modulus constraints.
• Algorithmic Construction: The proof is constructive, providing a method to compute the necessary bounds, partitions, and substitutions to eliminate quantifiers.

Significance and Limitations
The paper claims to settle the decidability question for the existential fragment of Villemaire's original expansion for coprime bases. The author explicitly notes that their reliance on coprimality is a significant constraint.

• Dependence on Coprimality: The proof uses coprimality twice: once in the application of Baker's theorem (Lemma 12) and, more critically, in Lemma 33 regarding the structure of $\beta^n \pmod{\alpha^m}$. The author states that for non-coprime, multiplicatively independent bases, the set of residues behaves more irregularly (growing linearly rather than stabilizing), and they do not know how to circumvent this issue.
• Scope: The result is specific to the existential fragment. The full theory remains undecidable.
• Future Directions: The author discusses that extending this to more than two predicates (e.g., three power predicates) would likely require Schanuel's conjecture to handle linear independence of logarithms. They also note that the problem for general multiplicatively independent (non-coprime) bases remains open and likely requires new ideas, possibly involving $p$-adic versions of Baker's theorem.

In summary, the paper establishes a decidability frontier for existential Büchi arithmetic, bridging the gap between power predicates and full Büchi predicates, but explicitly acknowledges that the general case of multiplicatively independent bases remains an open challenge.