Quantifier elimination — Presburger arithmetic

The elementary theory of addition in the natural numbers admits a certain logical reducibility—every assertion is equivalent to a finite combination of atomic facts about identity and congruency.

We continue our investigation of quantifier elimination. Recall that a theory admits quantifier-elimination when every assertion is logically equivalent over the theory to a quantifier-free assertion, a Boolean combination of atomic assertions. This is quite a remarkable property when it occurs, revealing a severe limitation on expressive power and definability, and we are generally able to establish quantifier-elimination only when we have a profound mastery over the the theory and its models.

In an earlier post we showed that the theory of endless dense linear orders admits elimination of quantifiers, and then in a follow-up post, we showed the same for the theory of the successor operation.

Here, we shall consider the theory of addition in the natural numbers.

Enjoy this installment from A Panorama of Logic, an introduction to topics in logic for philosophers, mathematicians, and computer scientists. Fresh content each week.

Please consider subscribing as a free or paid subscriber.

Presburger arithmetic

Presburger arithmetic is the theory of addition on the natural numbers, that is, the theory of the structure ⟨ℕ,+,0,1⟩. The numbers 0 and 1 are actually definable here from addition alone, since 0 is the unique additive identity, and 1 is the only number u that is not expressible as a sum x + y with both x ≠ u and y ≠ u. So we may view this model if desired as a definitional expansion of ⟨ℕ,+⟩, with addition only. The number 2 is similarly definable as 1 + 1, and indeed any number n is definable as 1 + ··· + 1, with n summands, and so this is a pointwise definable model and hence also Leibnizian.

Definable sets

The theory can define the order, since x ⩽ y ⇔ ∃z (x + z = y). And it knows that addition is commutative x + y = y + x and order-preserving and so forth. The induction principle also is valid here.

What are the definable subsets? We can define the even numbers, of course, since x is even if and only if ∃y (y + y = x). We can similarly define congruence modulo 2 by

\(x ≡_2 y ↔ ∃z \bigl[(z + z + x = y) ∨ (z + z + y = x)\bigr].\)

More generally, we can express the relation of congruence modulo n for any fixed n as follows:

\( x ≡_n y\quad\text{ if and only if }∃z \bigl[(\overbrace{z + ··· + z}^n + x = y) ∨ (\overbrace{z + ··· + z}^n + y = x)\bigr]. \)

What I claim is that this exhausts what is expressible.

Elimination of quantifiers

Namely, every assertion in the theory of natural-number addition amounts to a Boolean combination of atomic congruency assertions.

Theorem. Presburger arithmetic admits elimination of quantifiers in the definitional expansion with all the modular congruence relations.

\( ⟨ℕ,+,0,1, ≡_2, ≡_3, ≡_4,...⟩ \)

In particular, every assertion in the language of ⟨ℕ,+,0,1⟩ is equivalent to a quantifer-free assertion in the language with the congruence relations.

Professor Mojżesz Presburger (1904-1943), as I would like to imagine him living to old age in a better world

Let us prove it and draw several further conclusions as a consequence.