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\not= Sx$
2. $Sx=Sy\rightarrow 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)\rightarrow P(x+1)]\rightarrow\forall x P(x)$

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