Presburgerarithmetic

Presburger arithmetic is the first-order theory of the natural numbers with addition, the order relation, and the constant symbols 0 and 1. In this theory multiplication of two variables is not available in the language, though multiplication by a fixed constant can be expressed by repeated addition. The standard language is often described as {0, 1, +, <} and may include the successor function S(x) = x + 1.

The theory is decidable and, in fact, admits quantifier elimination. This means that every first-order formula is equivalent to a quantifier-free formula, and such formulas express linear arithmetic: linear equalities and inequalities, as well as congruence relations modulo fixed integers, all definable using addition and order. Consequently Presburger arithmetic can express basic arithmetical properties such as divisibility, parity, and residue classes.

Historically, the theory is named after Mojżesz Presburger, who published a decision procedure in 1929 for the theory of natural numbers with addition. His result established that the additive structure of the integers is complete and decidable, in stark contrast to theories that include multiplication.

Context and extensions: Presburger arithmetic serves as a foundational framework for reasoning about linear integer constraints and has influenced areas such as automated theorem proving and formal verification. It is decidable, but not expressive enough to capture multiplication of variables; once multiplication is added to the language, the theory becomes equivalent to Peano arithmetic, which is known to be undecidable.