Presburger arithmetic is an interesting example in computational complexity theory and computation because Fischer and Rabin proved in 1974 that every algorithm which decides the truth of Presburger statements has a runtime of at least 2^(2^(*cn*)) for some constant *c*. Here, *n* is the length of the Presburger statement. Hence, the problem is one of the few that provably need more than polynomial run time.

In the formal description of the theory, we use the object constants 0 and 1, the function constant +, and the predicate constant =. The axioms are:

- ∀
*x*: ¬ (0 =*x*+ 1) - ∀
*x*∀*y*: ¬ (*x*=*y*) ⇒ ¬ (*x*+ 1 =*y*+ 1) - ∀
*x*:*x*+ 0 =*x* - ∀
*x*∀*y*: (*x*+*y*) + 1 =*x*+ (*y*+ 1) - This is an axiom scheme consisting of infinitely many axioms. If
*P*(*x*) is any formula involving the constants 0, 1, +, = and a single free variable*x*, then the following formula is an axiom: (*P*(0) ∧ ∀*x*:*P*(*x*) ⇒*P*(*x*+ 1) ) ⇒ ∀*x*:*P*(*x*)

- ∀
*x*∀*y*: ( (∃*z*:*x*+*z*=*y*+ 1) ⇒ (∀*z*: ¬ (((1 +*y*) + 1) +*z*=*x*) ) )

- M. Presburger: "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". In
*Comptes Rendus du I congrès de Mathématiciens des Pays Slaves,*Warszawa, 1929, pp.92-101 - M.J. Fischer, M.O.Rabin: "Super-Exponential Complexity of Presburger Arithmetic".
*Proceedings of the SIAM-AMS Symposium in Applied Mathematics,*1974, vol. 7, pp.27-41