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ń 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. Płaczek, 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. Płaczek, 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