Presburger arithmetic is thefirst-order theory of thenatural numbers withaddition, named in honor ofMojżesz Presburger, who introduced it in 1929. Thesignature of Presburger arithmetic contains only the addition operation andequality, omitting themultiplication operation entirely. The theory iscomputably axiomatizable; the axioms include a schema ofinduction.

Presburger arithmetic is much weaker thanPeano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is adecidable theory. This means it is possible to algorithmically determine, for any sentence in the language of Presburger arithmetic, whether that sentence is provable from the axioms of Presburger arithmetic. The asymptotic running-timecomputational complexity of this algorithm is at leastdoubly exponential, however, as shown byFischer & Rabin (1974).

The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.

In this language, the axioms of Presburger arithmetic are theuniversal closures of the following:

1. ¬(0 =x + 1)^{[n 1]}
2. x + 1 =y + 1 →x =y
3. x + 0 =x
4. x + (y + 1) = (x +y) + 1
5. LetP(x) be afirst-order formula in the language of Presburger arithmetic with a free variablex (and possibly other free variables). Then the following formula is an axiom:
   (P(0) ∧ ∀x(P(x) →P(x + 1))) → ∀yP(y).

(5) is anaxiom schema ofinduction, representing infinitely many axioms. These cannot be replaced by any finite number of axioms, that is, Presburger arithmetic is not finitely axiomatizable in first-order logic.^[1]

Presburger arithmetic can be viewed as afirst-order theory with equality containing precisely all consequences of the above axioms. Alternatively, it can be defined as the set of those sentences that are true in theintended interpretation: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.

Presburger arithmetic is designed to be complete and decidable. Therefore, it cannot formalize concepts such asdivisibility orprimality, or, more generally, any number concept leading to multiplication of variables. However, it can formulate individual instances of divisibility; for example, it proves "for allx, there existsy : (y +y =x) ∨ (y +y + 1 =x)". This states that every number is either even or odd.

Presburger (1929) proved Presburger arithmetic to be:

• consistent: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
• complete: For each statement in the language of Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation.
• decidable: There exists analgorithm that decides whether any given statement in Presburger arithmetic is a theorem or a nontheorem - note that a "nontheorem" is a formula that cannot be proved, not in general necessarily one whose negation can be proved, but in the case of a complete theory like here the two definitions are equivalent.

The decidability of Presburger arithmetic can be shown usingquantifier elimination, supplemented by reasoning aboutarithmetical congruence.^{[2][3][4][5][6]} The steps used to justify a quantifier elimination algorithm can be used to define computable axiomatizations that do not necessarily contain the axiom schema of induction.^[2][7]

In contrast,Peano arithmetic, which is Presburger arithmetic augmented with multiplication, is not decidable, as proved by Church alongside the negative answer to theEntscheidungsproblem. ByGödel's incompleteness theorem, Peano arithmetic is incomplete and its consistency is not internally provable (but seeGentzen's consistency proof).

The decision problem for Presburger arithmetic is an interesting example incomputational complexity theory andcomputation. Letn be the length of a statement in Presburger arithmetic. ThenFischer & Rabin (1974) proved that, in the worst case, the proof of the statement in first-order logic has length at least${\displaystyle 2^{2^{cn}}}$, for some constantc>0. Hence, their decision algorithm for Presburger arithmetic has runtime at least exponential. Fischer and Rabin also proved that for any reasonable axiomatization (defined precisely in their paper), there exist theorems of lengthn that havedoubly exponential length proofs. Fischer and Rabin's work also implies that Presburger arithmetic can be used to define formulas that correctly calculate any algorithm as long as the inputs are less than relatively large bounds. The bounds can be increased, but only by using new formulas. On the other hand, a triply exponential upper bound on a decision procedure for Presburger arithmetic was proved by Oppen.^{[8][n 2]}

A more tight complexity bound was shown using alternating complexity classes byBerman (1980). The set of true statements in Presburger arithmetic (PA) is shown complete forTimeAlternations(2^2nO(1), n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is underKarp reductions. (Also, note that while Presburger arithmetic is commonly abbreviated PA, in mathematics in general PA usually meansPeano arithmetic.)

For a more fine-grained result, let PA(i) be the set of true Σ_i PA statements, and PA(i, j) the set of true Σ_i PA statements with each quantifier block limited to j variables. '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.
PA(1, j) is in P, while PA(1) is NP-complete.^[9]
For i > 0 and j > 2, PA(i + 1, j) isΣ_i^P-complete. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.
For i>0, PA(i+1) isΣ_i^EXP-complete.^[10]

Short${\displaystyle {\mathrm{\Sigma }}_n}$ Presburger Arithmetic (${\displaystyle n>2}$) is${\displaystyle {\mathrm{\Sigma }}_{n-2}^P}$ complete (and thus NP complete for${\displaystyle n=3}$). Here, 'short' requires bounded (i.e.${\displaystyle O(1)}$) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size). Also,${\displaystyle {\mathrm{\Sigma }}_2}$ two variable PA (without the restriction of being 'short') is NP-complete.^[11] Short${\displaystyle {\mathrm{\Pi }}_2}$ (and thus${\displaystyle {\mathrm{\Sigma }}_2}$) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.^[12]

