---
tag: B66JYY3K58
kind: example
name: Presburger arithmetic
msc: [03B25, 03C10, 11U09]
illustrates: [7FDDXV3JK7]
uses: [0MWKJ44V5A, 0C4JS9RF5M, 0WAY5WX8NY, 655K8Y7VS8, 0QFT7Z76N5]
sources:
  - url: https://en.wikipedia.org/wiki/Presburger_arithmetic
same_as:
  wikidata: Q956059
  wikipedia: Presburger arithmetic
---

## Example

*Presburger arithmetic* is the first-order theory of the [[natural numbers|0MWKJ44V5A]] with $0$, $1$ and addition.
It is the set of all sentences in the signature $\set{0, 1, +}$ that are true in $(\N, 0, 1, +)$.
It can be axiomatized by the axioms $x + 1 \ne 0$, $x + 1 = y + 1 \to x = y$, $x + 0 = x$, $x + (y + 1) = (x + y) + 1$, and the induction scheme for all formulas of this signature.

It does not have quantifier elimination in $\set{0, 1, +}$.
It has quantifier elimination after adding $<$ and, for each $n \ge 2$, a unary predicate $D_n(x)$ for "$n$ divides $x$".
Check on one formula: in $\N$, the formula $\exists y \, (x = y + y)$ says that $x$ is even.
It is equivalent to the quantifier-free formula $D_2(x)$.
It is not equivalent to any quantifier-free formula in $\set{0, 1, +}$, since those define finite or cofinite subsets of $\N$.
The set of even numbers is neither finite nor cofinite.

## Remarks

Quantifier elimination gives an algorithm that decides, for every sentence of the signature, whether it is true in $\N$.
So Presburger arithmetic is [[complete|655K8Y7VS8]] and decidable.
Mojżesz Presburger proved this in 1929.
In contrast, the theory of $(\N, 0, 1, +, \cdot)$ is undecidable, and the [[Peano axioms|0QFT7Z76N5]] do not decide all its sentences, by Gödel's incompleteness theorems.
Multiplication of two variables is therefore not definable from addition in $\N$.
The same method applies to the [[integers|0C4JS9RF5M]] with addition and order, where divisibility by $n$ is [[congruence modulo $n$|0WAY5WX8NY]] to $0$.

## Explanations

### L1 human

Presburger arithmetic is arithmetic of the natural numbers with addition but without multiplication.
Every statement in this language can be decided by a computer, unlike full arithmetic with multiplication.
The trick is that "there exists" can be removed if one also allows the order and statements such as "$x$ is divisible by $3$".