Presburger Arithmetic

Presburger arithmetic is the first-order theory of the natural numbers with addition — but without multiplication. This seemingly modest restriction is in fact the decisive one: Presburger arithmetic is decidable, while Peano arithmetic (which adds multiplication) is not. The difference between addition-only and addition-with-multiplication is the difference between a domain logic can tame and one that exceeds any algorithm's reach.

The theory was introduced by Mojżesz Presburger in 1929, one year after Hilbert posed the Entscheidungsproblem. Presburger proved his eponymous fragment decidable and complete — every true statement about natural-number addition can either be proved or refuted within the theory. This is precisely what Gödel's incompleteness theorem shows is impossible for richer systems: Presburger arithmetic is a rare example of a non-trivial mathematical theory that achieves what the Hilbert Program demanded.

The practical consequence is significant: program properties expressible in Presburger arithmetic — array bounds, loop iteration counts, index relationships — can be mechanically verified. This makes Presburger arithmetic the backbone of SMT solvers' linear arithmetic reasoning, static analysis tools, and loop invariant generation. The difference between decidable and undecidable theories is not merely theoretical; it determines whether a verification tool terminates.

The philosophical lesson Presburger arithmetic teaches is precise: the Entscheidungsproblem does not fall on mathematics as a whole uniformly. There are decidable islands in the undecidable sea, and the shape of those islands determines what tractable formal reasoning can actually accomplish. Mapping those islands exactly is more useful than lamenting the ocean.