Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-26T08:47:51.305Z Has data issue: false hasContentIssue false
  • English
  • Français

FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE

Published online by Cambridge University Press:  10 May 2016

KAREL CHVALOVSKÝ  and
ROSTISLAV HORČÍK
KAREL CHVALOVSKÝ
Affiliation:
INSTITUTE OF COMPUTER SCIENCE ACADEMY OF SCIENCES OF THE CZECH REPUBLIC POD VODÁRENSKOU VĚŽÍ 2 182 07 PRAGUE 8, CZECH REPUBLICE-mail: [email protected]
ROSTISLAV HORČÍK
Affiliation:
INSTITUTE OF COMPUTER SCIENCE ACADEMY OF SCIENCES OF THE CZECH REPUBLIC POD VODÁRENSKOU VĚŽÍ 2 182 07 PRAGUE 8, CZECH REPUBLICE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We prove that the set of formulae provable in the full Lambek calculus with the structural rule of contraction is undecidable. In fact, we show that the positive fragment of this logic is undecidable.

Keywords

substructural logicfull Lambek calculuscontraction rulesquare-increasing residuated latticeequational theorydecidability
Type
Articles
Information
The Journal of Symbolic Logic , Volume 81 , Issue 2 , June 2016 , pp. 524 - 540
Copyright
Copyright © The Association for Symbolic Logic 2016 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Book, Ronald V. and Otto, Friedrich, String-rewriting systems, Springer, Berlin, 1993.Google Scholar
Chottin, Laurent, Strict deterministic languages and controlled rewriting systems , Automata, languages and programming (Maurer, Hermann A., editor), Lecture Notes in Computer Science, vol. 71, Springer, Berlin Heidelberg, 1979, pp. 104–117.CrossRefGoogle Scholar
Chvalovský, Karel, Undecidability of consequence relation in full non-associative Lambek calculus, this Journal, vol. 80 (2015), no. 2, pp. 567–586.Google Scholar
Ciabattoni, Agata, Galatos, Nikolaos, and Terui, Kazushige, Algebraic proof theory for substructural logics: Cut-elimination and completions . Annals of Pure and Applied Logic, vol. 163 (2012), no. 3, pp. 266–290.CrossRefGoogle Scholar
Davey, Brian A. and Priestley, Hilary A., Introduction to lattices and order, 2nd ed., Cambridge University Press, Cambridge, 2002.Google Scholar
Freese, Ralph, Free modular lattices . Transactions of the AMS, vol. 261 (1980), no. 1, pp. 81–91.Google Scholar
Galatos, Nikolaos and Jipsen, Peter, Residuated frames with applications to decidability . Transactions of the AMS, vol. 365 (2013), pp. 1219–1249.Google Scholar
Galatos, Nikolaos, Jipsen, Peter, Kowalski, Tomasz, and Ono, Hiroakira, Residuated lattices: An algebraic glimpse at substructural logics, Studies in Logic and the Foundations of Mathematics, vol. 151, Elsevier, Amsterdam, 2007.Google Scholar
Gentzen, Gerhard, Untersuchungen über das logische Schließen I . Mathematische Zeitschrift, vol. 39 (1935), no. 1, pp. 176–210.Google Scholar
Gentzen, Gerhard, Untersuchungen über das logische Schließen II . Mathematische Zeitschrift, vol. 39 (1935), no. 1, pp. 405–431.Google Scholar
Hopcroft, John E. and Ullman, Jeffrey D., Introduction to automata theory, languages and computation, 1st ed., Addison-Wesley, Reading, Massachusetts, 1979.Google Scholar
Horčík, Rostislav, Word problem for knotted residuated lattices . Journal of Pure and Applied Algebra, vol. 219 (2015), no. 5, pp. 1548–1563.Google Scholar
Jipsen, Peter and Tsinakis, Constantine, A survey of residuated lattices , Ordered algebraic structures (Martínez, Jorge, editor), Developments in Mathematics, vol. 7, Kluwer, Dordrecht, 2002.Google Scholar
Kanovich, Max I., The direct simulation of Minsky machines in linear logic , Advances in linear logic (Girard, Jean-Yves, Lafont, Yves, and Regnier, Laurent, editors), London Mathematical Society Lecture Note Series, vol. 222, Cambridge University Press, Cambridge, 1995.Google Scholar
Kharlampovich, Olga G. and Sapir, Mark V., Algorithmic problems in varieties . International Journal of Algebra and Computation, vol. 5 (1995), pp. 379–602.CrossRefGoogle Scholar
Kiriyama, Eiji and Ono, Hiroakira, The contraction rule and decision problems for logics without structural rules . Studia Logica, vol. 50 (1991), no. 2, pp. 299–319.CrossRefGoogle Scholar
Komori, Yuichi, Predicate logics without the structural rules . Studia Logica, vol. 45 (1986), no. 4, pp. 393–404.Google Scholar
Kripke, Saul Aaron, The problem of entailment, this Journal, vol. 24 (1959), p. 324, abstract.Google Scholar
Lafont, Yves, The undecidability of second order linear logic without exponentials, this Journal, vol. 61 (1996), no. 2, pp. 541–548.Google Scholar
Lincoln, Patrick, Mitchell, John, Scedrov, Andre, and Shankar, Natarajan, Decision problems for propositional linear logic . Annals of Pure and Applied Logic, vol. 56 (1992), no. 1–3, pp. 239–311.Google Scholar
Lothaire, M., Algebraic combinatorics on words , Encyclopedia of Mathematics and its Applications, vol. 90, Cambridge University Press, Cambridge, 2002.Google Scholar
Surarso, Bayu and Ono, Hiroakira, Cut elimination in noncommutative substructural logics . Reports on Mathematical Logic, vol. 30 (1996), pp. 13–29.Google Scholar
Urquhart, Alasdair, The undecidability of entailment and relevant implication, this Journal, vol. 49 (1984), no. 4, pp. 1059–1073.Google Scholar