Because Presburger arithmetic is decidable,automatic theorem provers for Presburger arithmetic exist. For example, theRocq andLean proof assistant systems feature the tacticomega for Presburger arithmetic and theIsabelle proof assistant contains a verified quantifier elimination procedure byNipkow (2010). The double exponential complexity of the theory makes it infeasible to use the theorem provers on complicated formulas, but this behavior occurs only in the presence of nested quantifiers:Nelson & Oppen (1978) describe an automatic theorem prover that uses thesimplex algorithm on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas. More recentsatisfiability modulo theories solvers use completeinteger programming techniques to handle quantifier-free fragment of Presburger arithmetic theory.^[13]

Presburger arithmetic can be extended to include multiplication by constants, since multiplication is repeated addition. Most array subscript calculations then fall within the region of decidable problems.^{[n 3]} This approach is the basis of at least five^{[citation needed]} proof-of-correctness systems forcomputer programs, beginning with theStanford Pascal Verifier in the late 1970s and continuing through to Microsoft's Spec# system of 2005.

Some properties are now given about integerrelations definable in Presburger Arithmetic. For the sake of simplicity, all relations considered in this section are over non-negative integers.

A relation is Presburger-definable if and only if it is asemilinear set.^[14]

A unary integer relation${\displaystyle R}$, that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic. That is, if there exists a threshold${\displaystyle t\in \mathbb{N}}$ and a positive period${\displaystyle p\in {\mathbb{N}}^{>0}}$ such that, for all integer${\displaystyle n}$ such that${\displaystyle |n|\ge t}$,${\displaystyle n\in R}$ if and only if${\displaystyle n+p\in R}$.

By theCobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable inBüchi arithmetic of base${\displaystyle k}$ for all${\displaystyle k\ge 2}$.^[15][16] A relation definable in Büchi arithmetic of base${\displaystyle k}$ and${\displaystyle k^{\prime }}$ for${\displaystyle k}$ and${\displaystyle k^{\prime }}$ beingmultiplicatively independent integers is Presburger definable.

An integer relation${\displaystyle R}$ is Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and${\displaystyle R}$ (that is, Presburger arithmetic plus a predicate for${\displaystyle R}$) are Presburger-definable.^[17] Equivalently, for each relation${\displaystyle R}$ that is not Presburger-definable, there exists a first-order formula with addition and${\displaystyle R}$ that defines a set of integers that is not definable using only addition.

Presburger-definable relations admit another characterization: by Muchnik's theorem.^[18] It is more complicated to state, but led to the proof of the two former characterizations. Before Muchnik's theorem can be stated, some additional definitions must be introduced.

Let${\displaystyle R\subseteq {\mathbb{N}}^d}$ be a set, the section${\displaystyle x_i=j}$ of${\displaystyle R}$, for and${\displaystyle j\in \mathbb{N}}$ is defined as

${\displaystyle \left\{(x_0,\dots ,x_{i-1},x_{i+1},\dots ,x_{d-1})\in {\mathbb{N}}^{d-1}\mid (x_0,\dots ,x_{i-1},j,x_{i+1},\dots ,x_{d-1})\in R\right\}.}$

Given two sets${\displaystyle R,S\subseteq {\mathbb{N}}^d}$ and a${\displaystyle d}$-tuple of integers${\displaystyle (p_0,\dots ,p_{d-1})\in {\mathbb{N}}^d}$, the set${\displaystyle R}$ is called${\displaystyle (p_0,\dots ,p_{d-1})}$-periodic in${\displaystyle S}$ if, for all${\displaystyle (x_0,\dots ,x_{d-1})\in S}$ such that${\displaystyle (x_0+p_0,\dots ,x_{d-1}+p_{d-1})\in S,}$ then${\displaystyle (x_0,\dots ,x_{d-1})\in R}$ if and only if${\displaystyle (x_0+p_0,\dots ,x_{d-1}+p_{d-1})\in R}$. For${\displaystyle s\in \mathbb{N}}$, the set${\displaystyle R}$ is said to be${\displaystyle s}$-periodic in${\displaystyle S}$ if it is${\displaystyle (p_0,\dots ,p_{d-1})}$-periodic for some${\displaystyle (p_0,\dots ,p_{d-1})\in {\mathbb{Z}}^d}$ such that

Finally, for${\displaystyle k,x_0,\dots ,x_{d-1}\in \mathbb{N}}$ let

denote the cube of size${\displaystyle k}$ whose lesser corner is${\displaystyle (x_0,\dots ,x_{d-1})}$.

Intuitively, the integer${\displaystyle s}$ represents the length of a shift, the integer${\displaystyle k}$ is the size of the cubes and${\displaystyle t}$ is the threshold before the periodicity. This result remains true when the condition

${\displaystyle \sum _{i=0}^{d-1}{x}_i>t}$

is replaced either by${\displaystyle min(x_0,\dots ,x_{d-1})>t}$ or by${\displaystyle max(x_0,\dots ,x_{d-1})>t}$.

This characterization led to the so-called "definable criterion for definability in Presburger arithmetic", that is: there exists a first-order formula with addition and a${\displaystyle d}$-ary predicate${\displaystyle R}$ that holds if and only if${\displaystyle R}$ is interpreted by a Presburger-definable relation. Muchnik's theorem also allows one to prove that it is decidable whether anautomatic sequence accepts a Presburger-definable set.

• Robinson arithmetic
• Skolem arithmetic

• A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer

• 1929 introductions
• Formal theories of arithmetic
• Logic in computer science
• Proof theory
• Model theory

• Articles with short description
• Short description is different from Wikidata
• Use dmy dates from January 2026
• All articles with unsourced statements
• Articles with unsourced statements from October 2024
• CS1 Russian-language sources (ru)
• CS1: long volume value