Download PDF - One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and ComplexityCC BY-NC-ND: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0, Opens in new tab

ArticleOriginal scientific text

Title

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

Authors 1

Affiliations

  1. Adam Mickiewicz University, Faculty of Mathematics and Computer Science

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.

Keywords

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

Bibliography

  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
  2. A. Bastenhof, Categorial Symmetry, Ph.D. thesis, Utrecht University (2013).
  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
  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
  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
  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
  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
  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
  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
  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
  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.
Bulletin of the Section of Logic
2021/50/1
Export to PBN, Opens in new tab
Pages:
55-80
Main language of publication
English
Published
2020-11-13
Published online
2020-11-13

DOI: 10.18778/0138-0680.2020.25

Exact and natural sciences