that , if and only if . By the Cobham–Semenov theorem, a relation is Presburger-definable if and only if it is definable in Büchi arithmetic of base for all . A relation definable in Büchi arithmetic of base and for and being multiplicatively independent integers is Presburger definable. An integer relation is Presburger-definable if and only if all sets of integers which are definable in first order logic with addition and (that is, Presburger Arithmetic plus a predicate for ) are Presburger-definable. Equivalently, for each relation which is not Presburger-definable, there exists a first-order formula with addition and which defines a set of integers which is not definable using only addition. Muchnik's characterization Presburger-definable relations admit another characterization: by Muchnik's theorem. 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 be a set, the section of , for and is defined as Given two sets and a of integers , the set is called -periodic in if, for all such that then if and only if . For , the set is said to be in if it is for some such that Finally, for let denote the cube of size whose lesser corner is . Intuitively, the integer represents the length of a shift, the integer is the size of the cubes and is the threshold before the periodicity. This result remains true when the condition is replaced either by or by . 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 predicate which holds if and only if 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. See also Robinson arithmetic Skolem arithmetic References Bibliography , see for an English translation External links A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer 1929 introductions Formal theories of arithmetic Logic in computer science Proof theory Model theory