Semi-Substructural Logics à la Lambek with Symmetry

Cheng-Syuan Wan

doi:10.18778/0138-0680.2025.17

Authors

Cheng-Syuan Wan Tallinn University of Technology, Department of Software Science, Estonia https://orcid.org/0000-0003-2053-1688

DOI:

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

Keywords:

substructural logic, Lambek calculus, non-associative Lambek calculus, category theory, skew monoidal category, ternary relational semantics

Abstract

This work studies the proof theory and ternary relational semantics of left (right) skew monoidal closed categories and skew monoidal bi-closed categories, both symmetric and non-symmetric, from the perspective of non-associative Lambek calculus. Uustalu et al. used sequents with stoup (the leftmost position of an antecedent that can be either empty or a single formula) to deductively model left skew monoidal closed categories, yielding results regarding proof identities and categorical coherence. However, their syntax does not work well when modeling right skew monoidal closed and skew monoidal bi-closed categories, whether symmetric or non-symmetric.

We solve the problem via more flexible and equivalent frameworks to characterize the categories above: tree sequent calculus (where antecedents are binary trees) and axiomatic calculus (where antecedents are a single formula), inspired by works on non-associative Lambek calculus. Moreover, we prove that the axiomatic calculi are sound and complete with respect to their ternary relational models. We also prove a correspondence between frame conditions and structural laws, providing an algebraic way to understand the relationship between the left and right skew monoidal closed categories, encompassing both symmetric and non-symmetric variants.

References

V. M. Abrusci, Non-commutative intuitionistic linear logic, Mathematical Logic Quarterly, vol. 36(4) (1990), pp. 297–318, DOI: https://doi.org/10.1002/malq.19900360405.
Google Scholar DOI: https://doi.org/10.1002/malq.19900360405

T. Altenkirch, J. Chapman, T. Uustalu, Monads need not be endofunctors, Logical Methods in Computer Science, vol. 11(1) (2015), 3, DOI: https://doi.org/10.2168/lmcs-11(1:3)2015.
Google Scholar DOI: https://doi.org/10.2168/LMCS-11(1:3)2015

J.-M. Andreoli, Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, vol. 2(3) (1992), pp. 297–347, DOI: https://doi.org/10.1093/logcom/2.3.297.
Google Scholar DOI: https://doi.org/10.1093/logcom/2.3.297

E. Blaisdell, M. Kanovich, S. L. Kuznetsov, E. Pimentel, A. Scedrov, Non-associative, Non-commutative Multi-modal Linear Logic, [in:] J. Blanchette, L. Kovács, D. Pattinson (eds.), Proceedings of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, vol. 13385 of Lecture Notes in Computer Science, Springer (2022), pp. 449–467, DOI: https://doi.org/10.1007/978-3-031-10769-6_27.
Google Scholar DOI: https://doi.org/10.1007/978-3-031-10769-6_27

J. Bourke, Skew structures in 2-category theory and homotopy theory, Journal of Homotopy and Related Structures, vol. 12(1) (2017), pp. 31–81, DOI: https://doi.org/10.1007/s40062-015-0121-z.
Google Scholar DOI: https://doi.org/10.1007/s40062-015-0121-z

J. Bourke, S. Lack, Skew monoidal categories and skew multicategories, Journal of Algebra, vol. 506 (2018), pp. 237–266, DOI: https://doi.org/10.1016/j.jalgebra.2018.02.039.
Google Scholar DOI: https://doi.org/10.1016/j.jalgebra.2018.02.039

J. Bourke, S. Lack, Braided skew monoidal categories, Theory and Applications of Categories, vol. 35(2) (2020), pp. 19–63, URL: http://www.tac.mta.ca/tac/volumes/35/2/35-02abs.html.
Google Scholar DOI: https://doi.org/10.70930/tac/ei4b9k93

M. Buckley, R. Garner, S. Lack, R. Street, The Catalan simplicial set, Mathematical Proceedings of Cambridge Philosophical Society, vol. 158(2) (2015), pp. 211–222, DOI: https://doi.org/10.1017/s0305004114000498.
Google Scholar DOI: https://doi.org/10.1017/S0305004114000498

M. Bulińska, On the complexity of nonassociative Lambek calculus with unit, Studia Logica, vol. 93(1) (2009), pp. 1–14, DOI: https://doi.org/10.1007/s11225-009-9205-2.
Google Scholar DOI: https://doi.org/10.1007/s11225-009-9205-2

