A proof-theoretic treatment of left and right skew monoidal closed and skew monoidal bi-closed categories as semi-substructural logics in the style of the nonassociative Lambek calculus. The work builds cut-free sequent calculi with trees as antecedents that are equivalent to the earlier stoup-based and axiomatic calculi, proves soundness and completeness of the bi-closed calculus against relational models, and matches frame conditions to structural laws - overcoming the limits of stoup syntax for the right skew and bi-closed cases.
This NCL'24 proceedings paper develops the proof theory of left (and right) skew monoidal closed categories and skew monoidal bi-closed categories, viewed through the lens of the nonassociative Lambe…