Presburger arithmetic

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 Fischer & 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 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 doubly exponential length proofs. Intuitively, this suggests there are computational limits on what can be proven by computer programs. 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 (1978).

A more tight complexity bound was shown using alternating complexity classes by Berman (1980). The set of true statements in Presburger arithmetic (PA) is shown complete for TimeAlternations(2^2nO(1), n). Thus, its complexity is between double exponential nondeterministic time (2-NEXP) and double exponential space (2-EXPSPACE). Completeness is under polynomial time many-to-one reductions. (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 Σ_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.[8]
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.[9]

Short ${\displaystyle \Sigma _{n}}$ Presburger Arithmetic (${\displaystyle n>2}$) is ${\displaystyle \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 \Sigma _{2}}$ two variable PA (without the restriction of being 'short') is NP-complete.[10] Short ${\displaystyle \Pi _{2}}$ (and thus ${\displaystyle \Sigma _{2}}$) PA is in P, and this extends to fixed-dimensional parametric integer linear programming.[11]

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 ${\displaystyle i<d}$ and ${\displaystyle j\in \mathbb {N} }$ is defined as

${\displaystyle \left\{(x_{0},\ldots ,x_{i-1},x_{i+1},\ldots ,x_{d-1})\in \mathbb {N} ^{d-1}\mid (x_{0},\ldots ,x_{i-1},j,x_{i+1},\ldots ,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},\ldots ,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},\ldots ,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},\ldots ,p_{d-1})}$-periodic for some ${\displaystyle (p_{0},\dots ,p_{d-1})\in \mathbb {Z} ^{d}}$ such that

${\displaystyle \sum _{i=0}^{d-1}|p_{i}|<s.}$

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

${\displaystyle C(k,(x_{0},\ldots ,x_{d-1}))=\left\{(x_{0}+c_{0},\dots ,x_{d-1}+c_{d-1})\mid 0\leq c_{i}<k\right\}}$

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},\ldots ,x_{d-1})>t}$ or by ${\displaystyle \max(x_{0},\ldots ,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 an automatic sequence accepts a Presburger-definable set.