Theory and Logic

Speaker: George Metcalfe (University of Bern)

Date: Wednesday, 27.11.2013
Time: 17:00-18:00
Place: Seminar room "Gödel", Favoritenstraße 9

Abstract:
Proof theory can provide useful tools for tackling problems in algebra.
In particular, Gentzen systems admitting cut-elimination have been used to
establish decidability, complexity, amalgamation, admissibility, and
generation results for varieties of residuated lattices corresponding to
substructural logics. However, for classes of algebras bearing some family
resemblance to groups, such as lattice-ordered groups, MV-algebras,
BL-algebras, and cancellative residuated lattices, the proof-theoretic
approach has  met so far only with limited success.

The main aim of this talk will be to introduce proof-theoretic methods for the class of lattice-ordered groups and to explain how these methods can be used to obtain new syntactic proofs of two core theorems: 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.