Presburger arithmetic

From Wikipedia, the free encyclopedia

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.

Contents

[edit] Overview

The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition. In this language, the axioms of Presburger arithmetic are as follows (all free variables should be taken as tacitly universally quantified):

  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 in the language of Presburger arithmetic with a free variable x (and possibly other free variables). Then the following formula is an axiom:
(P(0) ∧ ∀x(P(x) → P(x + 1))) → P(y).

(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. Generally, any number concept leading to multiplication cannot be defined in Presburger arithmetic since that leads to incompleteness and undecidability. However, it can formulate individual instances of divisibility; for example, it proves "for all x, there exists y : y + y = x ∨ y + y + 1 = x". This states that every number is either even or odd.

[edit] Properties

Mojżesz Presburger proved Presburger arithmetic to be:

  • consistent: There is no statement in Presburger arithmetic which can be deduced from the axioms such that its negation can also be deduced.
  • complete: For each statement in Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation.
  • 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.[1]

Peano arithmetic, which is Presburger arithmetic augmented with multiplication, cannot be decidable as a consequence of the negative answer to the Entscheidungsproblem. By Gödel's incompleteness theorem, Peano arithmetic is either incomplete and its consistency is not internally provable, or Peano arithemetic is inconsistent, in which case all sentences are provable.

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 exponential run time. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of length n which have doubly exponential length proofs. Intuitively, this means there are computational limits on what can be proven by computer programs. Fischer and Rabin's work also implies that Presburger arithmetic can be used to define formulas which correctly calculate any algorithm as long as the inputs are less than relatively large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for Presburger Arithmetic was proved by Oppen (1978).

[edit] 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. The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but it only occurs in the presence of nested quantifiers: 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 array 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.

[edit] See also

[edit] References

[edit] Inline references

  1. ^ Enderton, A Mathematical Introduction to Logic, p. 188

[edit] External links

  • online prover A Java applet proves or disproves arbitrary formulas of Presburger arithmetic (In German)