Proof theory for lattice-ordered groups (Q287483)

The authors develop a proof theory for lattice orderes groups (\(\ell\)-groups), as the title of the paper says.NEWLINENEWLINEThey establish the following three main results.NEWLINENEWLINETheorem 5.4. The variety of \(\ell\)-groups is generated by Aut(\(\mathbb{R}\)), where Aut(\(\mathbb{R}\)) is the set of all order-preserving bijections on the real number chain \(\mathbb{R}\).NEWLINENEWLINEThe result was already proved by \textit{W. C. Holland} [Proc. Am. Math. Soc. 57, 25--28 (1976; Zbl 0339.06011)], however, they give a new syntactic proof and show that an identity is valid in Aut(\(\mathbb{R}\)) if and only if it is valid in all \(\ell\)-groups. It follows from Birkhoff's variety theorems that Aut(\(\mathbb{R}\)) generates the variety \(\mathcal{LG}\) of \(\ell\)-groups. 2. They provide a cut-free proof calculus (analytic hypersequent calculs) for \(\ell\)-groups (Lemma 6.5 and Theorem 6.6).NEWLINENEWLINELemma 6.5. (CUT) is \(G\mathcal{LG}_b\)-admissible.NEWLINENEWLINETheorem 6.6. A basic \(\ell\)-hypersequent \(\mathcal{G}\) is \(G\mathcal{LG}_b\)-derivable if and only if \(\mathcal{G}\) is \(\ell\)-valid.NEWLINENEWLINEFrom this result, they prove the (known) decidability for the equational theory of \(\ell\)-groups and the cut-elimination theorem for the equational logic of \(\ell\)-groups. Moreover, they give a procedure for obtaining proofs of valid \(\ell\)-group identities.NEWLINENEWLINEFrom the result above, they show that the equational theory of \(\ell\)-groups is co-NP complete (Theorem 8.3).