Presburger arithmetic

Presburger arithmetic is a weak arithmetic theory. It is consistent, complete, and decidable, but is not strong enough to form statements about multiplication. The decision problem of determining whether a given statement is a theorem of Presburger arithmetic is in a doubly exponential complexity class.
== Definition ==
The language of Presburger arithmetic extends predicate calculus with a constant 0, unary operator S, binary operator +, and relation =. Its axioms are:
* \(\forall n: S(n) \neq 0\)
* \(\forall n \forall m: S(n) = S(m) \Rightarrow n = m\)
* \(\forall n: n + 0 = n\)
* \(\forall n \forall m: n + S(m) = S(n + m)\)
* For every first-order formula \(\varphi(n)\): \((\varphi(0) \wedge (\forall n: \varphi(n) \Rightarrow \varphi(S(n)))) \Rightarrow \forall m: \varphi(m)\).
== Properties ==
As mentioned before, Presburger arithmetic is weak enough that it is not very useful as a general foundation for number theory. The fundamental theorem of arithmetic, for example, is arguably one of the most important results of number theory, but it is not expressible in the language of Presburger arithmetic.
The interest in the theory is that it is both consistent and complete. This does not violate , which only applies to theories with languages that can make statements about elementary arithmetic.
Presburger arithmetic is also decidable. Unlike its older siblings such as and Peano arithmetic, there is an algorithm that determines whether a given statement is a theorem. Fischer and Rabin showed that the decision problem is in a doubly exponential complexity class; that is, there is a positive constant c such that for every non-deterministic procedure that decides the problem, for all sufficiently large n the procedure takes more than \(2^{2^{cn}}\) steps.http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps
== Sources ==
== See also ==
Category:Arithmetic