On the Decidability of Presburger Arithmetic Expanded with Powers

Abstract

We prove that for any integers $\hat{I}\pm ,{\hat{I}}^2>1$, the existential fragment of the first-order theory of the structure $\langle \mathbb{Z}; 0,1,<, +, α^{\mathbb{N}}, β^{\mathbb{N}}\rangle$ is decidable (where $\hat{I}{\pm }^{\mathbb{N}}$ is the set of positive integer powers of $\hat{I}\pm$, and likewise for $β^{\mathbb{N}}$). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of $\langle \mathbb{N}; 0,1, <, +, x\mapsto α^x, x \mapsto β^x\rangle$ for any multiplicatively independent $\hat{I}\pm ,{\hat{I}}^2>1$ would lead to mathematical breakthroughs regarding base-$\hat{I}\pm$ and base-${\hat{I}}^2$ expansions of certain transcendental numbers.

SODA 2025