Published online by Cambridge University Press: 20 January 2009
The purpose of this note is to show the existence of a lattice ordered group G with a finite set of generators and a recursively enumerable set of defining relations such that there is no decision procedure to determine whether or not an arbitrary word in the generators reduces to the identity in G. In addition to the usual group-theoretic words, we may also use the two lattice operations ∨ and ∧ ; for example, a−l(b∨c) is a word in the generators a, b and c. At first sight it might appear that since we have an even greater harvest of words than in group theory and there exist finitely presented groups H (H has a finite number of generators and defining relations) with an insoluble word problem (no decision procedure to determine whether an arbitrary word in the generators reduces to the identity)—see (1), (2), (4) or (6)—the same would be true of lattice ordered groups. Unfortunately, such a naïve approach overlooks two salient points. First, the class of lattice ordered groups is strictly smaller than the class of all groups; second, there are certain relations connecting the lattice operations with the group operations which hold true for all lattice ordered groups. For example, a(b∧c) = ab∨ac and (a∨b)−1 = a−1∧b−1.