Definition. Theory of Presburger Arithmetic [003h]

Presburger Arithmetic (PA) is a first order theory over the signature \(\Sigma _{\mathbb {N}}\) which contains:

Where \(0\) and \(1\) are constant symbols representing zero and one respectively, \(+\) is a binary function symbol representing addition, and \(=\) is a binary relation symbol representing equality. The axioms of Presburger Arithmetic are:

Some important properties of \(T_{\mathbb {N}} are\):

• Validity in quantifer-free Presburger Arithmetic is decidable.
• Validity in full Presburger Arithmetic is decidable.
• Validity in Presburger Arithmetic has a super exponential complexity \(O(2^{2^n})\)
• \(T_{\mathbb {N}}\) is complete, i.e. \[ \forall F.\ T_{\mathbb {N}} \models F \lor T_{\mathbb {N}} \models \neg F \]