Proof theory for lattice-ordered groups
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).
- Proof theory and ordered groups
- scientific article; zbMATH DE number 194985
- Lattice-ordered groups in deduction
- scientific article; zbMATH DE number 3904649
- Sequent and hypersequent calculi for abelian and łukasiewicz logics
- On reversing the order of a lattice ordered group
- Ordering groups and validity in lattice-ordered groups
- Model-completions for abelian lattice-ordered groups with finitely many disjoint elements
- Identities in ordered sets
- Varieties of lattice ordered groups
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Analytic calculi for product logics
- Density elimination
- Generalized MV-algebras
- scientific article; zbMATH DE number 192848 (Why is no real title available?)
- scientific article; zbMATH DE number 3601634 (Why is no real title available?)
- Mapping Abelian \(\ell\)-groups with strong unit one-one into MV algebras
- On the Computational Complexity of Algebra on Lattices
- Ordered groups with a conucleus
- Proof Theory for Casari's Comparative Logics
- Proof theory for fuzzy logics
- Proving termination with multiset orderings
- Pseudo MV-algebras are intervals in ℓ-groups
- Residuated lattices. An algebraic glimpse at substructural logics
- Sequent and hypersequent calculi for abelian and łukasiewicz logics
- Substructural fuzzy logics
- The complexity of the word problem for abelian l-groups
- The Largest Proper Variety of Lattice Ordered Groups
- The lattice-ordered group of automorphisms of an ordered set
- A simple proof of the hereditary undecidability of the theory of lattice- ordered Abelian groups
- An alternative proof of distributivity in \(l\)-groups
- Proof theory and ordered groups
- From distributive -monoids to -groups, and back again
- Ordering groups and validity in lattice-ordered groups
- Lattice-ordered groups in deduction
- scientific article; zbMATH DE number 221383 (Why is no real title available?)
- Proof systems for lattice theory
- Free lattices proof-theoretically
- Asymptotic cyclic expansion and bridge groups of formal proofs
- Proof theory of abelian connexive logics
- Equational theories of idempotent semifields
- Proof-theoretic analysis of subabelian lattice logic
- Integrally closed residuated lattices
This page was built for publication: Proof theory for lattice-ordered groups
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287483)
