Presburger Arithmetic

Origin. Mojżesz Presburger, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt", presented at the First Congress of Mathematicians of Slavic Countries (Warsaw 1929, published 1930), written as a student exercise set by Tarski. Fischer and Rabin (1974) proved the doubly exponential lower bound that made the decision procedure a landmark in complexity rather than only in logic.

Models. Arithmetic with addition and without multiplication. The result is everything PA is not: complete, decidable, and admitting quantifier elimination — which locates incompleteness precisely. It is not number, not induction, not the infinite domain that defeats decision procedures; it is multiplication. Presburger arithmetic is the control case against which Gödel's theorem is read.

Formalism.

Language: 0, 1, +, <, = (over ℕ or ℤ; the two variants are mutually interpretable)

Axioms: P1. ¬(0 = x + 1) P2. x + 1 = y + 1 → x = y P3. x + 0 = x P4. (x + y) + 1 = x + (y + 1) P5. Induction: φ(0) ∧ ∀x(φ(x) → φ(x+1)) → ∀x φ(x), for each φ in the language of P

The induction schema is over the addition-only language. That restriction is the whole content: the schema is as strong as PA's, and the theory is still decidable.

Quantifier elimination: Not available in the bare language. The language must be expanded by the divisibility predicates x ≡ₙ y ("n divides x − y"), one for each n ≥ 2, after which every formula is equivalent to a Boolean combination of linear inequalities and congruences. Cooper's algorithm (1972) and the Omega test are the implementations.

Definable sets: exactly the semilinear sets — finite unions of linear sets {b + Σ λᵢaᵢ : λᵢ ∈ ℕ}. Equivalently (Büchi), the sets recognizable by a finite automaton reading base-k representations, uniformly in k (Cobham–Semenov gives the converse).

Complexity: Fischer–Rabin (1974): every decision procedure requires 2^(2^cn) nondeterministic time on infinitely many inputs. Berman (1980): the theory is complete for STA(∗, 2^(2^O(n)), n) — doubly exponential alternating time with a linear number of alternations. Oppen (1978): triply exponential upper bound for the Cooper procedure. The existential fragment is integer linear programming: NP-complete.

What destroys decidability: Adding × gives PA — undecidable. Adding the graph of × on any infinite definable set, likewise. Adding a free unary predicate: Π¹₁-complete. Adding the map x ↦ 2ˣ: undecidable in general, though ⟨ℕ, +, 2^ℕ⟩ (addition with the set of powers of 2) stays decidable (Semenov).

Symbols.

Metatheory. Complete: every sentence or its negation is provable. Decidable, by quantifier elimination after adding the congruence predicates — and the need for those predicates is not an artifact but a fact about definability, since ≡₂ is definable in P yet not quantifier-free definable in the bare language. Consistency is provable in PRA, indeed in EFA. There is no interpretation of Q in P, so the Tarski–Mostowski–Robinson method has nothing to work with; the two theories sit on opposite sides of the incompleteness boundary and Skolem arithmetic sits beside P on the decidable side. Decidability is not cheapness: the doubly exponential lower bound is unconditional, and Presburger is the standard example of a theory that is decidable and infeasible at once.

Applies to. Compiler dependence analysis and loop optimization (the Omega test). SMT solving — the linear integer arithmetic theory of SMT-LIB. Model checking of counter systems and array bounds. Automata theory, through the Büchi correspondence with base-k recognizability. Verification of pointer and length constraints. Any decision problem reducible to linear constraints over ℤ.

Limitations. No multiplication of variables, so nothing about primes, factorization, or Diophantine equations is expressible — the theory is decidable because it is blind to exactly what number theory is about. Doubly exponential lower bound rules out general-purpose use; solvers depend on fragments being easier than the worst case. The QE procedure blows up formulas badly. The theory is not finitely axiomatizable, and the induction schema is essential — dropping it gives an incomplete theory of ordered abelian groups.

© 2026 Lingenic LLC