Definition of Presburger Arithmetic

Minimalistic Language of Presburger Arithmetic

Consider $L=\{+\}$ and consider as ${\cal I}$ the set of all interpretations with domain $\mathbb{N} = \{0,1,2,\ldots\}$ where $+$ is interpreted as addition of natural numbers (these interpretations differ only in values for free variables. This is one definition of Presburger arithmetic over natural numbers.

This theory is very simple to describe, but it is very far from allowing quantifier-elimination. For example, it does not have a name for zero, so we cannot express $\forall x. x+y=x$ . It also does not have a way to express $\exists y. x+y=z$ .

Language of Presburger Arithmetic that Admits QE

We look at the theory of integers with addition.

introduce constant for each integer constant
to be able to restrict values to natural numbers when needed: we introduce $<$
introduce not only addition but also subtraction
to conveniently express certain expressions, introduce function $m_K$ for each $K \in {\cal Z}$ , to be interpreted as multiplication by a constant, $m_K(x)= K \cdot x$ . We write $m_K$ as $K \cdot x$
to enable quantifier elimination from $\exists x. y= K \cdot x$ introduce for each $K$ predicate $K|y$ (divisibility by constant)

The resulting language

$\begin{equation*} L = \{ +, -, < \} \cup \{ K \mid K \in \mathbb{Z}\} \cup \{ (K \cdot \_) \mid K \in \mathbb{Z} \} \cup \{ (K|\_) \mid K \in \mathbb{Z} \} \end{equation*}$