Introduction

Imagine you are handed a mathematical statement about whole numbers — something like "for every integer x, there exists an integer y such that x = 2y or x = 2y + 1." Can a computer always tell you whether it is true?

For full number theory — Peano arithmetic, which includes both addition and multiplication — the answer is no. Kurt Gödel's incompleteness theorems (1931) showed that no algorithm can decide all true statements, and Alan Turing's halting problem (1936) confirmed undecidability for Peano arithmetic.

But in 1929, the Polish logician Mojżesz Presburger discovered something remarkable: if you remove multiplication and keep only addition, the resulting system — now called Presburger arithmetic — is complete and decidable. Every first-order statement about integers with addition has a proof or a refutation, and a computer can always find which one applies.

The catch? Deciding those statements can be extraordinarily slow. Fischer and Rabin proved in 1974 that any decision procedure requires doubly exponential time in the worst case — a tower of exponentials — making Presburger arithmetic one of the most expensive decidable theories in mathematics.

Try It: Decide a Formula

The algorithm that decides Presburger arithmetic works by quantifier elimination: it progressively removes "for all" and "there exists" quantifiers until it reaches a plain arithmetic truth or falsehood.

Pick a formula below and watch the elimination steps unfold. Each step replaces a quantified variable with a finite case analysis derived purely from addition constraints.

<p class="hint">Select a Presburger formula and watch quantifier elimination decide it step by step. Each step removes one quantifier by replacing it with a finite case analysis over addition constraints.</p>
<div class="formula-picker">
  <label for="fsel"><strong>Formula:</strong></label>
  <select id="fsel"></select>
</div>
<div id="formula-display" class="formula-box"></div>
<div class="btns">
  <button id="btn-step" type="button">Next Step</button>
  <button id="btn-auto" type="button">Run All Steps</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div id="steps-log" class="steps-log"></div>
