Deciding whether the ordering is necessary in a Presburger formula
Christian Choffrut (1), Achille Frigeri (1) (2)
(1) Laboratoire d'informatique Algorithmique : Fondements et Applications
(2) Dipartimento di Matematica, "Francesco Brioschi"
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.
