Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who published it in 1929. It is not as powerful as Peano arithmetic because it omits multiplication.

Mojżesz Presburger proved Presburger arithmetic:

• Consistent. All provable statements in Pressburger arithmetic are true.
• Complete. All true statement in Presburger arithmetic are provable from the axioms.
• Decidable. There exists an algorithm which decides whether any given statement in Presburger arithmetic is true or false.

The decidability of Presburger arithmetic can be shown using quantifier elimination, supplemented by reasoning about arithmetical congruence (Enderton, A Mathematical Introduction to Logic, p.188).

Peano arithmetic, which is Presburger arithmetic augmented with multiplication, cannot be decidable as a consequence of the negative answer to the Entscheidungsproblem. Nor can it be both consistent and complete, because of Gödel's incompleteness theorem.

The decision problem for Presburger arithmetic is an interesting example in computational complexity theory and computation. Let n be the length of a statement in Presburger arithmetic. Then Fischer and Rabin (1974) proved that any decision algorithm for Presburger arithmetic has a worst-case runtime of at least $2^\{2^\{cn\}\}$, for some constant c>0. Hence, the decision problem for Presburger arithmetic is a rare example of a decision problem that has been proved to require more than polynomial or even exponential run time.

The following axioms invoke the object constants 0 and 1, the function constant +, and the predicate constant =. All free variables should be taken as tacitly universally quantified. The axioms are:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. (x + y) + 1 = x + (y + 1)
5. Let P(x) be a first order formula involving the constants 0, 1, +, = and a single free variable x. Then the following formula is an axiom:

(P(0) ∧ (P(x)→P(x + 1))) → P(x).

(5) is an axiom schema of induction, representing infinitely many axioms. (5) cannot be replaced by any finite number of axioms; hence Presburger arithmetic cannot be finitely axiomatized.

Presburger arithmetic cannot formalize concepts such as divisibility or prime number. An elementary result that cannot be proved in Presburger arithmetic is:

∀x∀y∃z+ z = y+1 ⇒ ∀z+ z = x)

This sentence states that if x≤y+1, then y+2>x.

Applications

---

Because Presburger arithmetic is decidable, a decision procedure exists for it. Thus, an automatic theorem prover for Presburger arithmetic is possible. Such theorem provers exist. Oppen and Nelson (1980) describes an automatic theorem prover which uses the simplex algorithm on an extended Presburger arithmetic without nested quantifiers. The simplex algorithm has exponential worst-case run time. But the average run time is far better. Exponential run time is only observed for specially constructed cases. This makes a simplex-based approach practical in a working system.

Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most subscript calculations then fall within the region of decidable problems. This approach is the basis of at least five proof of correctness systems for computer programs, beginning with the Stanford Pascal Verifier in the late 1970s and continuing though to Microsoft's Spec# system of 2005.

See also

---

• Peano arithmetic
• Robinson arithmetic
• first order logic

References

---

• Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91-100.
• Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
• Fischer, M. J., and Michael O. Rabin, 1974, ""Super-Exponential Complexity of Presburger Arithmetic." Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27-41.
• Mojżesz Presburger, 1929, "Ü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: 92-101.
• Pugh, William, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis,".
• Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320-325.

Mathematical logic

Arithmétique de Presburger