Presburger arithmetic: the decidable island

What if every yes-or-no question you could ask about addition had a guaranteed algorithmic answer?

Not “probably correct.” Not “works on the examples we tested.” A genuine guarantee: give me any sentence about natural numbers and addition, and I will tell you, in finite time, whether it is true or false.

That guarantee exists. It is called Presburger arithmetic, and it was proved in 1929 by Mojżesz Presburger, a student in Warsaw, two years before Gödel showed that full arithmetic cannot have this property.

The trick is not magic. It is scope. Presburger arithmetic talks about natural numbers with addition and nothing else. No multiplication, no exponentiation, no general recursion. By giving up those operations, the language stays small enough that every question in it is algorithmically decidable.

This tutorial builds Presburger arithmetic from scratch: the numbers, the axioms, the formulas, and the decision procedure. It ends with the reason this matters in practice: the fragment that powers array-bounds checking, loop analysis, and high-assurance verification in real tools is, at bottom, Presburger arithmetic.

Part I: building numbers from nothing

Presburger arithmetic starts with two primitives:

1. A constant: $0$ (zero).
2. A function: $S$ (successor), which takes a number and returns the next one.

That is all.

Every natural number is built by applying $S$ some number of times to $0$:

The symbols $1, 2, 3, \ldots$ are shorthand. They are not primitive. The only things that actually exist in the language are $0$ and $S$.

This is not an arbitrary choice. It is a design decision with a payoff: because every number is built from the same two pieces, proofs about all numbers can proceed by induction on the structure of $S$.

Try building numbers yourself:

Part II: the five axioms

Presburger arithmetic is defined by five axioms (the fifth is actually an axiom schema, meaning it generates infinitely many axioms, one for each formula in the language).

The five axioms at a glance

Axiom 1: zero is not a successor

In English: No number has zero as its successor. Zero is the beginning of the line, not a place you can reach by counting forward.

What it rules out: Without this axiom, the number line could loop. Some number’s successor could be zero, creating a cycle. This axiom forces the chain to be one-directional.

Axiom 2: successor is injective

In English: If two numbers have the same successor, they are the same number. The successor function never merges two different numbers into one.

What it rules out: Without this axiom, the number line could branch backward: two different numbers could both have the same next number. Injectivity says the line never converges.

Together, Axioms 1 and 2 ensure the natural numbers form a single, infinite, non-looping, non-merging chain starting at zero.

Axiom 3: additive identity

In English: Adding zero to any number gives back the same number.

What it provides: The base case for defining addition. Every recursive computation of $x + y$ will eventually reach $x + 0$ and stop.

Axiom 4: addition recurses through successor

In English: Adding the successor of $y$ to $x$ is the same as first adding $y$ to $x$ and then taking the successor. Addition peels one $S$ off the second argument at each step.

What it provides: The recursive step. Together with Axiom 3, this completely determines the value of $x + y$ for any two natural numbers: apply Axiom 4 repeatedly until the second argument is $0$, then apply Axiom 3.

Axiom 5: induction (restricted)

For every formula $\varphi(x)$ in the language ${0, S, +}$:

In English: If a property holds for zero, and whenever it holds for a number it also holds for that number’s successor, then it holds for every natural number.

The critical restriction: The formula $\varphi$ must be expressible in the language of Presburger arithmetic: it can only mention $0$, $S$, $+$, $=$, and the logical connectives. It cannot mention multiplication, exponentiation, or any other operation.

This restriction is what separates Presburger from Peano arithmetic. Peano allows induction over any first-order formula, including those that mention multiplication. That extra power is exactly what makes Peano arithmetic undecidable.

Induction at work: proving $0 + n = n$

Axiom 3 says $x + 0 = x$. But what about $0 + x = x$? That is not an axiom. The addition rules recurse on the second argument, so $0 + x$ requires actual work to evaluate. This is where induction earns its keep.

Claim: $\forall n.\; 0 + n = n$

Proof by induction on $n$:

Base case ($n = 0$):

Inductive step. Assume $0 + k = k$ for some $k$. Show $0 + S(k) = S(k)$:

Conclusion. By Axiom 5 (induction), $\forall n.\; 0 + n = n$. $\square$

