Quantifier elimination in ordered abelian groups

TL;DR

This paper presents a new proof of quantifier elimination for ordered abelian groups, showing that definable sets are unions of quantifier-free sets parameterized by ordered sets, and that definable functions are piecewise affine linear.

Contribution

It introduces a novel proof of quantifier elimination relative to ordered sets in ordered abelian groups, and characterizes definable functions as piecewise affine linear.

Findings

Definable sets are unions of quantifier-free definable sets parameterized by ordered sets.

All definable functions are piecewise affine linear.

Provides a new perspective on the structure of definable sets and functions in ordered abelian groups.

Abstract

We give a new proof of quantifier elimination in the theory of all ordered abelian groups in a suitable language. More precisely, this is only "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 runs over a set definable (with quantifiers) in a sort which carries the structure of an ordered set with some additional unary predicates. As a corollary, we find that all definable functions in ordered abelian groups are piecewise affine linear on finitely many definable pieces.