Presburger Arithmetic - Overview

Overview

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:

1. ¬(0 = x + 1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. x + (y + 1) = (x + y) + 1
5. Let P(x) be a first-order formula in the language of Presburger arithmetic with a free variable x (and possibly other free variables). Then the following formula is an axiom:

(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y).

(5) is an axiom schema of induction, representing infinitely many axioms. Since the axioms in the schema in (5) cannot be replaced by any finite number of axioms, Presburger arithmetic is not finitely axiomatizable.

Presburger arithmetic cannot formalize concepts such as divisibility or prime number. Generally, any number concept leading to multiplication cannot be defined in Presburger arithmetic, since that leads to incompleteness and undecidability. However, it can formulate individual instances of divisibility; for example, it proves "for all x, there exists y : (y + y = x) ∨ (y + y + 1 = x)". This states that every number is either even or odd.