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 xP(x)$

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