Editing Presburger arithmetic (section)

==Properties==

{{harvtxt|Presburger|1929}} proved Presburger arithmetic to be:
* [[Consistency proof|consistent]]: There is no statement in Presburger arithmetic that can be deduced from the axioms such that its negation can also be deduced.
* [[Completeness (logic)|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. 
* [[Decidability (logic)|decidable]]: There exists an [[algorithm]] 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 both definitions are equivalent.

The decidability of Presburger arithmetic can be shown using [[quantifier elimination]], supplemented by reasoning about [[Modular arithmetic|arithmetical congruence]].{{sfn|Presburger|1929}}{{sfn|Büchi|1962}}{{sfn|Monk|2012|p=240}}{{sfn|Nipkow|2010}}{{sfn|Enderton|2001|p=188}} 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.{{sfn|Presburger|1929}}{{sfn|Stansifer|1984}}

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]]. By [[Gödel's incompleteness theorem]], Peano arithmetic is incomplete and its consistency is not internally provable (but see [[Gentzen's consistency proof]]).

=== Computational complexity ===
The decision problem for Presburger arithmetic is an interesting example in [[computational complexity theory]] and [[computation]]. Let ''n'' be the length of a statement in Presburger arithmetic. Then {{harvtxt|Fischer|Rabin|1974}} proved that, in the worst case, the proof of the statement in first-order logic has length at least <math>2^{2^{cn}}</math>, for some constant ''c''>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 length ''n'' that have [[double exponential function|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. 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 {{harvtxt|Oppen|1978}}.

A more tight complexity bound was shown using alternating complexity classes by {{harvtxt|Berman|1980}}. The set of true statements in Presburger arithmetic (PA) is shown complete for [[Alternating Turing machine|TimeAlternations]](2<sup>2<sup>n<sup>O(1)</sup></sup></sup>, n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under [[Karp reduction]]s. (Also, note that while Presburger arithmetic is commonly abbreviated PA, in mathematics in general PA usually means [[Peano arithmetic]].)

For a more fine-grained result, let PA(i) be the set of true Σ<sub>i</sub> PA statements, and PA(i, j) the set of true Σ<sub>i</sub> PA statements with each quantifier block limited to j variables.  '<' is considered to be quantifier-free; here, bounded quantifiers are counted as quantifiers.<br/>
PA(1, j) is in P, while PA(1) is NP-complete.{{sfn|Nguyen Luu|2018|loc=chapter 3}}<br/>
For i > 0 and j > 2, PA(i + 1, j) is [[Polynomial_hierarchy|Σ<sub>i</sub><sup>P</sup>-complete]]. The hardness result only needs j>2 (as opposed to j=1) in the last quantifier block.<br/>
For i>0, PA(i+1) is [[Exponential_hierarchy|Σ<sub>i</sub><sup>EXP</sup>-complete]].{{sfn|Haase|2014|pp=47:1-47:10}}

Short <math>\Sigma_n</math> Presburger Arithmetic (<math>n>2</math>) is <math>\Sigma_{n-2}^P</math> complete (and thus NP complete for <math>n=3</math>).  Here, 'short' requires bounded (i.e. <math>O(1)</math>) sentence size except that integer constants are unbounded (but their number of bits in binary counts against input size).  Also, <math>\Sigma_2</math> two variable PA (without the restriction of being 'short') is NP-complete.{{sfn|Nguyen|Pak|2017}} Short <math>\Pi_2</math> (and thus <math>\Sigma_2</math>) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.{{sfn|Eisenbrand|Shmonin|2008}}