Semi-Substructural Logics with Additives

TL;DR

This paper develops a focused sequent calculus for skew monoidal categories with additive connectives, formalized in Agda, advancing proof theory for weak monoidal structures and their extensions.

Contribution

It introduces a new focused sequent calculus with additive connectives for skew monoidal categories, including formalization in Agda and extensions with units and implications.

Findings

Formalized a focused sequent calculus in Agda.

Extended calculus with additive conjunction, disjunction, units, and implications.

Proved correctness and cut elimination for the calculus.

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.