Colacito, Almudena; Metcalfe, George Proof theory and ordered groups. (English) Zbl 1496.03227 Kennedy, Juliette (ed.) et al., Logic, language, information, and computation. 24th international workshop, WoLLIC 2017, London, UK, July 18–21, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10388, 80-91 (2017). Summary: Ordering theorems, characterizing when partial orders of a group extend to total orders, are used to generate hypersequent calculi for varieties of lattice-ordered groups (\(\ell\)-groups). These calculi are then used to provide new proofs of theorems arising in the theory of ordered groups. More precisely: an analytic calculus for abelian \(\ell\)-groups is generated using an ordering theorem for abelian groups; a calculus is generated for \(\ell\)-groups and new decidability proofs are obtained for the equational theory of this variety and extending finite subsets of free groups to right orders; and a calculus for representable \(\ell\)-groups is generated and a new proof is obtained that free groups are orderable.For the entire collection see [Zbl 1369.03021]. Cited in 3 Documents MSC: 03F03 Proof theory in general (including proof-theoretic semantics) 06F15 Ordered groups PDFBibTeX XMLCite \textit{A. Colacito} and \textit{G. Metcalfe}, Lect. Notes Comput. Sci. 10388, 80--91 (2017; Zbl 1496.03227) Full Text: DOI arXiv