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.
Title  Presburger arithmetic 

Canonical name  PresburgerArithmetic 
Date of creation  20130322 12:51:11 
Last modified on  20130322 12:51:11 
Owner  Henry (455) 
Last modified by  Henry (455) 
Numerical id  8 
Author  Henry (455) 
Entry type  Definition 
Classification  msc 03B10 
Related topic  PeanoArithmetic 