# 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. 1.

$0\not=Sx$

2. 2.

$Sx=Sy\rightarrow x=y$

3. 3.

$x+0=x$

4. 4.

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

5. 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.

Title Presburger arithmetic PresburgerArithmetic 2013-03-22 12:51:11 2013-03-22 12:51:11 Henry (455) Henry (455) 8 Henry (455) Definition msc 03B10 PeanoArithmetic