Semi-Substructural Logics à la Lambek with Symmetry

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.