The theory is computably axiomatizable; the axioms include a schema of induction.
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-time computational complexity of this algorithm is at least doubly exponential, however, as shown by Fischer & Rabin (1974).
The language of Presburger arithmetic contains constants 0 and 1 and a binary function +, interpreted as addition.
[1] Presburger arithmetic can be viewed as a first-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 the intended interpretation: the structure of non-negative integers with constants 0, 1, and the addition of non-negative integers.
However, it can formulate individual instances of divisibility; for example, it proves "for all x, there exists y : (y + y = x) ∨ (y + y + 1 = x)".
[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 the Entscheidungsproblem.
Then Fischer & Rabin (1974) proved that, in the worst case, the proof of the statement in first-order logic has length at least
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 length n that have doubly 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.
On the other hand, a triply exponential upper bound on a decision procedure for Presburger arithmetic was proved by Oppen (1978).
The set of true statements in Presburger arithmetic (PA) is shown complete for TimeAlternations(22nO(1), n).
The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.
) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.
For example, the Coq proof assistant system features the tactic omega for Presburger arithmetic and the Isabelle proof assistant contains a verified quantifier elimination procedure by Nipkow (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 the simplex algorithm on an extended Presburger arithmetic without nested quantifiers to prove some of the instances of quantifier-free Presburger arithmetic formulas.
More recent satisfiability modulo theories solvers use complete integer programming techniques to handle quantifier-free fragment of Presburger arithmetic theory.
Most array subscript calculations then fall within the region of decidable problems.
[13] This approach is the basis of at least five[citation needed] proof-of-correctness systems for computer programs, beginning with the Stanford Pascal Verifier in the late 1970s and continuing through to Microsoft's Spec# system of 2005.
Some properties are now given about integer relations definable in Presburger Arithmetic.
For the sake of simplicity, all relations considered in this section are over non-negative integers.
, that is, a set of non-negative integers, is Presburger-definable if and only if it is ultimately periodic.
By the Cobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable in Büchi arithmetic of base
is Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and
Presburger-definable relations admit another characterization: by Muchnik's theorem.
Before Muchnik's theorem can be stated, some additional definitions must be introduced.
Muchnik's theorem also allows one to prove that it is decidable whether an automatic sequence accepts a Presburger-definable set.