Presburger arithmetic

Presburger arithmetic is a weakened form of arithmetic which includes the structure $\mathbb{N}$, the constant $0$, the unary function $S$, the binary function $+$, and the binary relation . Essentially, it is Peano arithmetic without multiplication.

The axioms are:

1. $0\ne Sx$

2. $Sx=Sy\to x=y$

3. $x+0=x$

4. $x+Sy=S(x+y)$

5. For each first order formula $P(x)$, $P(0)\wedge \forall x[P(x)\to P(x+1)]\to \forall xP(x)$

Presburger arithmetic is decidable, but is consequently very limited in what it can express.