Presburger arithmetic is the first-order theory of the natural numbers with addition. It is not as powerful as Peano arithmetic because multiplication is omitted. In fact, Mojżesz Presburger proved in 1929 that Presburger arithmetic is decidable. In other words, there is an algorithm which decides for any given statement in Presburger arithmetic whether it is provable or not. No such algorithm exists for general arithmetic as a consequence of the negative answer to the Entscheidungsproblem. Furthermore, Presburger proved that his arithmetic is consistent (does not contain contradictions) and complete (every statement can either be proven or disproven). Again, such a proof cannot be given for general arithmetic; in fact, it follows from Gödel's incompleteness theorem that (any recursive axiomatization of) general arithmetic cannot be both consistent and complete. First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... In mathematics, a natural number is either a positive integer (1, 2, 3, 4, ...) or a non-negative integer (0, 1, 2, 3, 4, ...). The former definition is generally used in number theory, while the latter is preferred in set theory and computer science. ... 3 + 2 with apples, a popular choice in textbooks Addition is the basic operation of arithmetic. ... In mathematics, the Peano axioms (or Peano postulates) are a set of first-order axioms proposed by Giuseppe Peano which determine the theory of Peano arithmetic (also known as first-order arithmetic). ... In mathematics, multiplication is an arithmetic operation which is the inverse of division, and in elementary arithmetic, can be interpreted as repeated addition. ... Mojżesz Presburger (1904 - 1943) was a Polish mathematician, logician, and philosopher. ... 1929 (MCMXXIX) was a common year starting on Tuesday (link will take you to calendar). ... The word decidable has formal meaning in computability theory, the theory of formal languages, and mathematical logic. ... Flowcharts are often used to represent algorithms. ... Arithmetic is the current mathematics collaboration of the week! Please help improve it to featured article standard. ... The Entscheidungsproblem (English: decision problem) is the challenge in symbolic logic to find a general algorithm which decides for given first-order statements whether they are universally valid or not. ... In mathematical logic, Gödels incompleteness theorems are two celebrated theorems proven by Kurt Gödel in 1931. ...

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). Quantifier elimination is a technique in logic, model theory, and theoretical computer science. ...

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 worst-case runtime of at least 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 (indeed, even more than exponential time!). In computer science, computational complexity theory is the branch of the theory of computation that studies the resources, or cost, of the computation required to solve a given problem. ... To meet Wikipedias quality standards, this article or section may require cleanup. ... Michael Oser Rabin (born 1931 in Breslau, Germany, today in Poland) is a noted computer scientist and a recipient of the Turing Award, the most prestigious award in the field. ... 1974 (MCMLXXIV) was a common year starting on Tuesday (the link is to a full 1974 calendar). ...

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:

1. ∀ x : ¬ (0 = x + 1)
2. ∀ x ∀ y : ¬ (x = y) ⇒ ¬ (x + 1 = y + 1)
3. ∀ x : x + 0 = x
4. ∀ x ∀ y : (x + y) + 1 = x + (y + 1)
5. 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)

Concepts such as divisibility or prime number cannot be formalized in Presburger arithmetic. Here is a typical theorem that can be proven from the above axioms:

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

It says that if x ≤ y + 1, then y + 2 > x.

Applications

Because Presburger arithmetic is decidable, a decision procedure can be constructed for it. Thus, an automatic theorem prover which will reliably produce a correct result for such problems is possible. The word decidable has formal meaning in computability theory, the theory of formal languages, and mathematical logic. ... In logic, a decision problem is determining whether or not there exists a decision procedure or algorithm for a class S of questions requiring a Boolean value (i. ... Automated theorem proving (currently the most important subfield of automated reasoning) is the proving of mathematical theorems by a computer program. ...

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. In mathematical optimization theory, the simplex algorithm of George Dantzig is a popular technique for numerical solution of the linear programming problem. ...

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. In mathematical optimization theory, the simplex algorithm of George Dantzig is a popular technique for numerical solution of the linear programming problem. ...

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. In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. ... A computer program (often simply called a program) is an example of computer software that prescribes the actions (computations) that are to be carried out by a computer. ... Spec♯ is a programming language that extends the capabilities of the C# programming language with object invariants, including preconditions and post-conditions. ...

References

• 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 (Postscript)
• C. R. Reddy and D. W. Loveland: "Presburger Arithmetic with Bounded Quantifier Alternation". ACM Symposium on Theory of Computing,, 1978, pp.320-325 (from ACM)
• Jeanne Ferrante and Charles W. Rackoff: "The Computational Complexity of Logical Theories". Lecture Notes in Mathematics 718. Springer. 1979.
• D. C. Cooper: "Theorem Proving in Arithmetic without Multiplication". In B. Meltzer and D. Michie (eds.): Machine Intelligence,, Edinburgh University Press, 1972. pp.91-100
• William Pugh: "The Omega test: a fast and practical integer programming algorithm for dependence analysis", 1991. (from ACM)
• 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.