Presburger arithmetic

The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.

In this language, the axioms of Presburger arithmetic are the universal closures of the following:

Some properties are now given about integer relations definable in Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers.