Abstract
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.
Supported by Swiss National Science Foundation grant 200021_146748 and the EU Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 689176.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Anderson, M.E., Feil, T.H.: Lattice-Ordered Groups: An Introduction. Springer, Heidelberg (1988)
Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Springer, Heidelberg (1981)
Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: cut-elimination and completions. Ann. Pure Appl. Logic 163(3), 266–290 (2012)
Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory: hypersequents and hypercompletions. Ann. Pure Appl. Logic 168(3), 693–737 (2017)
Cignoli, R., D’Ottaviano, I.M.L., Mundici, D.: Algebraic foundations of many-valued reasoning. Kluwer, Berlin (1999)
Clay, A., Smith, L.H.: Corrigendum to [19]. J. Symb. Comput. 44(10), 1529–1532 (2009)
Dantzig, G.B.: Linear Programming and Extensions. Princeton University, Press (1963)
Fuchs, L.: Partially Ordered Algebraic Systems. Pergamon Press, Oxford (1963)
Galatos, N., Metcalfe, G.: Proof theory for lattice-ordered groups. Ann. Pure Appl. Logic 8(167), 707–724 (2016)
Holland, W.C.: The lattice-ordered group of automorphisms of an ordered set. Mich. Math. J. 10, 399–408 (1963)
Holland, W.C.: The largest proper variety of lattice-ordered groups. Proc. Am. Math. Soc. 57, 25–28 (1976)
Holland, W.C., McCleary, S.H.: Solvability of the word problem in free lattice-ordered groups. Houston J. Math. 5(1), 99–105 (1979)
Jipsen, P., Montagna, F.: Embedding theorems for classes of GBL-algebras. J. Pure Appl. Algebra 214(9), 1559–1575 (2010)
Kopytov, V.M., Medvedev, N.Y.: The Theory of Lattice-Ordered Groups. Kluwer, Alphen aan den Rijn (1994)
Metcalfe, G., Olivetti, N., Gabbay, D.: Sequent and hypersequent calculi for abelian and Łukasiewicz logics. ACM Trans. Comput. Log. 6(3), 578–613 (2005)
Metcalfe, G., Olivetti, N., Gabbay, D.: Proof Theory for Fuzzy Logics. Springer, Heidelberg (2008)
Montagna, F., Tsinakis, C.: Ordered groups with a conucleus. J. Pure Appl. Algebra 214(1), 71–88 (2010)
Neumann, B.H.: On ordered groups. Am. J. Math. 71(1), 1–18 (1949)
Smith, L.H.: On ordering free groups. J. Symb. Comput. 40(6), 1285–1290 (2005)
Terui, K.: Which structural rules admit cut elimination? – An algebraic criterion. J. Symbolic Logic 72(3), 738–754 (2007)
Weinberg, E.C.: Free abelian lattice-ordered groups. Math. Ann. 151, 187–199 (1963)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Colacito, A., Metcalfe, G. (2017). Proof Theory and Ordered Groups. In: Kennedy, J., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2017. Lecture Notes in Computer Science(), vol 10388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55386-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-55386-2_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-55385-5
Online ISBN: 978-3-662-55386-2
eBook Packages: Computer ScienceComputer Science (R0)