What structures lie between the decidable and well-understood Presburger Arithmetic \((\mathbb{Z},+,<)\) and the wild and undecidable structure \((\mathbb{Z},+,\times)\)? A natural class of examples comes from considering \(\ell^{\mathbb{N}} = \{\ell^n : n \in \mathbb{N}\}\) for \(\ell \in \mathbb{N}\). It follows from work of Büchi (1960) that \((\mathbb{Z} +,<,2^{\mathbb{N}})\) is decidable. Progress on the expansion of Presburger Arithmetic by two predicates for powers has only been made recently: \((\mathbb{Z},+,<,2^{\mathbb{N}},3^{\mathbb{N}})\) is undecidable (Hieronymi, Schulz; 2022) but existentially decidable (Karimov, Luca, Nieuwveld, Ouaknine, Worrell; 2025).

We axiomatize the first-order theory of \((\mathbb{Z},+,2^\mathbb{N},3^\mathbb{N})\). Using the algorithms of Karimov et al., we obtain that this axiomatization is computable, which establishes decidability of the theory. Furthermore, we axiomatize the universal theory of \((\mathbb{Z},+,<,2^\mathbb{N},3^\mathbb{N})\).

This is joint work with Philipp Hieronymi and Xiaoduo Wang.