What good is arithmetic without multiplication? Pretty great, actually! Presburger arithmetic, formally defined as the theory of the natural numbers with addition, is a particularly interesting model of arithmetic. Because it does not formalize multiplication, Presburger arithmetic is relatively weak in terms of what it can express\u2014weak enough, in fact, that G\u00f6del\u2019s Incompleteness Theorems don\u2019t apply to it. While it can\u2019t define prime numbers or division by variables, it is complete and decidable. This means it is possible to check any sentence to determine whether or not it is true in the model, i.e. whether it is a theorem or nontheorem of Presburger arithmetic.<\/p>\n
The axioms of Presburger arithmetic are essentially a subset of the Peano axioms<\/a>, excluding those pertaining to multiplication. For our purposes, it suffices to know that Presburger arithmetic deals with the nonnegative integers with standard definitions for equality, succession, and addition. Most of the usual properties of integer arithmetic can be built up from those definitions\u2014for example, \u201cless than\u201d is a definable relation in Presburger arithmetic. It is also permissible to define constant multiplication for a given integer\u2014that is, we are allowed to define the operation 3 * x<\/em> because it is essentially shorthand for adding the term x<\/em> to itself a specified number of times. However, we may not define x<\/em> * y<\/em>, because both terms are variables and this introduces a problematic ambiguity.<\/p>\n Now that we know what the ground rules are, what makes Presburger arithmetic interesting? Compared to other models of arithmetic, it may seem restrictive and boring, but its restrictiveness is precisely what makes it important. G\u00f6del\u2019s Incompleteness Theorems, which assert the existence of undecidable propositions, only apply to formal theories of a certain strength. By excluding generalized multiplication, Presburger arithmetic remains insufficiently strong for the Incompleteness Theorems to apply, and hence all its propositions are decidable. This makes Presburger arithmetic especially appealing for automated theorem proving\u2014since you can find a finite decision algorithm for any proposition, you can program a computer to prove or disprove\u00a0theorems in the language. The Coq proof assistant and the theorem prover Princess are both examples of automated theorem provers that base some or all of their functionality on Presburger arithmetic. These theorem provers can have applications beyond model theory\u2014Princess has been used by such programs as Seneschal, a ranking function generator for bitvector relations, and Joogie, which detects infeasible code in the Java programming language. That\u2019s a broad scope of applications for a model that can\u2019t even define multiplication!<\/p>\n If you\u2019re interested in reading more about Presburger arithmetic or its applications, Wikipedia<\/a> has a great overview, and the official webpage for the Princess theorem prover<\/a> provides a lot of documentation.<\/p>\n