Two lines of real work. But each line is licensed: one by Axiom 4, one by the inductive hypothesis. That is the difference between “obviously true” and “proved from the axioms.” A machine can check this derivation with no understanding of what addition means.

Part III: cheatsheet for reading logic formulas

Logic notation can look alien on first contact. This reference card covers every symbol used in Presburger arithmetic.

How to read a formula aloud

Start from the outside and work inward. Quantifiers set the stage; the body makes the claim.

Example 1:

Read: “For every $x$, $x$ plus zero equals $x$.” This is Axiom 3.

Example 2:

Read: “There exists an $x$ such that $x$ plus $x$ equals four.” This asks whether 4 is even. It is true: $x = 2$ is a witness.

Example 3:

Read: “For every $x$, there exists a $y$ such that $x$ plus $y$ equals five.” Is this true? No. When $x = 6$, no natural number $y$ satisfies $6 + y = 5$.

Example 4:

Read: “There exists an $x$ whose successor is zero.” This is false by Axiom 1.

Part IV: addition, step by step

Axioms 3 and 4 together make addition a purely mechanical process. Here is $2 + 3 = 5$ derived line by line.

Each line applies exactly one axiom. Three applications of Axiom 4 peel the three $S$’s from the second argument. Then Axiom 3 resolves the base case. The result accumulates as nested $S$’s around the first argument.

This is not hand-waving. It is a derivation: every step is licensed by a specific rule, and a machine could check each step mechanically. That is the difference between arriving at an answer and proving one.

Addition as a program

The axioms are also a program. Here is a Python implementation that follows the axioms exactly:

def add(x, y):
    """Presburger addition, axiom by axiom."""
    if y == 0:
        return x          # Axiom 3: x + 0 = x
    else:
        return add(x, y - 1) + 1  # Axiom 4: x + S(y) = S(x + y)

The recursion peels $S$ off the second argument, exactly as the axioms prescribe. The base case returns $x$ unchanged, exactly as Axiom 3 says. This is not an analogy. The program and the derivation are the same computation.

Part V: what you can say in Presburger arithmetic

The language is small (just $0$, $S$, and $+$) but it can express more than it first appears.

Ordering

The relation $x < y$ is not primitive, but it is definable:

“$x$ is less than $y$ if and only if there exists a positive number $z$ such that $x + (z + 1) = y$.” This works because $S(z)$ is always at least 1.

Evenness

“$x$ is even if and only if there exists a $y$ such that $x$ equals $y$ plus $y$.” Since there is no multiplication symbol, we write $2y$ as $y + y$.

Divisibility by a fixed constant

For any fixed $n$, “$n$ divides $x$” is expressible:

This is a crucial pattern: while Presburger arithmetic has no multiplication function, it can express divisibility by any fixed constant using repeated addition. The constant must be fixed in the formula; you cannot quantify over divisors.

Modular arithmetic

Congruence modulo a fixed constant is also expressible. For example, “$x$ leaves remainder 2 when divided by 3” is:

The pattern generalizes: for any fixed $n$ and remainder $r$, write $n$ copies of $q$ added together, then add $r$ as a successor numeral. The key word is fixed: both $n$ and $r$ must be constants baked into the formula.

This expressiveness matters because the decision procedure reduces every Presburger formula to a Boolean combination of exactly these two kinds of constraint: linear inequalities and divisibility conditions.

Some example sentences and their truth values

Every one of these questions has a definite, algorithmically computable answer. That is decidability.

Part VI: what “decidable” actually means

A theory is decidable if there exists an algorithm that:

1. takes any sentence in the language as input,
2. always terminates (no infinite loops, no timeouts, no “try harder”),
3. correctly outputs TRUE or FALSE.

Presburger arithmetic is decidable. Mojżesz Presburger proved this in 1929, presenting his result at the First Congress of Mathematicians of Slavic Countries in Warsaw.

This means there is a machine (not a heuristic, not a best-effort search, but a terminating algorithm) that can answer every question expressible in the language ${0, S, +}$.

The algorithm does not need to be fast. Presburger’s decision procedure has high worst-case complexity (at least doubly exponential in the length of the formula). But it always finishes, and it is always right. For finite or bounded queries, modern implementations are practical.

