Complexity of Nonassociative Lambek Calculus with Classical and Intuitionistic Logic

Paweł Płaczek

doi:10.18778/0138-0680.2025.18

Authors

Paweł Płaczek WSB Merito University in Poznań, Faculty of Finance and Banking, Poland https://orcid.org/0000-0002-8086-3150

DOI:

https://doi.org/10.18778/0138-0680.2025.18

Keywords:

Lambek calculus, nonassociative logics, non-commutative logics, substructural logics, consequence relation, nonlogical axioms

Abstract

The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction (FNL) makes the consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof, that we can merge classical logic with NL (i.e. BFNL) and intuitionistic logic with NL (i.e. HFNL), and still consequence relations are decidable in exponential time.

References

W. Buszkowski, Lambek calculus with nonlogical axioms, [in:] C. Casadio, P. J. Scott, R. A. G. Seely (eds.), Language and Grammar. Studies in Mathematical Linguistics and Natural Language (2005), pp. 77–93.
Google Scholar

W. Buszkowski, Lambek Calculus with Classical Logic, [in:] R. Loukanova (ed.), Natural Language Processing in Artificial Intelligence—NLPinAI 2020, Springer International Publishing (2021), pp. 1–36, DOI: https://doi.org/10.1007/978-3-030-63787-3_1.
Google Scholar

K. Chvalovskỳ, Undecidability of consequence relation in full non-associative Lambek calculus, Journal of Symbolic Logic, vol. 80(2) (2015), pp. 567––586, DOI: https://doi.org/10.1017/jsl.2014.39.
Google Scholar

N. Galatos, P. Jipsen, Distributive residuated frames and generalized bunched implication algebras, Algebra universalis, vol. 78(3) (2017), pp. 303–336, DOI: https://doi.org/10.1007/s00012-017-0456-x.
Google Scholar

J. Lambek, The mathematics of sentence structure, The American Mathematical Monthly, vol. 65(3) (1958), pp. 154–170.
Google Scholar

J. Lambek, On the calculus of syntactic types, [in:] R. Jakobson (ed.), Structure of Language and Its Mathematical Aspects, vol. 12, Providence, RI: American Mathematical Society (1961), pp. 166–178.
Google Scholar

M. Pentus, Lambek calculus is NP-complete, Theoretical Computer Science, vol. 357(1) (2006), pp. 186–201, DOI: https://doi.org/10.1016/j.tcs.2006.03.018.
Google Scholar

P. Płaczek, Complexity of Nonassociative Lambek Calculus with classical logic, [in:] A. Indrzejczak, M. Zawidzki (eds.), Proceedings of the 11th International Conference on Non-Classical Logics. Theory and Applications, vol. 415 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2024), pp. 150–164, DOI: https://doi.org/10.4204/eptcs.415.15.
Google Scholar

D. Shkatov, C. J. Van Alten, Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids., Algebra Universalis, vol. 80(3) (2019), DOI: https://doi.org/10.1007/s00012-019-0609-1.
Google Scholar

C. J. van Alten, Partial algebras and complexity of satisfiability and universal theory for distributive lattices, boolean algebras and Heyting algebras, Theoretical Computer Science, vol. 501 (2013), pp. 82–92, DOI: https://doi.org/10.1016/j.tcs.2013.05.012.
Google Scholar