Proof Theory and Ordered Groups

TL;DR

This paper develops hypersequent calculi based on ordering theorems to analyze varieties of lattice-ordered groups, providing new proofs and decidability results in the theory of ordered groups.

Contribution

It introduces new hypersequent calculi for various classes of lattice-ordered groups, leading to novel proofs and decidability results in ordered group theory.

Findings

An analytic calculus for abelian l-groups was developed.

Decidability of the equational theory of l-groups was established.

New proofs that free groups are orderable were provided.

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 (l-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 l-groups is generated using an ordering theorem for abelian groups; a calculus is generated for l-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 l-groups is generated and a new proof is obtained that free groups are orderable.