What decidability is not

Decidability does not mean the theory is trivial. It means the theory is tame enough that a machine can navigate it exhaustively.

Decidability does not mean every proof is short. Some true sentences have only very long proofs. But the decision procedure always finds one.

Decidability does not mean every question is easy to answer quickly. The worst-case complexity is very high. But “always terminates with the right answer, eventually” is still a vastly stronger guarantee than “might loop forever” or “might give the wrong answer.”

The contrast with Peano arithmetic

Peano arithmetic extends Presburger arithmetic by adding multiplication and allowing induction over all formulas.

That extension destroys decidability:

1. Gödel’s first incompleteness theorem (1931): There exist sentences in Peano arithmetic that are true in $\mathbb{N}$ but not provable from the axioms.
2. Undecidability: No algorithm can decide all sentences of Peano arithmetic.
3. Encoding power: With multiplication, you can encode Turing machines, and the halting problem reduces to arithmetic truth.

Presburger arithmetic avoids all three of these. Its completeness and decidability come precisely from excluding multiplication.

Part VII: the boundary, and what multiplication destroys

The difference between Presburger and Peano arithmetic is exactly one operation: ×.

The loss of decidability is not gradual. It is a sharp boundary. The moment a formula can write x × y = z, it can encode arbitrary computation, and the halting problem infects the theory.

To see the boundary concretely, consider primality. In Peano arithmetic, “$x$ is prime” is expressible:

This formula uses multiplication between two variables ($a \times b$). There is no way to rewrite it using only addition. You cannot check whether a number has non-trivial factors without multiplying. That single operation, variable-times-variable, is enough to encode Turing machines and bring in the halting problem.

In Presburger arithmetic, you can ask “is $x$ divisible by 3?” (since 3 is fixed). But you cannot ask “does $x$ have any divisor other than 1 and itself?” because that would require quantifying over divisors and multiplying them.

This is why Presburger arithmetic’s limitation is actually its greatest strength. By staying on the decidable side of the boundary, every question has a guaranteed answer. For high-assurance software, that guarantee is worth more than the ability to talk about multiplication.

Part VIII: how the decision procedure works

The core technique is quantifier elimination: transform any formula into an equivalent formula with no quantifiers.

The idea

Every Presburger formula, no matter how deeply nested its quantifiers, is equivalent to a Boolean combination of:

• linear inequalities ($a_1 x_1 + a_2 x_2 + \cdots \geq c$), and
• divisibility constraints ($d \mid (a_1 x_1 + \cdots + c)$).

Once all quantifiers are removed, what remains is a finite Boolean expression that can be evaluated directly.

Cooper’s algorithm (sketch)

The standard modern procedure is due to D. C. Cooper (1972). Here is the high-level shape:

1. Normalize the formula so that quantified variables appear in standard positions.
2. Eliminate one quantifier at a time, starting from the innermost.
3. To eliminate $\exists x.\,\psi(x)$:
   • Collect all constraints on $x$ from $\psi$.
   • Identify finitely many candidate values for $x$ from the lower bounds.
   • Replace $\exists x.\,\psi(x)$ with a disjunction: $\psi(c_1) \vee \psi(c_2) \vee \cdots$
4. Universal quantifiers are handled dually: $\forall x.\,\psi(x) \equiv \neg\exists x.\,\neg\psi(x)$.
5. After all quantifiers are eliminated, evaluate the resulting ground expression.

Worked example: “Is 4 even?”

The formula:

Step 1. rewrite in terms of integers: $\exists x.\; 2x = 4$.

Step 2. solve: $x = 2$. This is a natural number, so the existential is satisfied.

Result: TRUE, with witness $x = 2$.

Worked example: “Is 3 even?”

Step 1. rewrite: $\exists x.\; 2x = 3$.

Step 2. solve: $x = 1.5$. This is not a natural number.

Result: FALSE. No witness exists.

Worked example: “Can every number reach 5?”

Step 1. eliminate the inner $\exists y$: $y = 5 - x$. This is a natural number only when $x \leq 5$.

