Semi-Substructural Logics \`a la Lambek

TL;DR

This paper develops cut-free sequent calculi for skew monoidal closed categories inspired by non-associative Lambek calculus, providing proof-theoretic and categorical insights into their structure and coherence.

Contribution

It introduces novel sequent calculi for left skew monoidal closed and skew monoidal bi-closed categories, addressing limitations of previous syntax and establishing soundness, completeness, and algebraic correspondences.

Findings

Constructed cut-free sequent calculi for skew monoidal categories

Proved soundness and completeness of the calculus for bi-closed categories

Established algebraic correspondence between frame conditions and structural laws

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.