<div id="verdict" class="verdict"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.formula-picker { display: flex; align-items: center; gap: .6rem; margin-bottom: .6rem; }
select { font: inherit; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px;
         background: #f5f7fa; flex: 1; }
.formula-box { background: #e8eef3; border: 1px solid #cdd9e3; border-radius: 8px;
               padding: .55rem .8rem; font-family: ui-monospace, monospace; font-size: .93rem;
               color: #1d3557; margin-bottom: .6rem; min-height: 2em; line-height: 1.5; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }
.steps-log { display: flex; flex-direction: column; gap: .4rem; max-height: 180px;
             overflow-y: auto; }
.step-card { background: #f5f7fa; border: 1px solid #dde3ea; border-radius: 7px;
             padding: .4rem .7rem; font-size: .84rem; line-height: 1.45; }
.step-card .label { font-weight: 700; color: #1d3557; margin-bottom: .15rem; }
.step-card .expr { font-family: ui-monospace, monospace; color: #333; }
.step-card .expl { color: #555; font-style: italic; margin-top: .1rem; }
.verdict { font: 700 1rem system-ui, sans-serif; margin-top: .5rem; min-height: 1.4em; }
.verdict.true  { color: #0a7d33; }
.verdict.false { color: #c92f3c; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Presburger Arithmetic — Quantifier Elimination Demo
// We represent a small set of hand-crafted formulas and their pre-computed
// elimination steps so the demo is self-contained (no SMT solver needed).
// Each formula object has:
//   label      – display name
//   formula    – pretty mathematical string
//   steps      – array of {label, expr, expl} elimination steps
//   verdict    – true | false
//   verdictMsg – plain-English explanation

const FORMULAS = [
  {
    label: "Every integer is even or odd",
    formula: "∀x ∃y ( x = 2·y  ∨  x = 2·y + 1 )",
    steps: [
      {
        label: "Step 1 — Eliminate ∃y",
        expr: "∀x ( (x mod 2 = 0) ∨ (x mod 2 = 1) )",
        expl: "Replace '∃y (x = 2y ∨ x = 2y+1)' by the remainder condition: x leaves remainder 0 or 1 when divided by 2."
      },
      {
        label: "Step 2 — Simplify modular cases",
        expr: "∀x ( x mod 2 ∈ {0, 1} )",
        expl: "The two cases cover all possible remainders mod 2 (only 0 and 1 exist), so the disjunction always holds."
      },
      {
        label: "Step 3 — Eliminate ∀x",
        expr: "TRUE",
        expl: "The body holds for every integer x by exhaustive case analysis on x mod 2. No counterexample exists."
      }
    ],
    verdict: true,
    verdictMsg: "TRUE — every integer is either even (2y) or odd (2y+1). Verified by quantifier elimination."
  },
  {
    label: "There exist two consecutive integers summing to 5",
    formula: "∃x ( x + (x + 1) = 5 )",
    steps: [
      {
        label: "Step 1 — Simplify body",
        expr: "∃x ( 2·x + 1 = 5 )",
        expl: "Combine like terms: x + (x+1) = 2x + 1."
      },
      {
        label: "Step 2 — Isolate x",
        expr: "∃x ( 2·x = 4 )",
        expl: "Subtract 1 from both sides: 2x = 4."
      },
      {
        label: "Step 3 — Eliminate ∃x",
        expr: "4 mod 2 = 0",
        expl: "∃x (2x = 4) holds iff 4 is divisible by 2 (the coefficient). Check: 4 mod 2 = 0. ✓"
      },
      {
        label: "Step 4 — Evaluate constant",
        expr: "TRUE  (x = 2, since 2+3 = 5)",
        expl: "The modular condition is satisfied. The witness is x = 2: 2 + 3 = 5."
      }
    ],
    verdict: true,
    verdictMsg: "TRUE — x = 2 and x+1 = 3 sum to 5. Quantifier elimination finds the witness automatically."
  },
  {
    label: "There exist two integers summing to 1 both divisible by 2",
    formula: "∃x ∃y ( x + y = 1  ∧  2|x  ∧  2|y )",
    steps: [
      {
        label: "Step 1 — Substitute divisibility",
        expr: "∃x ∃y ( x + y = 1  ∧  x mod 2 = 0  ∧  y mod 2 = 0 )",
        expl: "Replace '2|x' with 'x mod 2 = 0' and likewise for y."
      },
      {
        label: "Step 2 — Eliminate ∃y",
        expr: "∃x ( x mod 2 = 0  ∧  (1 - x) mod 2 = 0 )",
        expl: "From x + y = 1, substitute y = 1 - x. The constraint becomes (1-x) mod 2 = 0."
      },
      {
        label: "Step 3 — Modular arithmetic",
        expr: "∃x ( x mod 2 = 0  ∧  1 mod 2 = 0 )",
        expl: "(1-x) mod 2 = 0 iff 1 mod 2 = x mod 2 = 0. But 1 mod 2 = 1 ≠ 0, contradiction."
      },
      {
        label: "Step 4 — Eliminate ∃x",
        expr: "FALSE",
        expl: "The body requires 1 mod 2 = 0, which is false. No integer x can satisfy it."
      }
    ],
    verdict: false,
    verdictMsg: "FALSE — the sum of two even integers is always even, so it can never equal 1 (odd). Quantifier elimination reveals the contradiction."
  },
  {
    label: "For all x > 0, there exists y with x < y < 2x",
    formula: "∀x ( x > 0 → ∃y ( x < y  ∧  y < 2·x ) )",
    steps: [
      {
        label: "Step 1 — Eliminate ∃y",
        expr: "∀x ( x > 0 → x + 1 ≤ 2·x - 1 )",
        expl: "The smallest y satisfying x < y is x+1. We need x+1 < 2x, i.e., x+1 ≤ 2x-1 (integers)."
      },
      {
        label: "Step 2 — Simplify inequality",
        expr: "∀x ( x > 0 → x ≥ 2 )",
        expl: "x+1 ≤ 2x-1 simplifies to 2 ≤ x, i.e., x ≥ 2."
      },
      {
        label: "Step 3 — Check x = 1",
        expr: "1 > 0 → 1 ≥ 2  ⟹  TRUE → FALSE",
        expl: "The antecedent holds (1 > 0) but the consequent fails (1 < 2). Counterexample: x = 1."
      },
      {
        label: "Step 4 — Eliminate ∀x",
        expr: "FALSE",
        expl: "x = 1 is a counterexample: there is no integer y with 1 < y < 2 (no integer lies strictly between 1 and 2)."
      }
    ],
    verdict: false,
    verdictMsg: "FALSE — for x = 1 there is no integer strictly between 1 and 2. (This would be true for real numbers but fails for integers.)"
  }
];

let current = 0;   // selected formula index
let stepIdx  = 0;  // next step to show

const fsel    = document.getElementById('fsel');
const fdisp   = document.getElementById('formula-display');
const log     = document.getElementById('steps-log');
const verdict = document.getElementById('verdict');
const btnStep = document.getElementById('btn-step');
const btnAuto = document.getElementById('btn-auto');
const btnReset= document.getElementById('btn-reset');

// Populate selector
FORMULAS.forEach((f, i) => {
  const o = document.createElement('option');
  o.value = i; o.textContent = f.label;
  fsel.appendChild(o);
});

function reset() {
  current  = Number(fsel.value);
  stepIdx  = 0;
  const f  = FORMULAS[current];
  fdisp.textContent = f.formula;
  log.innerHTML     = '';
  verdict.textContent = '';
  verdict.className   = 'verdict';
  btnStep.disabled    = false;
  btnAuto.disabled    = false;
}

function addStep(s) {
  const card = document.createElement('div');
  card.className = 'step-card';
  card.innerHTML =
    `<div class="label">${s.label}</div>` +
    `<div class="expr">${s.expr}</div>` +
    `<div class="expl">${s.expl}</div>`;
  log.appendChild(card);
  log.scrollTop = log.scrollHeight;
}

function showVerdict() {
  const f = FORMULAS[current];
  verdict.textContent = f.verdictMsg;
  verdict.className   = 'verdict ' + (f.verdict ? 'true' : 'false');
  btnStep.disabled    = true;
  btnAuto.disabled    = true;
  console.assert(
    typeof f.verdict === 'boolean',
    'Formula verdict must be boolean'
  );
}

function doStep() {
  const f = FORMULAS[current];
  if (stepIdx < f.steps.length) {
    addStep(f.steps[stepIdx]);
    stepIdx++;
  }
  if (stepIdx >= f.steps.length) {
    showVerdict();
  }
}

function doAll() {
  const f = FORMULAS[current];
  while (stepIdx < f.steps.length) doStep();
}

fsel.addEventListener('change', reset);
btnStep.addEventListener('click', doStep);
btnAuto.addEventListener('click', doAll);
btnReset.addEventListener('click', reset);

// Verify all formulas have steps and correct verdict types
FORMULAS.forEach((f, i) => {
  console.assert(f.steps.length > 0, fmt('Formula %i% has no steps', { i: i }));
  console.assert(typeof f.verdict === 'boolean', fmt('Formula %i% verdict not boolean', { i: i }));
});

reset();
Result
Console

Notice that even for small formulas the case analysis can branch quickly. Checking a quantifier-free arithmetic fact (like 3 + 5 = 8) is instant. Deciding a formula with many nested quantifiers requires exponentially more case splits at each level — a glimpse of the doubly exponential blowup proved by Fischer and Rabin.

The Real Complexity

Presburger arithmetic sits at a fascinating point in the landscape of mathematical logic:

  • Decidable (proven by Presburger, 1929): for every first-order statement about integers using only addition, equality, and logical connectives, there is an algorithm that terminates and says true or false. This is far from obvious — the domain is infinite.
  • Complete: every true statement has a proof; there are no Gödel-style gaps. This stands in stark contrast to Peano arithmetic, where true statements exist that cannot be proved.
  • Doubly exponential lower bound (Fischer & Rabin, 1974): any decision procedure must, in the worst case, run in time at least 22(cn2^{2^(cn}) for some constant c, where n is the length of the formula. No polynomial or even singly exponential algorithm can exist.
  • The culprit is quantifier alternation: each "∀ x ∃ y …" layer roughly squares the complexity. A formula with k alternating quantifier blocks can force case splits that multiply together, stacking exponentials.
  • Contrast with Peano arithmetic (addition + multiplication): as proved by Gödel and later formalized by Turing and Church, that system is undecidable — no algorithm terminates for all inputs. Multiplication is the ingredient that pushes number theory beyond the decidable frontier.

The boundary between addition alone (decidable, doubly exponential) and addition-plus-multiplication (undecidable) is one of the sharpest dividing lines in all of logic. It shows how a single operation can transform a tractable system into one beyond any algorithm's reach. For a broader view of what decidability means in practice, see the Halting Problem and P vs NP.

Where It Matters

Although Presburger arithmetic is a purely theoretical fragment of logic, it powers a surprising range of real-world tools:

  • Program verification and static analysis: properties like "this array index is always in bounds" or "this counter never goes negative" are Presburger statements when the code uses only addition and comparisons. Tools like Omega, ISL, and LLVM's polyhedral analysis use Presburger decision procedures internally.
  • Compiler loop optimization: transformations such as loop fusion, tiling, and parallelization require proving that index expressions (always linear arithmetic) satisfy certain inequalities. Polyhedral compilers like Polly solve Presburger constraints to restructure loops for modern CPUs and GPUs.
  • Hardware model checking: verifying that a counter-based circuit never reaches a forbidden state often reduces to Presburger arithmetic, enabling automatic formal proofs.
  • Scheduling and resource allocation: "can these tasks be assigned to time slots without conflict?" is a constraint problem expressible in Presburger arithmetic when all constraints are additive.
  • Database query optimization: certain integer constraints in query plans can be simplified or proven satisfiable using Presburger decision procedures.

The fact that these tools work at all — despite the doubly exponential worst case — is because practical formulas tend to have few quantifier alternations and small coefficients, keeping the actual runtime manageable. Presburger arithmetic is the theoretical guarantee that the tool can always terminate with an answer.

Conclusion

Presburger arithmetic occupies a rare and beautiful position: it is rich enough to express countless real questions about integers, yet restricted just enough for every such question to have an algorithmic answer. Remove multiplication and the infinite universe of numbers becomes — at least in principle — fully tamed.

The price of that tameness is steep: doubly exponential time in the worst case. But the theoretical guarantee matters enormously. It tells engineers that their loop-analysis tools will terminate, that their array-bounds checker can always give a verdict, and that integer linear constraints are decidable.

Add multiplication back and the guarantee vanishes. Gödel's incompleteness and Turing's undecidability take over, and no algorithm can cover all cases. That single operator — multiplication — is the wall between the decidable and the unknowable. Presburger arithmetic lives on exactly the right side of that wall.

To explore the broader picture of what computers can and cannot decide, see the Halting Problem and Diophantine equations.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/presburger-arithmetic/Content licensed under CC BY-NC 4.0.