Open AccessProof theory for lattice-ordered groups
Author(s) -
George Metcalfe
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/3szk
Subject(s) - decidability , mathematical proof , mathematics , lattice (music) , word problem (mathematics education) , automorphism , variety (cybernetics) , residuated lattice , discrete mathematics , class (philosophy) , pure mathematics , algebra over a field , computer science , arithmetic , statistics , physics , geometry , artificial intelligence , acoustics , fuzzy logic
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.