Step 2. the formula reduces to $\forall x.\;(x \leq 5)$.

Step 3. this is false ($x = 6$ is a counterexample).

Result: FALSE.

A formula evaluator in Python

def successor_notation(n):
    """Display n in Presburger's successor notation."""
    if n == 0:
        return "0"
    return f"S({successor_notation(n - 1)})"

def decide_exists_even(n):
    """Decide: ∃x. x + x = n"""
    for x in range(n + 1):
        if x + x == n:
            return True, x     # TRUE with witness
    return False, None         # FALSE, no witness

# Run the decision procedure
for n in range(7):
    result, witness = decide_exists_even(n)
    status = f"TRUE (x = {witness})" if result else "FALSE"
    print(f"∃x. x+x = {successor_notation(n)}  →  {status}")

Output:

∃x. x+x = 0           →  TRUE (x = 0)
∃x. x+x = S(0)        →  FALSE
∃x. x+x = S(S(0))     →  TRUE (x = 1)
∃x. x+x = S(S(S(0)))  →  FALSE
∃x. x+x = S(S(S(S(0))))        →  TRUE (x = 2)
∃x. x+x = S(S(S(S(S(0)))))     →  FALSE
∃x. x+x = S(S(S(S(S(S(0))))))  →  TRUE (x = 3)

The decision procedure separates even from odd, correctly and mechanically, for every input.

Part IX: programs are proofs

There is a deep correspondence between logic and computation discovered independently by Haskell Curry and William Howard.

The Curry-Howard correspondence (informal)

Under this correspondence:

• A proof of $\exists x.\,\varphi(x)$ is a program that computes the witness $x$.
• A proof of $\forall x.\,P(x) \rightarrow Q(x)$ is a program that transforms any proof of $P(x)$ into a proof of $Q(x)$.

What this means for Presburger arithmetic

Presburger’s decision procedure is constructive. When it proves an existential sentence $\exists x.\,\varphi(x)$, it does not merely assert that some $x$ exists. It produces the actual value.

That production is program synthesis:

• Input: a logical specification (a Presburger formula).
• Output: a concrete value satisfying the specification (the witness), together with a proof that it works.

The decision procedure is therefore a synthesizer: you state what you want as a formula, and the procedure either hands you a solution or proves no solution exists.

def synthesize_additive_inverse(target, x):
    """
    Spec: ∃y. x + y = target
    Synthesize y if it exists.
    """
    if x <= target:
        y = target - x
        # Proof obligation: x + y = target
        assert x + y == target, "certificate check failed"
        return y, f"Witness y = {y}, verified: {x} + {y} = {target}"
    else:
        return None, f"No solution: {x} > {target}"

# Synthesize
for x in range(8):
    result, explanation = synthesize_additive_inverse(5, x)
    print(f"  x={x}: {explanation}")

Output:

  x=0: Witness y = 5, verified: 0 + 5 = 5
  x=1: Witness y = 4, verified: 1 + 4 = 5
  x=2: Witness y = 3, verified: 2 + 3 = 5
  x=3: Witness y = 2, verified: 3 + 2 = 5
  x=4: Witness y = 1, verified: 4 + 1 = 5
  x=5: Witness y = 0, verified: 5 + 0 = 5
  x=6: No solution: 6 > 5
  x=7: No solution: 7 > 5

Notice the structure: for each input, the program either synthesizes a witness and verifies it, or proves impossibility. There is no “maybe” and no timeout. That is the programs-are-proofs principle applied to a decidable theory.

The deeper point

In undecidable theories, program synthesis from specifications is not always possible. Some specs have no algorithm that reliably finds a satisfying program.

In Presburger arithmetic, synthesis always works. Every satisfiable existential formula yields a witness. Every unsatisfiable one yields a refutation. The theory is tame enough to be fully mechanized.

This is why decidable fragments matter for engineering: they are the fragments where “prove it correct” and “synthesize it automatically” are the same operation.

Part X: high-assurance software

Presburger arithmetic is not a classroom curiosity. It is the engine behind a large portion of automated software verification.

SMT solvers: the linear arithmetic theory

