Axiomatizations of Presburger Arithmetic With Predicates For Powers

TL;DR

This paper provides a complete axiomatization of Presburger arithmetic extended with predicates for powers of integers, establishing decidability results for structures involving two multiplicatively independent bases.

Contribution

It introduces a new axiomatization for Presburger arithmetic with power predicates and proves its computability and decidability for structures with two independent bases.

Findings

A complete first-order axiomatization for the structure with power predicates.

Decidability of the structure $( Z,+,k^{ N}, L^{ N})$ for two bases.

Axiomatization of the universal theory with order and power predicates.

Abstract

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