On the Decidability of Presburger Arithmetic Expanded with Powers

Abstract

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

SODA 2025