Modern SMT (Satisfiability Modulo Theories) solvers like Z3 and CVC5 include a theory called Linear Integer Arithmetic (LIA). LIA is essentially Presburger arithmetic presented for solver consumption.

When a verification tool asks “is this integer constraint satisfiable?”, the LIA solver answers using a decision procedure descended from Presburger and Cooper. This happens inside:

• Program analysis tools (abstract interpreters, static analyzers),
• Proof assistants (Isabelle, Lean, Coq, which all delegate integer subgoals to arithmetic solvers),
• Model checkers (CBMC, SPARK, for bounded and unbounded verification of C, Ada, and other code).

Array bounds checking

The question “is arr[i] always within bounds?” typically reduces to:

This is a Presburger formula (variables, addition, ordering, fixed constants). The solver decides it in one pass.

Loop invariant verification

A loop invariant like “the counter stays between 0 and MAX” is:

When the loop body only increments or decrements by constants, the invariant and the transition relation are both in Presburger arithmetic. Verification is decidable.

Compiler optimizations

The polyhedral model for loop optimization (used in LLVM’s Polly, GCC’s Graphite, and research compilers) represents loop iteration spaces as integer polyhedra. Dependence analysis, tiling, interchange, and parallelization all reduce to Presburger queries:

• “Do these two array accesses alias?” is an integer linear constraint check.
• “Can this loop nest be tiled?” is parametric integer programming.
• “Is this schedule valid?” is checking that all dependences are satisfied.

seL4 and kernel verification

The seL4 microkernel’s formal verification includes thousands of subgoals about pointer arithmetic, capability indices, and memory layout. Many of these subgoals are pure Presburger formulas, decided automatically by the arithmetic tactics in Isabelle/HOL.

The pattern

The common thread is this: real systems deal with integers, indices, offsets, and counters. When the operations are limited to addition, subtraction, comparison, and divisibility by constants, and they often are, the problem lives in Presburger arithmetic, and decidability gives you a guarantee that no heuristic can match.

That is the practical payoff of Presburger’s 1929 theorem: a fragment of arithmetic that is powerful enough to express most integer reasoning in software, and tame enough that a machine can always give the right answer.

Where to go deeper

This tutorial covers the core ideas. Several directions lead further.

Automata-theoretic decision procedures. Büchi (1960) showed that a subset of $\mathbb{N}^k$ is Presburger-definable if and only if it is recognizable by a finite automaton when numbers are written in a suitable base. This gives an alternative decision procedure: translate the formula to an automaton, then check emptiness or universality.

Complexity. The decision problem for Presburger arithmetic is at least doubly exponential in the worst case (Fischer and Rabin, 1974). This is the cost of full generality. But many practically occurring formulas have much lower effective complexity, and modern solvers exploit structure aggressively.

Extensions that stay decidable. Some extensions of Presburger arithmetic preserve decidability: adding the divisibility predicates $n \mid x$ explicitly, adding bounded quantifiers, or combining with other decidable theories via the Nelson-Oppen method in SMT solvers.

The Curry-Howard correspondence in full. The connection between proofs and programs runs much deeper than the sketch in Part IX. Martin-Löf type theory, the Calculus of Constructions (the foundation of Coq and Lean), and homotopy type theory all develop this correspondence into a full-scale foundation for mathematics and verified programming.

References

• Presburger, M. (1929) Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, Warsaw, 92–101.
• Cooper, D. C. (1972) Theorem Proving in Arithmetic without Multiplication. Machine Intelligence 7, Edinburgh University Press, 91–99.
• Büchi, J. R. (1960) Weak Second-Order Arithmetic and Finite Automata. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 6, 66–92.
• Fischer, M. J. and Rabin, M. O. (1974) Super-Exponential Complexity of Presburger Arithmetic. SIAM-AMS Proceedings 7, 27–41.
• Gödel, K. (1931) Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 173–198.
• de Moura, L. and Bjørner, N. (2008) Z3: An Efficient SMT Solver. TACAS 2008, Springer LNCS 4963, 337–340.
• Howard, W. A. (1980) The Formulae-as-Types Notion of Construction. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 479–490.
• Klein, G. et al. (2009) seL4: Formal Verification of an OS Kernel. SOSP 2009, ACM, 207–220.