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

Paweł Płaczek

Bulletin of the Section of Logic (2021)

  • Volume: 50, Issue: 1, page 55-80
  • ISSN: 0138-0680

Abstract

top
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.

How to cite

top

Paweł Płaczek. "One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity." Bulletin of the Section of Logic 50.1 (2021): 55-80. <http://eudml.org/doc/296788>.

@article{PawełPłaczek2021,
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.},
author = {Paweł Płaczek},
journal = {Bulletin of the Section of Logic},
keywords = {Substructural logic; Lambek calculus; nonassociative linear logic; sequent system; PTime complexity},
language = {eng},
number = {1},
pages = {55-80},
title = {One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity},
url = {http://eudml.org/doc/296788},
volume = {50},
year = {2021},
}

TY - JOUR
AU - Paweł Płaczek
TI - One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
JO - Bulletin of the Section of Logic
PY - 2021
VL - 50
IS - 1
SP - 55
EP - 80
AB - 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.
LA - eng
KW - Substructural logic; Lambek calculus; nonassociative linear logic; sequent system; PTime complexity
UR - http://eudml.org/doc/296788
ER -

References

top
  1. [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. [2] A. Bastenhof, Categorial Symmetry, Ph.D. thesis, Utrecht University (2013). 
  3. [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. [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. [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. [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. [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. [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. [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. [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. [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. 

NotesEmbed ?

top

You must be logged in to post comments.