Editing Presburger arithmetic (section)

==Presburger-definable integer relation==
Some properties are now given about integer [[Finitary relation|relations]] 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 a [[semilinear set]].{{sfn|Ginsburg|Spanier|1966|pp=285–296}}

A unary integer relation <math>R</math>, 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 <math>t\in \N</math> and a positive period <math>p\in\N^{>0}</math> such that, for all integer <math>n</math> such that <math>|n|\ge t</math>, <math>n\in R</math> if and only if <math>n+p\in R</math>.

By the [[Cobham–Semenov theorem]], a relation is Presburger-definable if and only if it is definable in [[Büchi arithmetic]] of base <math>k</math> for all <math>k\ge2</math>.{{sfn|Cobham|1969|pp=186–192}}{{sfn|Semenov|1977|pp=403–418}} A relation definable in Büchi arithmetic of base <math>k</math> and <math>k'</math> for <math>k</math> and <math>k'</math> being [[Multiplicative independence|multiplicatively independent]] integers is Presburger definable.

An integer relation <math>R</math> is Presburger-definable if and only if all sets of integers that are definable in first-order logic with addition and <math>R</math> (that is, Presburger arithmetic plus a predicate for <math>R</math>) are Presburger-definable.{{sfn|Michaux|Villemaire|1996|pp=251–277}} Equivalently, for each relation <math>R</math> that is not Presburger-definable, there exists a first-order formula with addition and <math>R</math> that defines a set of integers that is not definable using only addition.

===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.