One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

Paweł Płaczek

doi:10.18778/0138-0680.2020.25

Authors

Paweł Płaczek Adam Mickiewicz University, Faculty of Mathematics and Computer Science Uniwersytetu Poznanskiego 4, 61-614 Poznan, Poland https://orcid.org/0000-0002-8086-3150

DOI:

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

Keywords:

Substructural logic, Lambek calculus, nonassociative linear logic, sequent system, PTime complexity

Abstract

Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.

References

[1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, The Journal of Symbolic Logic, vol. 56(4) (1991), pp. 1403–1451, DOI: http://dx.doi.org/10.2307/2275485
Google Scholar DOI: https://doi.org/10.2307/2275485

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

[3] W. Buszkowski, On classical nonassociative Lambek calculus, [in:] M. Amblard, P. de Groote, S. Pogodalla, C. Retoré (eds.), Logical Aspects of Computational Linguistics, vol. 10054 of Lecture Notes in Computer Science, Springer (2016), pp. 68–84, DOI: http://dx.doi.org/10.1007/978-3-662-53826-5_5
Google Scholar DOI: https://doi.org/10.1007/978-3-662-53826-5_5

[4] W. Buszkowski, Involutive nonassociative Lambek calculus: Sequent systems and complexity, Bulletin of the Section of Logic, vol. 46(1/2) (2017), DOI: http://dx.doi.org/10.18778/0138-0680.46.1.2.07
Google Scholar DOI: https://doi.org/10.18778/0138-0680.46.1.2.07

[5] P. De Groote, F. Lamarche, Classical non-associative Lambek calculus, Studia Logica, vol. 71(3) (2002), pp. 355–388, DOI: http://dx.doi.org/10.1023/A:1020520915016
Google Scholar DOI: https://doi.org/10.1023/A:1020520915016

[6] N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the American Mathematical Society, vol. 365(3) (2013), pp. 1219–1249, URL: https://www.jstor.org/stable/23513444
Google Scholar DOI: https://doi.org/10.1090/S0002-9947-2012-05573-5

[7] N. Galatos, H. Ono, Cut elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic, vol. 161(9) (2010), pp. 1097–1133, DOI: http://dx.doi.org/0.1016/j.apal.2010.01.003
Google Scholar DOI: https://doi.org/10.1016/j.apal.2010.01.003

[8] J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–101, DOI: http://dx.doi.org/10.1016/0304-3975(87)90045-4
Google Scholar DOI: https://doi.org/10.1016/0304-3975(87)90045-4

[9] 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, DOI: http://dx.doi.org/10.1090/psapm/012/9972
Google Scholar DOI: https://doi.org/10.1090/psapm/012/9972

[10] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae, vol. 22(1, 2) (1995), pp. 53–67, DOI: http://dx.doi.org/10.3233/FI-1995-22123
Google Scholar DOI: https://doi.org/10.3233/FI-1995-22123

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