Quantifier elimination in ordered abelian groups (Q763703)

A new quantifier elimination proof is given for the theory of all ordered abelian groups. This result was already shown by Gurevich and Schmitt by a different method. Here a new language is introduced, allowing a quantifier elimination ``relative'' to ordered sets in the following sense: Each definable set in the group is a union of a family of quantifier-free definable sets, where the parameter of the family ranges over a set definable (with quantifiers) in a sort which carries the structure of an ordered set with some additional unary predicates. The relation between this approach and the one by Gurevich and Schmitt is illustrated. As a corollary of the quantifier elimination theorem, a result of piecewise linearity of definable functions is obtained. In more detail, it is shown that, for every definable function \(f : G^n \rightarrow G\) in an ordered abelian group \(G\), there is a partition of \(G^n\) into finitely many definable sets such that the restriction of \(f\) to any of these sets is of the form \(f(x_1, \dots, x_n) = {1 \over s} \sum_i (r_i x_i + b)\) where \(r_i\), \(s\) are integers and \(b \in G\).