Summary

In any ordered Abelian group, the projection of a finite intersection of generalized halfspaces is a finite intersection of generalized halfspaces. The generalized halfspaces making this result possible were introduced in [7], which showed that regular groups obey the result. Just as before, the result implies a generalization of Farkas' Lemma. The result amounts to a special quantifier-elimination theorem, which is uniform in parameters in a fashion described below.

Introduction

This paper generalizes, to arbitrary ordered Abelian groups, the closure under projection of the class of finite intersections of halfspaces. The result rests on a generalization, of the notion of halfspace, introduced in ([7], Section 4). Just as a halfspace is the solution set of a homogeneous weak linear inequality, so a generalized halfspace is the solution set of a so-called congruence inequality, which combines a weak linear inequality with a congruence in a special way described in Section 2. [7] uses modeltheoretic arguments to show that in any regular group, the class of finite intersections of generalized halfspaces is closed under projection. The language ℒ = {+, −, ≤, 0} of ordered Abelian groups is expanded by new predicate symbols for congruence inequalities, and [7] applies a modeltheoretic test for when a formula is equivalent, modulo a given theory, to a conjunction of atomic formulas. The mathematical challenge in [7] is to extend a congruence-inequality-preserving homomorphism, from a substructure of a direct product of regular groups into a sufficiently saturated regular group, to the entire direct product.