Presburger arithmetic

The Presburger arithmetic is in the first order predicate logic formulated mathematical theory of natural numbers with addition . It is named after Mojżesz Presburger , who introduced it in 1929. The signature of the Presburger arithmetic only contains addition, but not multiplication. The axiom system also includes an axiom scheme of complete induction .

Presburger arithmetic is considerably weaker than Peano arithmetic , in which both addition and multiplication are formalized. In contrast to Peano arithmetic, Presburger arithmetic is a decidable theory; H. For every statement formulated in the language of Presburger arithmetic, one can effectively decide whether it can be proven from the axioms of the theory or not. However, according to a study by Fischer and Rabin, the asymptotic running time of a corresponding algorithm is doubly exponential.

definition

The language of Presburger arithmetic contains constants 0 and 1 as well as a binary operation +, which is to be interpreted as addition. In this language the axioms of Presburger arithmetic are as follows:

${\ displaystyle 0 + 1 = 1}$
${\ displaystyle \ forall x \ colon \ neg (x + 1 = 0)}$
${\ displaystyle \ forall x, y \ colon (x + 1 = y + 1 \ rightarrow x = y)}$
${\ displaystyle \ forall x \ colon x + 0 = x}$
${\ displaystyle \ forall x, y \ colon (x + y) + 1 = x + (y + 1)}$
Be a formula in the language of Presburger arithmetic with free variables . Then the following statement is an axiom: ${\ displaystyle P (x, y_ {1}, \ ldots, y_ {k})}$ ${\ displaystyle x, y_ {1}, \ ldots, y_ {k}}$

{\ displaystyle \ forall y_ {1}, \ ldots, y_ {k} \ colon ((P (0, y_ {1}, \ ldots, y_ {k}) \ land \ forall x \ colon (P (x, y_ {1}, \ ldots, y_ {k}) \ rightarrow P (x + 1, y_ {1}, \ ldots, y_ {k}))) \ rightarrow \ forall x \ colon P (x, y_ {1 }, \ ldots, y_ {k}))}

The latter is an axiom scheme of complete induction and stands for an infinite number of individual axioms. These axioms corresponding to scheme (6) cannot be replaced by a finite number of axioms, so that Presburger arithmetic as a whole cannot be axiomatized finitely.

description

Presburger arithmetic can not formalize concepts such as divisibility or prime numbers , let alone multiplication, because then Presburger arithmetic like Peano arithmetic would have to be incomplete and undecidable. Individual instances of divisibility can, however, be formalized, for example “ is straight through” ; hereby expressible true statements like ${\ displaystyle x}$ ${\ displaystyle G (x): \ Leftrightarrow \ exists z \ colon z + z = x}$

{\ displaystyle \ forall x, y \ colon (G (x) \ land G (y) \ rightarrow G (x + y))}

("The sum of two even numbers is even")

are then provable sentences.

properties

Mojżesz Presburger demonstrated the following properties of his arithmetic:

Consistency : There is no statement formulated in their language for which both and can be derived from the axioms. ${\ displaystyle P}$ ${\ displaystyle P}$ ${\ displaystyle \ neg P}$
Completeness : For every statement formulated in the language of Presburger arithmetic, either the negative or the negative can be derived from the axioms. ${\ displaystyle P}$ ${\ displaystyle P}$ ${\ displaystyle \ neg P}$
Decidability : There is an algorithm that can decide for any given statement in Presburger arithmetic whether it is true or false.

The decidability of Presburger arithmetic can be demonstrated by eliminating quantifiers and considering arithmetic congruences .

The Peano arithmetic, i.e. Presburger arithmetic plus multiplication, on the other hand, cannot be decided. According to Gödel's incompleteness theorem , it is also incomplete and its consistency cannot be proven (internally).

The decision problem for Presburger arithmetic is an interesting example of complexity theory . Let be the length of a statement in Presburger arithmetic. Then, according to a work by Fischer and Rabin, the decision algorithm for the Presburger arithmetic has at least double-exponential running time, i.e. H. in the worst case, the running time is at least for a certain positive constant . On the other hand, there is a triple exponential upper estimate for the running time. It is therefore a question of a decision problem that demonstrably cannot be solved in exponential (let alone polynomial) time. Fischer and Rabin also showed that for every reasonable axiomatization (in a more precise sense) there exist sentences of any length, the shortest proof of which is of double-exponential length. Intuitively, this means that there are practical limits to computer evidence. The work of Fischer and Rabin also shows that Presburger arithmetic can be used to define formulas that correctly simulate any algorithm, as long as the inputs do not exceed certain - relatively high - limits. These limits can be increased by switching to other formulas. ${\ displaystyle n}$ ${\ displaystyle 2 ^ {2 ^ {cn}}}$ ${\ displaystyle c}$

