Geodesic
Sequent Systems for Consequence Relations of Cyclic Linear Logics
Bulletin of the Section of Logic, Tome 53 (2024) no. 2, pp. 245-274

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: linear logic, Lambek calculus, nonassociative logics, noncommutative logics, substructural logics, consequence relation, nonlogical axioms, conservativeness 
Płaczek, Paweł. Sequent Systems for Consequence Relations of Cyclic Linear Logics. Bulletin of the Section of Logic, Tome 53 (2024) no. 2, pp. 245-274. http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a5/
@article{BSL_2024_53_2_a5,
     author = {P{\l}aczek, Pawe{\l}},
     title = {Sequent {Systems} for {Consequence} {Relations} of {Cyclic} {Linear} {Logics}},
     journal = {Bulletin of the Section of Logic},
     pages = {245--274},
     year = {2024},
     volume = {53},
     number = {2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a5/}
}
TY  - JOUR
AU  - Płaczek, Paweł
TI  - Sequent Systems for Consequence Relations of Cyclic Linear Logics
JO  - Bulletin of the Section of Logic
PY  - 2024
SP  - 245
EP  - 274
VL  - 53
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a5/
LA  - en
ID  - BSL_2024_53_2_a5
ER  - 
%0 Journal Article
%A Płaczek, Paweł
%T Sequent Systems for Consequence Relations of Cyclic Linear Logics
%J Bulletin of the Section of Logic
%D 2024
%P 245-274
%V 53
%N 2
%U http://geodesic.mathdoc.fr/item/BSL_2024_53_2_a5/
%G en
%F BSL_2024_53_2_a5

[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

[2] V. M. Abrusci, Classical Conservative Extensions of Lambek Calculus, Studia Logica, vol. 71(3) (2002), pp. 277–314 | DOI

[3] 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.

[4] 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

[5] W. Buszkowski, Involutive nonassociative Lambek calculus: Sequent systems and complexity, Bulletin of the Section of Logic, vol. 46(1/2) (2017) | DOI

[6] K. Chvalovský, Undecidability of consequence relation in full non-associative Lambek calculus, The Journal of Symbolic Logic, (2015), pp. 567–586 | DOI

[7] J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–101 | DOI

[8] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae, vol. 22(1–2) (1995), pp. 53–67 | DOI

[9] 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

[10] 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

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

[12] D. N. Yetter, Quantales and (Noncommutative) Linear Logic, The Journal of Symbolic Logic, vol. 55(1) (1990), pp. 41–64 | DOI