Deciding Whether the Ordering is Necessary in a Presburger Formula (Report‪)‬

Introduction Presburger arithmetic is the fragment of arithmetic concerning the integers with addition and order. Presburger's supervisor considered the decidability of this fragment too modest a result to deserve a Ph.D. degree and he accepted it only as a Master's Thesis in 1928. Looking at the number of citations, we may say that history revised this depreciative judgment long ago. There still remains, at least as far as we can see, some confusion concerning the domain of the structure: Z or N? with or without the order relation? (the main popular mathematical web sites disagree on that respect). The original paper deals with the additive group of positive and negative integers with no binary relation, but in a final remark of the original communication, the author asserts that the same result, namely quantifier elimination, holds when the structure is enriched with the binary relation " ". In [1], which is the main reference on the subject, Presburger arithmetic is defined as the elementary theory of integers with equality, addition and having 0 and 1 as constant symbols and " " as binary predicate, see also [20]. On the other hand, the majority of the "modern" papers referring to Presburger arithmetic is concerned with the natural numbers where the order relation is unnecessary as it is first-order expressible in (N; +}.