Semi-Substructural Logics à la Lambek
Cheng-Syuan Wan
TL;DR
This work develops cut-free sequent calculi for left skew monoidal closed and skew monoidal bi-closed categories within a non-associative Lambek framework, using tree-structured antecedents to overcome limitations of stoup-style syntax. It introduces both an axiomatic calculus ($\mathtt{SkMBiCA}$) and a Lambek-style calculus ($\mathtt{SkMBiCT}$), proving their equivalence and establishing cut-elimination, along with an equivalence to the corresponding calculi for left skew monoidal closed categories. A relational (ternary-frame) semantics is provided for $\mathtt{SkMBiCA}$, with soundness, completeness, and a main correspondence theorem linking frame conditions to structural laws, enabling modular derivations of skew-category results. The paper also demonstrates how to obtain thin skew monoidal bi-closed categories from frames and outlines future directions, including interpolation and modal extensions, solidifying a constructive bridge between substructural logics and semi-associative skew categories. The results advance formal tools for semi-substructural logics that interpolate between non-associative Lambek calculus and associative linear logic, with potential applications to language semantics and resource-sensitive reasoning.
Abstract
This work studies the proof theory of left (right) skew monoidal closed categories and skew monoidal bi-closed categories from the perspective of non-associative Lambek calculus. Skew monoidal closed categories represent a relaxed version of monoidal closed categories, where the structural laws are not invertible; instead, they are natural transformations with a specific orientation. 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. We solve the problem by constructing cut-free sequent calculi for left skew monoidal closed and skew monoidal bi-closed categories, reminiscent of non-associative Lambek calculus, with trees as antecedents. Each calculus is respectively equivalent to the sequent calculus with stoup (for left skew monoidal categories) and the axiomatic calculus (for skew monoidal bi-closed categories). Moreover, we prove that the latter calculus is sound and complete with respect to its 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.