Residuated frames with applications to decidability

Galatos, Nikolaos; Jipsen, Peter

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

			Journals Home Search Author Info Subscribe Tech Support My Subscriptions Browser Compatibility Info Help
ISSN 1088-6850(online) ISSN 0002-9947(print)

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
Posted: October 31, 2012
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 (93a:03060), http://dx.doi.org/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 (2005d:03039), http://dx.doi.org/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 (2003j:06017), http://dx.doi.org/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 (2007b:06019), http://dx.doi.org/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 (2005b:06011), http://dx.doi.org/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 (2006f:06012), http://dx.doi.org/10.2178/jsl/1122038911
[11] Maciej Farulewski, Finite embeddability property for residuated groupoids, Rep. Math. Logic 43 (2008), 25–42. MR 2417720 (2009e:03066)
[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 (2011d:03033)
[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 (2007d:03035), http://dx.doi.org/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 (2011i:03019), http://dx.doi.org/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 (2005h:06012), http://dx.doi.org/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 (2000i:06002b)
[17] Mai Gehrke, Generalized Kripke frames, Studia Logica 84 (2006), no. 2, 241–275. MR 2284541 (2007j:03031), http://dx.doi.org/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 (2005e:06024)
[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 (2002g:03043), http://dx.doi.org/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 (87a:03053), http://dx.doi.org/10.2307/2273798
[21] Kimmo I. Rosenthal, Quantales and their applications, Pitman Research Notes in Mathematics Series, vol. 234, Longman Scientific & Technical, Harlow, 1990. MR 1088258 (92e:06028)
[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 (57 #12314)
[23] Kazushige Terui, Which structural rules admit cut elimination? An algebraic criterion, J. Symbolic Logic 72 (2007), no. 3, 738–754. MR 2354898 (2008h:03063), http://dx.doi.org/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 (2005m:03127), http://dx.doi.org/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 (2005e:03132), http://dx.doi.org/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 (2007j:03092), http://dx.doi.org/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 (91f:03052), http://dx.doi.org/10.2307/2274953

	Publications Meetings The Profession Membership Programs Math Samplings Policy & Advocacy In the News About the AMS
\|