Presburger arithmetic

Example

Presburger arithmetic is the first-order theory of the natural numbers with $0$, $1$ and addition. It is the set of all sentences in the signature $\set{0, 1, +}$ that are true in $(\N, 0, 1, +)$. It can be axiomatized by the axioms $x + 1 \ne 0$, $x + 1 = y + 1 \to x = y$, $x + 0 = x$, $x + (y + 1) = (x + y) + 1$, and the induction scheme for all formulas of this signature.

It does not have quantifier elimination in $\set{0, 1, +}$. It has quantifier elimination after adding $<$ and, for each $n \ge 2$, a unary predicate $D_n(x)$ for "$n$ divides $x$". Check on one formula: in $\N$, the formula $\exists y \, (x = y + y)$ says that $x$ is even. It is equivalent to the quantifier-free formula $D_2(x)$. It is not equivalent to any quantifier-free formula in $\set{0, 1, +}$, since those define finite or cofinite subsets of $\N$. The set of even numbers is neither finite nor cofinite.