Integrally Closed Residuated Lattices
- PDF / 520,223 Bytes
- 24 Pages / 453.543 x 680.315 pts Page_size
- 86 Downloads / 180 Views
tegrally Closed Residuated Lattices
Abstract. A residuated lattice is said to be integrally closed if it satisfies the quasiequations xy ≤ x =⇒ y ≤ e and yx ≤ x =⇒ y ≤ e, or equivalently, the equations x\x ≈ e and x/x ≈ e. Every integral, cancellative, or divisible residuated lattice is integrally closed, and, conversely, every bounded integrally closed residuated lattice is integral. It is proved that the mapping a → (a\e)\e on any integrally closed residuated lattice is a homomorphism onto a lattice-ordered group. A Glivenko-style property is then established for varieties of integrally closed residuated lattices with respect to varieties of lattice-ordered groups, showing in particular that integrally closed residuated lattices form the largest variety of residuated lattices admitting this property with respect to lattice-ordered groups. The Glivenko property is used to obtain a sequent calculus admitting cut-elimination for the variety of integrally closed residuated lattices and to establish the decidability, indeed PSPACE-completenes, of its equational theory. Finally, these results are related to previous work on (pseudo) BCI-algebras, semi-integral residuated pomonoids, and Casari’s comparative logic. Keywords: Residuated lattice, Lattice-ordered group, Glivenko property, Proof theory, BCI-algebra, Semi-integral residuated pomonoid, Comparative logic.
1.
Introduction
A residuated lattice-ordered monoid (residuated lattice for short) is an algebraic structure A = A, ∧, ∨, ·, \, /, e of type 2, 2, 2, 2, 2, 0 such that A, ∧, ∨ is a lattice, A, ·, e is a monoid, and \, / are left and right residuals of · in the underlying lattice order, i.e., for all a, b, c ∈ A, b ≤ a\c ⇐⇒ ab ≤ c ⇐⇒ a ≤ c/b. These structures form a variety (equivalently, equational class) RL and provide algebraic semantics for substructural logics, as well as encompassing well-studied classes of algebras such as lattice-ordered groups (-groups for short) and lattices of ideals of rings with product and division operators (see, e.g., [4,15,23,28]).
Presented by Daniele Mundici; Received February 9, 2019
Studia Logica https://doi.org/10.1007/s11225-019-09888-9
c Springer Nature B.V. 2019
J. Gil-F´erez et al.
It is proved in [1] that a residuated lattice A is cancellative—i.e., satisfies the monoid quasiequations xy ≈ xz =⇒ y ≈ z and yx ≈ zx =⇒ y ≈ z—if and only if it satisfies the equations x\xy ≈ y and yx/x ≈ y. Cancellative residuated lattices hence form a variety CanRL that subsumes the varieties of -groups LG and their negative cones LG − , but excludes many important residuated lattices studied in logic (e.g., all non-trivial Brouwerian algebras). In [29] it is proved that varieties of cancellative residuated lattices satisfying a further condition are categorically equivalent to varieties of lattice-ordered groups with a co-nucleus. Despite this rich structural theory, however, no analytic (cut-free) proof system is known for CanRL and the decidability of its equational theory is still an open problem. The same issues ari
Data Loading...
