QUANTIFIER ELIMINATION FOR LEXICOGRAPHIC PRODUCTS OF ORDERED ABELIAN GROUPS

Let L-ag = {+, -, 0} be the language of the abelian groups, L an expansion of L-ag(<) by relations and constants, and L-mod = L-ag boolean OR {equivalent to(n)}(n >= 2) where each equivalent to(n) is defined as follows: x equivalent to(n) y if and only if n vertical bar x - y. Let H be a structure for L such that H vertical bar L-ag (<) is a totally ordered abelian group and K a totally ordered abelian group. We consider a product interpretation of H x K with a new predicate I for {0} x K defined by N. Suzuki [9]. Suppose that H admits quantifier elimination in L. 1. If K is a Presburger arithmetic with smallest positive element 1(K) then the product interpretation G of H x K with a new predicate I admits quantifier elimination in L(I, 1) boolean OR L-mod with 1(G) = (0(H), K-1). 2. If K is dense regular and K/nK is finite for every integer n >= 2 then the product interpretation G of H x K with a new predicate I admits quantifier elimination in L(I, D) boolean OR L-mod for some set D of constant symbols where G vertical bar= I (d) for each d is an element of D. 3. If K admits quantifier elimination in L-mod (<, D) for some set D of constant symbols then the product interpretation G of H X K with a new predicate I admits quantifier elimination in L(I, d) boolean OR L-mod unless K is dense regular with K/nK being infinite for some n. Conversely, if the product interpretation G of H x K with a new predicate I admits quantifier elimination in L(I, D) boolean OR L-mod for some set D of constant symbols such that G vertical bar= I (d) for each d is an element of D then H admits quantifier elimination in L boolean OR L-mod, and K admits quantifier elimination in L-mod (<, D). We also discuss the axiomatization of the theory of the product interpretation of H x K.