### Deciding whether the ordering is necessary in a Presburger formula

*Christian Choffrut, Achille Frigeri*

#### Abstract

We characterize the relations which are first-order definable in the model
of the group of integers with the constant 1.
This allows us to show that given a relation defined
by a first-order formula in this model
enriched with the usual ordering, it is recursively decidable
whether or not it is first-order definable without the ordering.

Full Text: PDF PostScript