Semi-Substructural Logics with Additives
Niccolò Veltri, Cheng-Syuan Wan
TL;DR
This work advances the proof theory of semi-substructural logics built atop skew monoidal categories by introducing a cut-free sequent calculus for a fragment with additive connectives and a focused sequent calculus with tag annotations that canonicalize derivations modulo a coherence-preserving congruence. It provides categorical semantics via distributive skew monoidal categories, with the sequent calculus forming the initial model (the free distributive skew monoidal category on atoms) and a rigorous normalization procedure formalized in Agda. The authors extend the logic with additive units, skew exchange, and a linear implication, adapting the focusing framework and coherence machinery to these extensions and outlining their semantic counterparts (terminal/initial objects, skew symmetry, and closed structure). The resulting framework offers a modular, constructive route to coherence results and normalization across a family of skew-structured sublogics, with potential impact on linguistics and combinatorics where resource-sensitive reasoning plays a role. ${S}$ ${|}$ ${\Gamma}$ ${\vdash}$ ${A}$ in various skew settings and the tagged focusing strategy are central to achieving complete, confluence-friendly proof search and to enabling Agda-based formal verification of correctness claims.
Abstract
This work concerns the proof theory of (left) skew monoidal categories and their variants (e.g. closed monoidal, symmetric monoidal), continuing the line of work initiated in recent years by Uustalu et al. Skew monoidal categories are a weak version of Mac Lane's monoidal categories, where the structural laws are not required to be invertible, they are merely natural transformations with a specific orientation. Sequent calculi which can be modelled in such categories can be identified as deductive systems for restricted substructural fragments of intuitionistic linear logic. These calculi enjoy cut elimination and admit a focusing strategy, sharing resemblance with Andreoli's normalization technique for linear logic. The focusing procedure is useful for solving the coherence problem of the considered categories with skew structure. Here we investigate possible extensions of the sequent calculi of Uustalu et al. with additive connectives. As a first step, we extend the sequent calculus with additive conjunction and disjunction, corresponding to studying the proof theory of skew monoidal categories with binary products and coproducts satisfying a left-distributivity condition. We introduce a new focused sequent calculus of derivations in normal form, which employs tag annotations to reduce non-deterministic choices in bottom-up proof search. The focused sequent calculus and the proof of its correctness have been formalized in the Agda proof assistant. We also discuss extensions of the logic with additive units, a form of skew exchange and linear implication.