Residuated frames with applications to decidability

Galatos, Nikolaos; Jipsen, Peter

doi:10.1090/S0002-9947-2012-05573-5

Residuated frames with applications to decidability
HTML articles powered by AMS MathViewer

by Nikolaos Galatos and Peter Jipsen PDF

Trans. Amer. Math. Soc. 365 (2013), 1219-1249 Request permission

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.

References

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, DOI 10.2307/2275485
Francesco Belardinelli, Peter Jipsen, and Hiroakira Ono, Algebraic aspects of cut elimination, Studia Logica 77 (2004), no. 2, 209–240. MR 2080239, DOI 10.1023/B:STUD.0000037127.15182.2a
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, DOI 10.1007/s000120200000
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, DOI 10.1090/S0002-9947-04-03654-2
Kevin Kendall Blount, On the structure of residuated lattices, ProQuest LLC, Ann Arbor, MI, 1999. Thesis (Ph.D.)–Vanderbilt University. MR 2700270
Kevin Blount and Constantine Tsinakis, The structure of residuated lattices, Internat. J. Algebra Comput. 13 (2003), no. 4, 437–461. MR 2022118, DOI 10.1142/S0218196703001511
Wojciech Buszkowski, Interpolation and FEP for logics of residuated algebras, Log. J. of IGPL. doi:10.1093/jigpal/jzp094.
Agatha Ciabattoni, Nikolaos Galatos, and Kazushige Terui, From axioms to analytic rules in nonclassical logics, Proceedings of LICS’08 (2008), 229–240.
Agatha Ciabattoni, Nikolaos Galatos, and Kazushige Terui, The expressive power of structural rules for FL. submitted.
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, DOI 10.2178/jsl/1122038911
Maciej Farulewski, Finite embeddability property for residuated groupoids, Rep. Math. Logic 43 (2008), 25–42. MR 2417720
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
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, DOI 10.1007/s11225-006-8305-5
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, DOI 10.1016/j.apal.2010.01.003
Nikolaos Galatos and Constantine Tsinakis, Generalized MV-algebras, J. Algebra 283 (2005), no. 1, 254–291. MR 2102083, DOI 10.1016/j.jalgebra.2004.07.002
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, DOI 10.1007/978-3-642-59830-2
Mai Gehrke, Generalized Kripke frames, Studia Logica 84 (2006), no. 2, 241–275. MR 2284541, DOI 10.1007/s11225-006-9008-7
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, DOI 10.1007/978-1-4757-3627-4_{3}
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, DOI 10.2307/2586501
Hiroakira Ono and Yuichi Komori, Logics without the contraction rule, J. Symbolic Logic 50 (1985), no. 1, 169–201. MR 780534, DOI 10.2307/2273798
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
Jürgen Schmidt and Constantine Tsinakis, Relative pseudo-complements, join-extensions, and meet-retractions, Math. Z. 157 (1977), no. 3, 271–284. MR 472618, DOI 10.1007/BF01214357
Kazushige Terui, Which structural rules admit cut elimination? An algebraic criterion, J. Symbolic Logic 72 (2007), no. 3, 738–754. MR 2354898, DOI 10.2178/jsl/1191333839
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, DOI 10.2178/jsl/1107298511
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, DOI 10.1023/B:STUD.0000032087.02579.e2
Annika M. Wille, A Gentzen system for involutive residuated lattices, Algebra Universalis 54 (2005), no. 4, 449–463. MR 2218856, DOI 10.1007/s00012-005-1957-6
David N. Yetter, Quantales and (noncommutative) linear logic, J. Symbolic Logic 55 (1990), no. 1, 41–64. MR 1043543, DOI 10.2307/2274953