# 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

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

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.

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

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

## Keep reading with a 7-day free trial

Subscribe to Infinitely More to keep reading this post and get 7 days of free access to the full post archives.