Cheng-Syuan Wan

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.

This work studies Craig interpolation for the logic $$\texttt{SkNMILL}$$, a substructural logic supporting only directed versions of the structural rules of associativity and unitality. In this setting, Craig interpolation cannot be proved by directly employing standard proof-theoretic methods, such as Maehara’s method, a situation that $$\texttt{SkNMILL}$$ shares with other logical systems such as the product-free Lambek calculus and the implicational fragment of intuitionistic logic. We show how to overcome this issue and appropriately modify Maehara’s method for recovering Craig interpolation. We take one step further and, following the category-theoretic perspective of Čubrić, we produce a proof-relevant version of the interpolation theorem, in which we show that our interpolation procedures are right inverses of the admissible cut rules. All our results have been formalized in the proof assistant Agda.