Axiomatizations of Presburger Arithmetic With Predicates For Powers

We give a complete first-order axiomatization of the structure $(\mathbb{Z},+,({\mathrm{\ell }}^{\mathbb{N}}{)}_{\mathrm{\ell }\in L})$, where $L\subseteq {\mathbb{Z}}_{\ge 2}$ is a set of pairwise multiplicatively independent integers and ${\mathrm{\ell }}^{\mathbb{N}}=\{{\mathrm{\ell }}^n:n\in \mathbb{N}\}$. Using recent work of Karimov et al., we obtain that this axiomatization is computable for $\mathrm{\mid }L\mathrm{\mid }=2$, which proves that $(\mathbb{Z},+,k^{\mathbb{N}},{\mathrm{\ell }}^{\mathbb{N}})$ is decidable for $k,\mathrm{\ell }\in {\mathbb{Z}}_{\ge 2}$. Furthermore, we give an axiomatization of the universal theory of $(\mathbb{Z},+,<,({\mathrm{\ell }}^{\mathbb{N}}{)}_{\mathrm{\ell }\in L})$.