B. Day, M. Laplaza, On embedding closed categories, Bulletin of the Australian Mathematical Society, vol. 18(3) (1978), pp. 357–371, DOI: https://doi.org/10.1017/s0004972700008236.
Google Scholar DOI: https://doi.org/10.1017/S0004972700008236

W. J. de Schipper, Symmetric closed categories, vol. 64 of Mathematical Centre Tracts, CWI, Amsterdam (1975).
Google Scholar

K. Došen, A brief survey of frames for the Lambek calculus, Mathematical Logic Quarterly, vol. 38(1) (1992), pp. 179–187, DOI: https://doi.org/10.1002/malq.19920380113.
Google Scholar DOI: https://doi.org/10.1002/malq.19920380113

S. Eilenberg, G. M. Kelly, Closed categories, [in:] S. Eilenberg, D. K. Harrison, S. Mac Lane, H. Röhrl (eds.), Proceedings of Conference on Categorical Algebra (La Jolla, 1965), Springer (1966), pp. 421–562, DOI: https://doi.org/10.1007/978-3-642-99902-4_22.
Google Scholar DOI: https://doi.org/10.1007/978-3-642-99902-4_22

J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102, 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.-Y. Girard, A new constructive logic: classical logic, Mathematical Structures in Computer Science, vol. 1(3) (1991), pp. 255–296, DOI: https://doi.org/10.1017/s0960129500001328.
Google Scholar DOI: https://doi.org/10.1017/S0960129500001328

S. Lack, R. Street, Skew monoidales, skew warpings and quantum categories, Theory and Applications of Categories, vol. 26(15) (2012), pp. 385–402, URL: http://www.tac.mta.ca/tac/volumes/26/15/26-15abs.html.
Google Scholar DOI: https://doi.org/10.70930/tac/yo3yioev

S. Lack, R. Street, Triangulations, orientals, and skew monoidal categories, Advances in Mathematics, vol. 258 (2014), pp. 351–396, DOI: https://doi.org/10.1016/j.aim.2014.03.003.
Google Scholar DOI: https://doi.org/10.1016/j.aim.2014.03.003

J. Lambek, The mathematics of sentence structure, American Mathematical Monthly, vol. 65(3) (1958), pp. 154–170, DOI: https://doi.org/10.2307/2310058.
Google Scholar DOI: https://doi.org/10.1080/00029890.1958.11989160

J. Lambek, On the Calculus of Syntactic Types, [in:] R. Jakobson (ed.), Structure of Language and Its Mathematical Aspects, AMS, Providence (1961), pp. 166–178, DOI: https://doi.org/10.1090/psapm/012.
Google Scholar DOI: https://doi.org/10.1090/psapm/012/9972

S. Mac Lane, Natural associativity and commutativity, Rice University Studies, vol. 49(4) (1963), pp. 28–46, URL: http://hdl.handle.net/1911/62865.
Google Scholar

M. Moortgat, Multimodal linguistic inference, Journal of Logic, Language and Information, vol. 5(3–4) (1996), pp. 349–385, DOI: https://doi.org/10.1007/bf00159344.
Google Scholar DOI: https://doi.org/10.1007/BF00159344

M. Moortgat, The Tamari order for D3 and derivability in semi-associative Lambek-Grishin Calculus, Talk at 16th Workshop on Computational Logic and Applications, CLA 2020 (2020), slides available at: http://cla.tcs.uj.edu.pl/history/2020/pdfs/CLA_slides_Moortgat.pdf.
Google Scholar

R. Moot, C. Retoré, The logic of categorial grammars: A deductive account of natural language syntax and semantics, vol. 6850 of Lecture Notes in Computer Science, Springer (2012), DOI: https://doi.org/10.1007/978-3-642-31555-8.
Google Scholar DOI: https://doi.org/10.1007/978-3-642-31555-8

K. Rosenthal, Relational monoids, multirelations, and quantalic recognizers, Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 38(2) (1997), pp. 161–171.
Google Scholar

R. Street, Skew-closed categories, Journal of Pure and Applied Algebra, vol. 217(6) (2013), pp. 973–988, DOI: https://doi.org/10.1016/j.jpaa.2012.09.020.
Google Scholar DOI: https://doi.org/10.1016/j.jpaa.2012.09.020

K. Szlachányi, Skew-monoidal categories and bialgebroids, Advances in Mathematics, vol. 231(3–4) (2012), pp. 1694–1730, DOI: https://doi.org/10.1016/j.aim.2012.06.027.
Google Scholar DOI: https://doi.org/10.1016/j.aim.2012.06.027

