Editing Presburger arithmetic (section)

===Muchnik's characterization===
Presburger-definable relations admit another characterization: by Muchnik's theorem.{{sfn|Muchnik|2003|pp=1433–1444}} 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 <math>R\subseteq\N^d</math> be a set, the section <math>x_i = j</math> of <math>R</math>, for <math>i < d</math> and <math>j \in \N</math> is defined as 
:<math>\left \{(x_0,\ldots,x_{i-1},x_{i+1},\ldots,x_{d-1})\in\N^{d-1}\mid(x_0,\ldots,x_{i-1},j,x_{i+1},\ldots,x_{d-1})\in R \right \}.</math>

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

:<math>\sum_{i=0}^{d-1}|p_i| < s.</math>

Finally, for <math>k,x_0,\dots,x_{d-1}\in\N</math> let 
:<math>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 \}</math> 
denote the cube of size <math>k</math> whose lesser corner is <math>(x_0,\dots,x_{d-1})</math>.

{{math theorem|name=Muchnik's Theorem|math_statement= <math>R\subseteq\N^d</math> is Presburger-definable if and only if:
* if <math>d > 1</math> then  all sections of <math>R</math> are Presburger-definable and 
* there exists <math>s\in\N</math> such that, for every <math>k\in\N</math>, there exists <math>t\in\N</math> such that for all <math>(x_0,\dots,x_{d-1})\in\N^d</math> with <math display="block">\sum_{i=0}^{d-1}x_i>t,</math> <math>R</math> is {{nowrap|<math>s</math>-periodic}} in <math>C(k,(x_0,\dots,x_{d-1}))</math>.}}

Intuitively, the integer <math>s</math> represents the length of a shift, the integer <math>k</math> is the size of the cubes and <math>t</math> is the threshold before the periodicity. This result remains true when the condition 

:<math>\sum_{i=0}^{d-1}x_i>t</math> 

is replaced either by <math>\min(x_0,\ldots,x_{d-1})>t</math> or by <math>\max(x_0,\ldots,x_{d-1})>t</math>.

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 {{nowrap|<math>d</math>-ary}} predicate <math>R</math> that holds if and only if <math>R</math> 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.