(Joint work with Nikolaos Galatos.) Proof-theoretic methods provide useful tools for tackling problems for many classes of algebras. In particular, Gentzen systems admitting cut-elimination may be used to establish decidability, complexity, amalgamation, admissibility, and generation results for classes of residuated lattices corresponding to substructural logics. However, for classes of algebras bearing a family resemblance to groups, such methods have so far met only with limited success. The main aim of this talk will be to explain how proof-theoretic methods can be used to obtain new syntactic proofs of two core theorems for the class of lattice-ordered groups: namely, Holland's result that this class is generated as a variety by the lattice-ordered group of order-preserving automorphisms of the real numbers, and the decidability of the word problem for free lattice-ordered groups.
