Residuated frames with applications to decidability

Authors:
Nikolaos Galatos and Peter Jipsen

Journal:
Trans. Amer. Math. Soc. **365** (2013), 1219-1249

MSC (2010):
Primary 06F05; Secondary 08B15, 03B47, 03G10, 03F05

Published electronically:
October 31, 2012

MathSciNet review:
3003263

Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: Residuated frames provide relational semantics for substructural logics and are a natural generalization of Kripke frames in intuitionistic and modal logic, and of phase spaces in linear logic. We explore the connection between Gentzen systems and residuated frames and illustrate how frames provide a uniform treatment for semantic proofs of cut-elimination, the finite model property and the finite embeddability property, which imply the decidability of the equational/universal theories of the associated residuated lattice-ordered groupoids. In particular these techniques allow us to prove that the variety of involutive FL-algebras and several related varieties have the finite model property.

**[1]**V. Michele Abrusci,*Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic*, J. Symbolic Logic**56**(1991), no. 4, 1403–1451. MR**1136467**, 10.2307/2275485**[2]**Francesco Belardinelli, Peter Jipsen, and Hiroakira Ono,*Algebraic aspects of cut elimination*, Studia Logica**77**(2004), no. 2, 209–240. MR**2080239**, 10.1023/B:STUD.0000037127.15182.2a**[3]**W. J. Blok and C. J. van Alten,*The finite embeddability property for residuated lattices, pocrims and BCK-algebras*, Algebra Universalis**48**(2002), no. 3, 253–271. MR**1954775**, 10.1007/s000120200000**[4]**W. J. Blok and C. J. Van Alten,*On the finite embeddability property for residuated ordered groupoids*, Trans. Amer. Math. Soc.**357**(2005), no. 10, 4141–4157. MR**2159703**, 10.1090/S0002-9947-04-03654-2**[5]**Kevin Kendall Blount,*On the structure of residuated lattices*, ProQuest LLC, Ann Arbor, MI, 1999. Thesis (Ph.D.)–Vanderbilt University. MR**2700270****[6]**Kevin Blount and Constantine Tsinakis,*The structure of residuated lattices*, Internat. J. Algebra Comput.**13**(2003), no. 4, 437–461. MR**2022118**, 10.1142/S0218196703001511**[7]**Wojciech Buszkowski,*Interpolation and FEP for logics of residuated algebras*, Log. J. of IGPL. doi:10.1093/jigpal/jzp094.**[8]**Agatha Ciabattoni, Nikolaos Galatos, and Kazushige Terui,*From axioms to analytic rules in nonclassical logics*, Proceedings of LICS'08 (2008), 229-240.**[9]**Agatha Ciabattoni, Nikolaos Galatos, and Kazushige Terui,*The expressive power of structural rules for FL*. submitted.**[10]**J. Michael Dunn, Mai Gehrke, and Alessandra Palmigiano,*Canonical extensions and relational completeness of some substructural logics*, J. Symbolic Logic**70**(2005), no. 3, 713–740. MR**2155263**, 10.2178/jsl/1122038911**[11]**Maciej Farulewski,*Finite embeddability property for residuated groupoids*, Rep. Math. Logic**43**(2008), 25–42. MR**2417720****[12]**Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono,*Residuated lattices: an algebraic glimpse at substructural logics*, Studies in Logic and the Foundations of Mathematics, vol. 151, Elsevier B. V., Amsterdam, 2007. MR**2531579****[13]**Nikolaos Galatos and Hiroakira Ono,*Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL*, Studia Logica**83**(2006), no. 1-3, 279–308. MR**2250112**, 10.1007/s11225-006-8305-5**[14]**Nikolaos Galatos and Hiroakira Ono,*Cut elimination and strong separation for substructural logics: an algebraic approach*, Ann. Pure Appl. Logic**161**(2010), no. 9, 1097–1133. MR**2646809**, 10.1016/j.apal.2010.01.003**[15]**Nikolaos Galatos and Constantine Tsinakis,*Generalized MV-algebras*, J. Algebra**283**(2005), no. 1, 254–291. MR**2102083**, 10.1016/j.jalgebra.2004.07.002**[16]**Bernhard Ganter and Rudolf Wille,*Formal concept analysis*, Springer-Verlag, Berlin, 1999. Mathematical foundations; Translated from the 1996 German original by Cornelia Franzke. MR**1707295****[17]**Mai Gehrke,*Generalized Kripke frames*, Studia Logica**84**(2006), no. 2, 241–275. MR**2284541**, 10.1007/s11225-006-9008-7**[18]**P. Jipsen and C. Tsinakis,*A survey of residuated lattices*, Ordered algebraic structures, Dev. Math., vol. 7, Kluwer Acad. Publ., Dordrecht, 2002, pp. 19–56. MR**2083033**, 10.1007/978-1-4757-3627-4_3**[19]**Mitsuhiro Okada and Kazushige Terui,*The finite model property for various fragments of intuitionistic linear logic*, J. Symbolic Logic**64**(1999), no. 2, 790–802. MR**1777787**, 10.2307/2586501**[20]**Hiroakira Ono and Yuichi Komori,*Logics without the contraction rule*, J. Symbolic Logic**50**(1985), no. 1, 169–201. MR**780534**, 10.2307/2273798**[21]**Kimmo I. Rosenthal,*Quantales and their applications*, Pitman Research Notes in Mathematics Series, vol. 234, Longman Scientific & Technical, Harlow; copublished in the United States with John Wiley & Sons, Inc., New York, 1990. MR**1088258****[22]**Jürgen Schmidt and Constantine Tsinakis,*Relative pseudo-complements, join-extensions, and meet-retractions*, Math. Z.**157**(1977), no. 3, 271–284. MR**0472618****[23]**Kazushige Terui,*Which structural rules admit cut elimination? An algebraic criterion*, J. Symbolic Logic**72**(2007), no. 3, 738–754. MR**2354898**, 10.2178/jsl/1191333839**[24]**C. J. van Alten,*The finite model property for knotted extensions of propositional linear logic*, J. Symbolic Logic**70**(2005), no. 1, 84–98. MR**2119124**, 10.2178/jsl/1107298511**[25]**Clint J. van Alten and James G. Raftery,*Rule separation and embedding theorems for logics without weakening*, Studia Logica**76**(2004), no. 2, 241–274. MR**2072985**, 10.1023/B:STUD.0000032087.02579.e2**[26]**Annika M. Wille,*A Gentzen system for involutive residuated lattices*, Algebra Universalis**54**(2005), no. 4, 449–463. MR**2218856**, 10.1007/s00012-005-1957-6**[27]**David N. Yetter,*Quantales and (noncommutative) linear logic*, J. Symbolic Logic**55**(1990), no. 1, 41–64. MR**1043543**, 10.2307/2274953

Retrieve articles in *Transactions of the American Mathematical Society*
with MSC (2010):
06F05,
08B15,
03B47,
03G10,
03F05

Retrieve articles in all journals with MSC (2010): 06F05, 08B15, 03B47, 03G10, 03F05

Additional Information

**Nikolaos Galatos**

Affiliation:
Department of Mathematics, University of Denver, 2360 S. Gaylord Street, Denver, Colorado 80208

Email:
ngalatos@du.edu

**Peter Jipsen**

Affiliation:
Mathematics and CS, Faculty of Mathematics, School of Computer Science, Chapman University, One University Drive, Orange, California 92866

Email:
jipsen@chapman.edu

DOI:
http://dx.doi.org/10.1090/S0002-9947-2012-05573-5

Keywords:
Substructural logic,
Gentzen system,
residuated lattice,
residuated frame,
cut elimination,
decidability,
finite model property,
finite embeddability property

Received by editor(s):
August 29, 2008

Received by editor(s) in revised form:
February 22, 2011

Published electronically:
October 31, 2012

Article copyright:
© Copyright 2012
American Mathematical Society

The copyright for this article reverts to public domain 28 years after publication.