Definition of Presburger Arithmetic
Minimalistic Language of Presburger Arithmetic
Consider and consider as
the set of all interpretations with domain
where
is interpreted as addition of natural numbers (these interpretations differ only in values for free variables. This is one definition of Presburger arithmetic over natural numbers.
This theory is very simple to describe, but it is very far from allowing quantifier-elimination. For example, it does not have a name for zero, so we cannot express . It also does not have a way to express
.
Language of Presburger Arithmetic that Admits QE
We look at the theory of integers with addition.
- introduce constant for each integer constant
- introduce not only addition but also subtraction
- to conveniently express certain expressions, introduce function
for each
, to be interpreted as multiplication by a constant,
. We write
as
- to enable quantifier elimination from
introduce for each
predicate
(divisibility by constant)
The resulting language