On the decidability of Presburger arithmetic expanded with powers

We prove that for any integers α, β > 1, the existential fragment of the first-order theory of the structure ❬Z; 0, 1, <, +, α^N, β^N❭ is decidable (where α^N is the set of positive integer powers of α, and likewise for β^N). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of ❬N; 0, 1, <, +, x↦α^x, x↦β^x❭ for any multiplicatively independent α, β > 1 would lead to mathematical breakthroughs regarding base-α and base-β expansions of certain transcendental numbers. Finally, modifying the original proof of Hieronymi and Schulz we show that for any multiplicatively independent α, β > 1, it is undecidable whether a given formula with at most 3 alternating blocks of quantifiers holds in ❬N; 0, 1, <, +, α^N, β^N❭.

Proceedings of SODA 25, 2025. 24 pages.

PDF © 2025 SIAM.