T. Uustalu, N. Veltri, C.-S. Wan, Proof theory of skew non-commutative MILL, [in:] A. Indrzejczak, M. Zawidzki (eds.), Proceedings of 10th International Conference on Non-classical Logics: Theory and Applications, NCL 2022, vol. 358 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2022), pp. 118–135, DOI: https://doi.org/10.4204/eptcs.358.9.
Google Scholar DOI: https://doi.org/10.4204/EPTCS.358.9

T. Uustalu, N. Veltri, N. Zeilberger, Eilenberg-Kelly reloaded, volume 352 of Electronic Notes in Theoretical Computer Science, vol. 352 (2020), pp. 233–256, DOI: https://doi.org/10.1016/j.entcs.2020.09.012.
Google Scholar DOI: https://doi.org/10.1016/j.entcs.2020.09.012

T. Uustalu, N. Veltri, N. Zeilberger, Deductive systems and coherence for skew prounital closed categories, [in:] C. Sacerdoti Coen, A. Tiu (eds.), Proceedings of 15th Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, vol. 332 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2021), pp. 35–53, DOI: https://doi.org/10.4204/eptcs.332.3.
Google Scholar DOI: https://doi.org/10.4204/EPTCS.332.3

T. Uustalu, N. Veltri, N. Zeilberger, Proof theory of partially normal skew monoidal categories, [in:] D. I. Spivak, J. Vicary (eds.), Proceedings of 3rd Annual International Applied Category Theory Conference 2020, ACT 2020, vol. 333 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2021), pp. 230–246, DOI: https://doi.org/10.4204/eptcs.333.16.
Google Scholar DOI: https://doi.org/10.4204/EPTCS.333.16

T. Uustalu, N. Veltri, N. Zeilberger, The sequent calculus of skew monoidal categories, [in:] C. Casadio, P. J. Scott (eds.), Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, vol. 20 of Outstanding Contributions to Logic, Springer (2021), pp. 377–406, DOI: https://doi.org/10.1007/978-3-030-66545-6_11.
Google Scholar DOI: https://doi.org/10.1007/978-3-030-66545-6_11

N. Veltri, Coherence via focusing for symmetric skew monoidal categories, [in:] A. Silva, R. Wassermann, R. de Queiroz (eds.), Proceedings of 27th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2021, vol. 13028 of Lecture Notes in Computer Science, Springer (2021), pp. 184–200, DOI: https://doi.org/10.1007/978-3-030-88853-4_12.
Google Scholar DOI: https://doi.org/10.1007/978-3-030-88853-4_12

N. Veltri, Maximally multi-focused proofs for skew non-commutative MILL, [in:] H. H. Hansen, A. Scedrov, R. J. G. B. de Queiroz (eds.), Proceedings of 29th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2023, vol. 13923 of Lecture Notes in Computer Science, Springer (2023), pp. 377–393, DOI: https://doi.org/10.1007/978-3-031-39784-4_24.
Google Scholar DOI: https://doi.org/10.1007/978-3-031-39784-4_24

N. Veltri, Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories, Journal of Logic and Computation, (to appear), DOI: https://doi.org/10.1093/logcom/exae059.
Google Scholar DOI: https://doi.org/10.1093/logcom/exae059

N. Veltri, C.-S. Wan, Semi-substructural logics with additives, [in:] T. Kutsia, D. Ventura, D. Monniaux, J. F. Morales (eds.), Proceedings of 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis, LSFA/HCVS 2023, vol. 402 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2024), pp. 63–80, DOI: https://doi.org/10.4204/eptcs.402.8.
Google Scholar DOI: https://doi.org/10.4204/EPTCS.402.0

C.-S. Wan, Semi-substructural logics à la Lambek, [in:] A. Indrzejczak, M. Zawidzki (eds.), Proceedings of 11th International Conference on Non-classical Logics: Theory and Applications, NCL 2024, vol. 415 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association (2024), pp. 195–213, DOI: https://doi.org/10.4204/eptcs.415.18.
Google Scholar DOI: https://doi.org/10.4204/EPTCS.415.18

N. Zeilberger, A sequent calculus for a semi-associative law, Logical Methods in Computer Science, vol. 15(1) (2019), 9, DOI: https://doi.org/10.23638/lmcs-15(1:9)2019.
Google Scholar DOI: https://doi.org/10.23638/LMCS-15(1:9)2019