Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

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
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.

References [Enhancements On Off] (What's this?)

  • [1] V. M. 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)
  • [2] F. Belardinelli, Peter Jipsen, and Hiroakira Ono, Algebraic aspects of cut elimination, Studia Logica 77 (2004), 209-240. MR 2080239 (2005d:03039)
  • [3] Willem J. Blok and Clint J. van Alten, The finite embeddability property for residuated lattices, pocrims and BCK-algebras, Algebra Universalis 48 (2002), 253-271. MR 1954775 (2003j:06017)
  • [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)
  • [5] Kevin Blount, On the structure of residuated lattices, Ph.D. thesis, Vanderbilt University, Nashville, Tennessee, 1999. MR 2700270
  • [6] Kevin Blount and Constantine Tsinakis, The structure of residuated lattices, International Journal of Algebra and Computation 13 (2003), no. 4, 437-461. MR 2022118 (2005b:06011)
  • [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)
  • [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, 2007. MR 2531579 (2011d:03033)
  • [13] Nikolaos Galatos and Hiroakira Ono, Algebraization, parametrized local deduction theorem and interpolation for substructural logics over $ \mathbf {FL}$, Studia Logica 83 (2006), 279-308. MR 2250112 (2007d:03035)
  • [14] Nikolaos Galatos and Hiroakira Ono, Cut elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic 161 (2010), 1097-1133. MR 2646809
  • [15] Nikolaos Galatos and Constantine Tsinakis, Generalized MV-algebras, J. of Algebra 283 (2005), 254-291. MR 2102083 (2005h:06012)
  • [16] Bernhard Ganter and Rudolf Wille, Formal Concept Analysis: Mathematical Foundations, Springer-Verlag, Berlin, 1998. MR 1707295 (2000i:06002b)
  • [17] Mai Gehrke, Generalized Kripke frames, Studia Logica 84 (2006), 241-275. MR 2284541 (2007j:03031)
  • [18] Peter Jipsen and Constantine Tsinakis, A survey of residuated lattices, Ordered Algebraic Structures, Kluwer, 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, Journal of Symbolic Logic 64 (1999), 790-802. MR 1777787 (2002g:03043)
  • [20] Hiroakira Ono and Yuichi Komori, Logics without the contraction rule, Journal of Symbolic Logic 50 (1985), 169-201. MR 780534 (87a:03053)
  • [21] K.I. Rosenthal, Quantales and Their Applications, Pitman Research Notes in Mathematics, vol. 234, Longman, 1990. MR 1088258 (92e:06028)
  • [22] J. Schmidt and C. Tsinakis, Relative pseudo-complements, join-extensions and meet-retractions, Mathematische Zeitschrift 157 (1977), 271-284. MR 0472618 (57:12314)
  • [23] Kazushige Terui, Which Structural Rules Admit Cut Elimination? An Algebraic Criterion, Journal of Symbolic Logic 72 (2007), no. 3, 738-754. MR 2354898 (2008h:03063)
  • [24] C.J. van Alten, The finite model property for knotted extensions of propositional linear logic, Journal of Symbolic Logic 70 (2005), no. 1, 84-98. MR 2119124 (2005m:03127)
  • [25] C.J. van Alten and J.G. Raftery, Rule Separation and Embedding Theorems for Logics Without Weakening, Studia Logica 76 (2004), 241-274. MR 2072985 (2005e:03132)
  • [26] Annika M. Wille, A Gentzen system for involutive residuated lattices, Algebra Universalis 54 (2005), no. 4, 449-463. MR 2218856 (2007j:03092)
  • [27] David N. Yetter, Quantales and (noncommutative) linear logic, J. Symbolic Logic 55 (1990), no. 1, 41-64. MR 1043543 (91f:03052)

Similar Articles

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

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

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.

American Mathematical Society