A simple proof of the hereditary undecidability of the theory of lattice- ordered Abelian groups (Q1064333)

In [Algebra Logika 6, 45-62 (1967; Zbl 0165.318)], \textit{Yu. Gurevich} proved that the class of divisible Archimedean lattice-ordered Abelian groups such that the lattice of carriers is an atomic Boolean algebra has hereditarily undecidable first-order lattice theory. The author provides an elegant proof of a weakened version of this result obtained by omitting the restriction ''divisible Archimedean''. Whereas Gurevich's proof depends heavily on constructing appropriate lattice-ordered groups and interpreting the theory of graphs on the natural numbers, the present proof interprets easily the class of Boolean pairs \(<B,B_ 0,\subseteq >\) with B atomic and \(B_ 0\subseteq B\). Since this class has hereditarily undecidable theory [\textit{S. Burris} and \textit{R. McKenzie}, Mem. Am. Math. Soc. 246 (1981; Zbl 0483.03019)], the result follows. Unfortunately, Burris' proof cannot be extended to get Gurevich's original theorem. Note: by letting G be divisible in the proof, it does extend to Gurevich's result with only the word ''Archimedean'' omitted.