Presburger arithmetic

Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely. The axioms include a schema of induction.

Presburger arithmetic is much weaker than Peano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a decidable theory. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-time computational complexity of this decision problem is doubly exponential, however, as shown by Fischer & Rabin (1974).

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 the universal closures of the following:

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))) → ∀y P(y).

(5) is an axiom schema of induction, representing infinitely many axioms. Since the axioms in the schema in (5) cannot be replaced by any finite number of axioms, Presburger arithmetic is not finitely axiomatizable in first-order logic.

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.

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 the language of 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 a theorem or a nontheorem.

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

Peano arithmetic, which is Presburger arithmetic augmented with multiplication, is not decidable, as a consequence of the negative answer to the Entscheidungsproblem. By Gödel's incompleteness theorem, Peano arithmetic is incomplete and its consistency is not internally provable (but see Gentzen's consistency proof).

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 an 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). A more tight complexity bound was shown using alternating complexity classes by Berman (1980).

Applications

Because Presburger arithmetic is decidable, automatic theorem provers for Presburger arithmetic exist. For example, the Coq proof assistant system features the tactic omega for Presburger arithmetic and the Isabelle proof assistant contains a verified quantifier elimination procedure by Nipkow (2010). The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers: Oppen and Nelson (1980) describe an automatic theorem prover which uses the simplex algorithm on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recent Satisfiability Modulo Theories solvers use complete integer programming techniques to handle quantifier-free fragment of Presburger arithmetic theory (King, Barrett, Tinelli 2014).

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 through to Microsoft's Spec# system of 2005.

Presburger-definable integer relation

Some properties are now given about integer relation definable in Presburger Arithmetic. For the sake of simplicity, all considered relations are over natural integers.

A relation is Presburger-definable if and only if it is a semilinear set.

A unary integer relation $R$, that is, a set of integer, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a natural integer threshold $t\in \mathbb {N}$ and a positive period $p\in \mathbb {N} ^{>0}$ such that, for all integer $n$ such that $|n|\geq t$, $n\in R$ if and only if $n+p\in R$.

By the Cobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable in Büchi arithmetic of base $k$ for all $k\geq 2$. A relation definable in Büchi aritmetic of base $k$ and $k'$ for $k$ and $k'$ being multiplicatively independent integers is Presburger definable.

An integer relation $R$ is Presburger-definable if and only if all sets of integers which are definable in the first order logic with addition and $R$ (that is, Presburger Arithmetic plus a predicate for $R$) are Presburger-definable. Equivalently, for each relation $R$ which is not Presburger-definable, there exists a first-order formula with addition and $R$ which defines a set of integer which is not definable using only addition.

Muchnik's characterization

Presburger-definable relations admits another characterization: Muchnik's theorem. This last characterization is more complicated to state, but led to the proof of the two last characterizations. In order to give the last characterization of this section, some preliminaries definitions must be introduced.

For $R\subseteq \mathbb {N} ^{d}$ a set, the section $x_{i}=j$, for $i<d$ and $j\in \mathbb {N}$ is defined as $\{(x_{0},\dots ,x_{i-1},x_{i+1},\dots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\dots ,x_{i-1},j,x_{i+1},\dots ,x_{d-1})\in R\}$.

Given two sets $R,S\subseteq \mathbb {N} ^{d}$ and a $d$-tuple of integers $(p_{0},\dots ,p_{d-1})\in \mathbb {N} ^{d}$, the set $R$ is $(p_{0},\dots ,p_{d-1})$-periodic in $S$ if and only if, for all $(x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}$ such that $(x_{0},\dots ,x_{d-1})\in S$ and $(x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in S$, then $(x_{0},\dots ,x_{d-1})\in R$ if and only if $(x_{0}+p_{0},\dots ,x_{d-1}+p_{d-1})\in R$. For $s\in \mathbb {N}$, the set $R$ is said to be $n$-periodic in $S$ if it is $(p_{0},\dots ,p_{d-1})$-periodic and $\sum _{i=0}^{d-1}p_{i}<s$.

Finally, for $k,x_{0},\dots ,x_{d-1}\in \mathbb {N}$, let $C(k,(x_{0},\dots ,x_{d-1}))=\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1}\mid 0\leq c_{i}<k\}$. It is the cube of size $k$ whose lesser corner is $(x_{0},\dots ,x_{d-1})$.

A set $R\subseteq \mathbb {N} ^{d}$ is Presburger-definable if and only:

• if the dimension is greater than 1 then all sections of $R$ are Presburger-definable arithmetic and
• there exists $s\in \mathbb {N}$ such that, for every $k\in \mathbb {N}$ there exists $t\in \mathbb {N}$ such that for all $(x_{0},\dots ,x_{d-1})\in \mathbb {N} ^{d}$ with $\sum _{i=0}^{d-1}x_{i}>t$ then $R$ is $s$-periodic in $C(k,(x_{0},\dots ,x_{d-1}))$.

Intuitively, $s$ represents the length of a shift, $k$ is the size of the cubes and $t$ is the threshold before the periodicity. This results remains true when the condition $\sum _{i=0}^{d-1}x_{i}>t$ is replaced either by $\min(x_{0},\dots ,x_{d-1})>t$ or by $\max(x_{0},\dots ,x_{d-1})>t$.

See also

• Robinson arithmetic

References

• Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence Vol. 7. Edinburgh University Press: 91–99.
• Enderton, Herbert (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3.
• Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
• Fischer, Michael J.; Rabin, Michael O. (1974). "Super-Exponential Complexity of Presburger Arithmetic". Proceedings of the SIAM-AMS Symposium in Applied Mathematics. 7: 27–41. {{cite journal}}: Invalid |ref=harv (help)
• G. Nelson and D. C. Oppen (Apr 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141–150. doi:10.1145/512760.512775.
• 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. — see Stansifer (1984)for an English translation
• Ryan Stansifer (Sep 1984). Presburger's Article on Integer Arithmetic: Remarks and Translation (PDF) (Technical Report). Vol. TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University.
• William Pugh, 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.
• Young, P., 1985, "Gödel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition" in A. Nerode and R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Oppen, Derek C. (1978). "A 2^22pn Upper Bound on the Complexity of Presburger Arithmetic" (PDF). J. Comput. Syst. Sci. 16 (3): 323–332. doi:10.1016/0022-0000(78)90021-1.
• Berman, L. (1980). "The Complexity of Logical Theories". Theoretical Computer Science. 11 (1): 71–77. doi:10.1016/0304-3975(80)90037-7.
• Nipkow, T (2010). "Linear Quantifier Elimination". Journal of Automated Reasoning. 45 (2): 189–212. doi:10.1007/s10817-010-9183-0.
• King, Tim; Barrett, Clark W.; Tinelli, Cesare (2014). "Leveraging linear and mixed integer programming for SMT". FMCAD. 2014: 139–146. doi:10.1109/FMCAD.2014.6987606.

External links

• [1] A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer