show/hide this revision's text 2 added 511 characters in body

Presburger arithmetic admits elimination of quantifiers, if one expands the language to include truncated minus and the unary relations for divisibility-by-2, divisibility-by-3 and so on, which are definable in Presburger arithmetic. (One can equivalently expand the language to include congruence $\equiv_k$ modulo $k$ for each natural number $k$.) That is to say, every assertion in the language of Presburger arithmetic is equivalent to a quantifier-free assertion in this the expanded language.

Since

It follows that the quantier-free assertions definable subsets of $\mathbb{N}$ in this the language of Presburger arithmetic are exactly the eventually periodic sets. These are comparatively trivial sets, this of course, and it means that the set of prime numbers and other interesting sets of natural numbers are simply not expressible in the language of Presburger arithmeticis comparatively weak. IndeedA similar analysis holds in higher dimensions, and for this is essentially why reason, we usually think of Presburger arithmetic as a weak theory.

The quantifier elimination argument leads directly to the conclusion that Presburger arithmetic is a decidable theory. Given : given any sentence, one finds the quantifier-free equivalent formulation, and such sentences are easily recognized as true or false.

There is an interesting account in these slides for a talk by Cesare Tinelli.

show/hide this revision's text 1

Presburger arithmetic admits elimination of quantifiers, if one expands the language to include the unary relations for divisibility-by-2, divisibility-by-3 and so on, which are definable in Presburger arithmetic. That is to say, every assertion in the language of Presburger arithmetic is equivalent to a quantifier-free assertion in this expanded language.

Since the quantier-free assertions in this language are comparatively trivial, this means that Presburger arithmetic is comparatively weak. Indeed, this is essentially why Presburger arithmetic is a decidable theory. Given any sentence, one finds the quantifier-free equivalent formulation, and such sentences are easily recognized as true or false.

There is an interesting account in these slides for a talk by Cesare Tinelli.