Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

Wojciech Buszkowski

doi:10.18778/0138-0680.46.1.2.07

Authors

Wojciech Buszkowski Adam Mickiewicz University, Faculty of Mathematics and Computer Science, Poznań, Poland

DOI:

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

Keywords:

nonassociative Lambek calculus, linear logic, sequent system, cut elimination, PTIME complexity

Abstract

In [5] we study Nonassociative Lambek Calculus (NL) augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus (CNL). Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

References

[1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, Journal of Symbolic Logic 56 (1991), pp. 1403–1451.
Google Scholar

[2] A. Bastenhof, Categorial Symmetry, Ph.D. Thesis, University of Utrecht (2013).
Google Scholar

[3] W. Buszkowski, Lambek Calculus with Nonlogical Axioms, [in:] Casadio, C., Scott, P.J. and Seely, R.A.S., Language and Grammar. Studies in Mathematical Linguistics and Natural Language. CSLI Lecture Notes 168 (2005), pp. 77–93.
Google Scholar

[4] W. Buszkowski, An Interpretation of Full Lambek Calculus in Its Variant without Empty Antecedents of Sequents, [in:] Asher, N. and Soloviev, S. (eds.), Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol. 8535 (2014), Springer, pp. 30–43.
Google Scholar

[5] W. Buszkowski, On Classical Nonassociative Lambek Calculus, [in:] Amblard, M,, de Groote, Ph., Pogodalla, S., and Retoré, C. (eds.), Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol. 10054 (2016), Springer, pp. 68–84.
Google Scholar

[6] W. Buszkowski, Phase Spaces for Involutive Nonassociative Lambek Calculus, [in:] Loukanova, R. and Liefke, K. (eds.), Proc. Logic and Algorithms in Computational Linguistics (LACompLing 2017), Stockholm University, (2017), pp. 21–45.
Google Scholar

[7] N. Galatos and P. Jipsen, Residuated frames with applications to decidability, Transactions of American Mathematical Society 365 (2013), pp. 1219–1249.
Google Scholar

[8] N. Galatos, P. Jipsen, T. Kowalski and H. Ono, Residuated Lattices. An Algebraic Glimpse at Substructural Logics, Elsevier (2007).
Google Scholar

[9] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987), pp. 1–102.
Google Scholar

[10] Ph. de Groote and F. Lamarche, Classical Non-Associative Lambek Calculus, Studia Logica 71/3 (2002), pp. 355–388.
Google Scholar

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

[12] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae 22 (1995), pp. 53–67.
Google Scholar

[13] J. Lambek, Some lattice models of bilinear logic, Algebra Universalis 34 (1995), pp. 541–550.
Google Scholar

[14] G.Malinowski,Many-valued Logics, Oxford Logic Guides 25, The Clarendon Press, Oxford University Press, 1993.
Google Scholar

[15] M. Okada and K. Terui, The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic 64 (1999), pp. 790–802.
Google Scholar

[16] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201.
Google Scholar

[17] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201.
Google Scholar