{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T20:50:34Z","timestamp":1769979034683,"version":"3.49.0"},"reference-count":32,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"Russian Academic Excellence Project","award":["5-100"],"award-info":[{"award-number":["5-100"]}]},{"name":"Young Russian Scientists and Leading Scientific Schools of Russia"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called \u2018Lambek\u2019s restriction\u2019, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek\u2019s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek\u2019s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek\u2019s restriction and cut elimination and another system with Lambek\u2019s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek\u2019s restriction is folklore and known to be undecidable.<\/jats:p>","DOI":"10.1093\/logcom\/exaa010","type":"journal-article","created":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T12:10:48Z","timestamp":1578485448000},"page":"239-256","source":"Crossref","is-referenced-by-count":6,"title":["Reconciling Lambek\u2019s restriction, cut-elimination and substitution in the presence of exponential modalities"],"prefix":"10.1093","volume":"30","author":[{"given":"Max","family":"Kanovich","sequence":"first","affiliation":[{"name":"University College London, Computer Science Department, London WC1E 6BT, UK and National Research University Higher School of Economics, Faculty of Computer Science, Moscow 109028, Russia"}]},{"given":"Stepan","family":"Kuznetsov","sequence":"first","affiliation":[{"name":"Steklov Mathematical Institute of the RAS, Department of Mathematical Logic, Moscow 119991, Russia and National Research University Higher School of Economics, Faculty of Computer Science, Moscow 109028, Russia"}]},{"given":"Andre","family":"Scedrov","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Department of Mathematics, Philadelphia 19104, USA and National Research University Higher School of Economics, Faculty of Computer Science, Moscow 109028, Russia"}]}],"member":"286","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"key":"2020040702351790600_ref1","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1002\/malq.19900360103","article-title":"A comparison between Lambek syntactic calculus and intuitionistic linear logic","volume":"36","author":"Abrusci","year":"1990","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik (Mathematical Logic Quarterly)"},{"key":"2020040702351790600_ref2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"2020040702351790600_ref3","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1002\/malq.19820283308","article-title":"Some decision problems in the theory of syntactic categories","volume":"28","author":"Buszkowski","year":"1982","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik (Mathematical Logic Quarterly)"},{"key":"2020040702351790600_ref4","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6945.001.0001","volume-title":"Type-Logical Semantics","author":"Carpenter","year":"1998"},{"key":"2020040702351790600_ref5","first-page":"95","article-title":"On the expressive power of the Lambek calculus extended with a structural modality","volume-title":"Language and Grammar. Studies in Mathematical Linguistics and Natural Language, vol. 168 of CSLI Lecture Notes","author":"de Groote","year":"2005"},{"key":"2020040702351790600_ref6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50,","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2020040702351790600_ref7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1006\/inco.1998.2700","article-title":"Light linear logic","volume":"143,","author":"Girard","year":"1998","journal-title":"Information and Computation"},{"key":"2020040702351790600_ref8","article-title":"Studied Flexibility. PhD Thesis, Institute for Logic","volume-title":"Language and Computation","author":"Hendriks","year":"1993,"},{"key":"2020040702351790600_ref9","article-title":"Lambek calculus: recognizing power and complexity","volume-title":"JFAK. Essays Dedicated to Johan van Benthem to the Occasion of His 50th Birthday","author":"Kanazawa","year":"1999"},{"key":"2020040702351790600_ref10","volume-title":"The expressive power of modalized purely implicational calculi","author":"Kanovich","year":"1993"},{"key":"2020040702351790600_ref11","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1017\/S0960129516000049","article-title":"The undecidability theorem for the Horn-like fragment of linear logic (revisited)","volume":"26,","author":"Kanovich","year":"2016","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020040702351790600_ref12","first-page":"228","article-title":"A logical framework with commutative and non-commutative subexponentials","volume-title":"Automated Reasoning (IJCAR 2018), vol. 10900 of Lecture Notes in Artificial Intelligence","author":"Kanovich","year":"2018"},{"key":"2020040702351790600_ref13","first-page":"1217","volume-title":"Subexponentials in non-commutative linear logic","author":"Kanovich","year":"2019"},{"key":"2020040702351790600_ref14","article-title":"Lambek calculus enriched with multiplexing","volume-title":"Mal\u2019tsev Meeting. Collection of Abstracts, Novosibirsk","author":"Kanovich","year":"2018"},{"key":"2020040702351790600_ref15","first-page":"94","article-title":"Simulating linear logic in 1-only linear logic. CNRS","author":"Kanovich","year":"1994","journal-title":"Laboratoire de Math\u00e9matiques Discr\u00e9tes. Pr\u00e9tirage n"},{"issue":"LICS 1995","key":"2020040702351790600_ref16","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1109\/LICS.1995.523282","article-title":"The complexity of neutrals in linear logic","author":"Kanovich","year":"1995","journal-title":"Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science"},{"key":"2020040702351790600_ref17","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1093\/jigpal\/jzr031","article-title":"Lambek grammars with one division and one primitive type","volume":"20,","author":"Kuznetsov","year":"2012","journal-title":"Logic Journal of the IGPL"},{"key":"2020040702351790600_ref18","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","article-title":"Soft linear logic and polynomial time","volume":"318,","author":"Lafont","year":"2004","journal-title":"Theoretical Computer Science"},{"key":"2020040702351790600_ref19","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1080\/00029890.1958.11989160","article-title":"The mathematics of sentence structure","volume":"65","author":"Lambek","year":"1958","journal-title":"American Mathematical Monthly"},{"key":"2020040702351790600_ref20","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1090\/psapm\/012\/9972","article-title":"On the calculus of syntactic types","volume-title":"Structure of Language and Its Mathematical Aspects, vol. 12 of Proceedings of Symposia in Applied Mathematics","author":"Lambek","year":"1961"},{"key":"2020040702351790600_ref21","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0168-0072(92)90075-B","article-title":"Decision problems for propositional linear logic","volume":"56,","author":"Lincoln","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702351790600_ref22","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/S0304-3975(99)00053-5","article-title":"Polynomial equivalence among systems $\\textrm{LLNC}$, LLNC$_a$ and LLNC$_o$","volume":"227,","author":"M\u00e9tayer","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"2020040702351790600_ref23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-31555-8","article-title":"The logic of categorial grammars","volume-title":"A Deductive Account of Natural Language Syntax and Semantics, vol. 6850 of Lecture Notes in Computer Science","author":"Moot","year":"2012"},{"key":"2020040702351790600_ref24","volume-title":"Categorial Grammar: Logical Syntax, Semantics, and Processing","author":"Morrill","year":"2011"},{"key":"2020040702351790600_ref25","first-page":"507","article-title":"Focusing in linear meta-logic","volume-title":"Automated Reasoning (IJCAR 2008), vol. 5195 of Lecture Notes in Artificial Intelligence","author":"Nigam","year":"2008"},{"key":"2020040702351790600_ref26","first-page":"129","article-title":"Algorithmic specifications in linear logic with subexponentials","volume-title":"Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP \u201909)","author":"Nigam","year":"2009"},{"key":"2020040702351790600_ref27","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1109\/LICS.1993.287565","article-title":"Lambek grammars are context-free","volume-title":"Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)","author":"Pentus","year":"1993"},{"key":"2020040702351790600_ref28","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1016\/j.tcs.2006.03.018","article-title":"Lambek calculus is NP-complete","volume":"357,","author":"Pentus","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"2020040702351790600_ref29","first-page":"273","article-title":"Lambek grammars with one division are decidable in polynomial time","volume-title":"Computer Science \u2014 Theory and Applications (CSR 2008), vol. 5010 of Lecture Notes in Computer Science","author":"Savateev","year":"2008"},{"key":"2020040702351790600_ref30","article-title":"Algorithmic Complexity of Fragments of the Lambek Calculus. PhD Thesis","author":"Savateev","year":"2009"},{"key":"2020040702351790600_ref31","first-page":"380","article-title":"Product-free Lambek calculus is NP-complete","author":"Savateev","year":"2009"},{"key":"2020040702351790600_ref32","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2307\/2274953","article-title":"Quantales and (noncommutative) linear logic","volume":"55,","author":"Yetter","year":"1990","journal-title":"Journal of Symbolic Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/239\/33016538\/exaa010.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/239\/33016538\/exaa010.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T06:35:37Z","timestamp":1586241337000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/239\/5739319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":32,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,2,20]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa010","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}