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—weak enough, in fact, that Gödel’s Incompleteness Theorems don’t apply to it. While it can’t 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.
The axioms of Presburger arithmetic are essentially a subset of the Peano axioms, 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—for example, “less than” is a definable relation in Presburger arithmetic. It is also permissible to define constant multiplication for a given integer—that is, we are allowed to define the operation 3 * x because it is essentially shorthand for adding the term x to itself a specified number of times. However, we may not define x * y, because both terms are variables and this introduces a problematic ambiguity.
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ödel’s 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—since you can find a finite decision algorithm for any proposition, you can program a computer to prove or disprove theorems 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—Princess 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’s a broad scope of applications for a model that can’t even define multiplication!
If you’re interested in reading more about Presburger arithmetic or its applications, Wikipedia has a great overview, and the official webpage for the Princess theorem prover provides a lot of documentation.
Referring to the issue of provability of consistency of the Arithmetic System (and Godel’s Second Incompleteness Theorem), I’d like to inform you about the paper: T. J. Stępień, Ł. T. Stępień, „On the Consistency of the Arithmetic System”, Journal of Mathematics and System Science, vol. 7, 43 (2017), arXiv:1803.11072 . In this paper a proof of the consistency of the Arithmetic System has been published, this proof has been done within this Arithmetic System.
Previously, in 2009, Dr Teodor J. Stepien and me delivered a talk at “Logic Colloquium 2009” in Sofia (Bulgaria). During this talk, a sketch of the proof of the consistency of the Arithmetic System was presented.
The abstract of this talk was published in The Bulletin of Symbolic Logic: T. J. Stepien and L. T. Stepien, “On the consistency of Peano’s Arithmetic System” , Bull. Symb. Logic 16, No. 1, 132 (2010), http://www.math.ucla.edu/~asl/bsl/1601-toc.htm .