Sequent Systems for Consequence Relations of Cyclic Linear Logics

Paweł Płaczek

doi:10.18778/0138-0680.2024.06

Authors

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

DOI:

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

Keywords:

linear logic, Lambek calculus, nonassociative logics, noncommutative logics, substructural logics, consequence relation, nonlogical axioms, conservativeness

Abstract

Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity and nonassociativity. We introduce a sequent system for CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL.

References

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: https://doi.org/10.2307/2275485
Google Scholar DOI: https://doi.org/10.2307/2275485

V. M. Abrusci, Classical Conservative Extensions of Lambek Calculus, Studia Logica, vol. 71(3) (2002), pp. 277–314, DOI: https://doi.org/10.1023/A:1020560613199
Google Scholar DOI: https://doi.org/10.1023/A:1020560613199

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

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, Berlin–Heidelberg (2016), pp. 68–84, DOI: https://doi.org/10.1007/978-3-662-53826-5_5
Google Scholar DOI: https://doi.org/10.1007/978-3-662-53826-5_5

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

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

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

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

Z. Lin, Modal nonassociative Lambek calculus with assumptions: complexity and context-freeness, [in:] Language and Automata Theory and Applications: 4th International Conference, LATA 2010, Trier, Germany, May 24–28, 2010. Proceedings 4, vol. 6031 of Lecture Notes in Computer Science, Springer (2010), pp. 414–425, DOI: https://doi.org/10.1007/978-3-642-13089-2_35
Google Scholar DOI: https://doi.org/10.1007/978-3-642-13089-2_35

P. Plączek, One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity, Bulletin of the Section of Logic, vol. 50(1) (2020), pp. 55–80, DOI: https://doi.org/10.18778/0138-0680.2020.25
Google Scholar DOI: https://doi.org/10.18778/0138-0680.2020.25

P. Plączek, Extensions of Lambek calculi: Sequent systems, conservativeness and computational complexity, Ph.D. thesis, Adam Mickiewicz University, Poznań (2021).
Google Scholar

D. N. Yetter, Quantales and (Noncommutative) Linear Logic, The Journal of Symbolic Logic, vol. 55(1) (1990), pp. 41–64, DOI: https://doi.org/10.2307/2274953
Google Scholar DOI: https://doi.org/10.2307/2274953