Applications

There are actually computer evidence systems that use algorithms to decide formulas in Presburger arithmetic. For example, Coq contains evidence tactics along these lines. The double-exponential complexity limits the practical applicability for complicated formulas, but this behavior only occurs with nested quantifiers : Oppen and Nelson describe an automatic proof system based on the simplex method for an extended Presburger arithmetic without nested quantifiers. The worst-case runtime of the simplex method is (simply) exponential. In fact, exponential running time is only observed for specially constructed cases, while it works considerably more efficiently in everyday cases. This makes this approach suitable for practical use.

The Presburger arithmetic can be extended by the multiplication with constants, since this is a repeated addition. In programming technology, this applies to the calculation of field indices, for example. This approach is the basis of at least five systems for proving the correctness of computer programs, from the Stanford Pascal Verifier from the late 1970s to Microsoft's Spec # from 2005.

literature

David C. Cooper: Theorem Proving in Arithmetic without Multiplication . In: Bernhard Meltzer, Donald Michie (Ed.): Machine Intelligence . tape 7 . Edinburgh University Press, Edinburgh 1972, ISBN 978-0-470-60110-5 , pp. 91-99 .
Jeanne Ferrante, Charles W. Rackoff: The Computational Complexity of Logical Theories (= Lecture Notes in Mathematics . No. 718 ). Springer-Verlag, 1979, ISBN 3-540-09501-2 , doi : 10.1007 / BFb0062837 .
William Pugh: The Omega test . a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM / IEEE conference on Supercomputing . 1991, ISBN 0-89791-459-7 , doi : 10.1145 / 125826.125848 .
Cattamanchi Ramalinga Reddy, Donald W. Loveland: Presburger Arithmetic with Bounded Quantifier Alternation . In: ACM Symposium on Theory of Computing . 1978, p. 320-325 , doi : 10.1145 / 800133.804361 .
Paul Young: Gödel theorems, exponential difficulty and undecidability of arithmetic theories. In exposure . In: Anil Nerode, Richard A. Shore (Ed.): Recursion Theory (= Proceedings of symposia in pure mathematics ). tape 42 . American Mathematical Society, 1985, ISBN 0-8218-1447-8 , pp. 503-522 .

Web links

Philipp Rümmer: Princess , a computer evidence system for Presburger arithmetic (English).

Individual evidence

↑ ^a ^b Mojżesz Presburger: About the completeness of a certain system of arithmetic of integers in which addition appears as the only operation . In: Comptes Rendus du I congrès de Mathématiciens des Pays Slaves . Warsaw 1929, p. 92-101 .

^ ^A ^b Michael J. Fischer, Michael O. Rabin: Super-Exponential Complexity of Presburger Arithmetic . In: Proceedings of the SIAM-AMS Symposium in Applied Mathematics . tape 7 , 1974, p. 27–41 ( mit.edu [ PostScript ; accessed February 26, 2012]). Super-Exponential Complexity of Presburger Arithmetic ( Memento of the original from September 15, 2006 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice. @1@ 2
^ Herbert B. Enderton: A mathematical introduction to logic . 2nd Edition. Academic Press, Boston 2001, ISBN 0-12-238452-0 , pp. 188 .
^ Derek C. Oppen: A 2 ^{2 ^{2 ^pn}} Upper Bound on the Complexity of Presburger Arithmetic . In: J. Comput. Syst. Sci. tape 16 , no. 3 , 1978, p. 323-332 , doi : 10.1016 / 0022-0000 (78) 90021-1 .
^ Greg Nelson, Derek C. Oppen: A simplifier based on efficient decision algorithms . In: Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages . April 1978, p. 141-150 , doi : 10.1145 / 512760.512775 .

[Presburger-1] Mojżesz Presburger: About the completeness of a certain system of arithmetic of integers in which addition appears as the only operation . In: Comptes Rendus du I congrès de Mathématiciens des Pays Slaves . Warsaw 1929, p. 92-101 .