The proof theory of skew logics

I will talk about skew logics. By skew logics I mean substructural logics defined by categories with various types of skew structure: skew monoidal categories and variations like skew closed or prounital
closed categories, skew monoidal closed categories, partially normal skew monoidal categories, symmetric skew monoidal categories etc.

Skew monoidal categories (due to K. Szláchanyi) differ from normal (= ordinary) monoidal categories in that the structural laws of unitality and associativity of the tensor are not required to be
natural isomorphisms; they are only natural transformations in a specific direction. Skew closed categories are a similar relaxation of closed categories. Partially normal skew monoidal categories are
between skew and normal: they have some structural laws invertible, e.g., in left-normal skew monoidal categories, the left unitality law is a natural isomorphism.

In a series of papers, I, Niccolò Veltri, Cheng-Syuan Wan and Noam Zeilberger have studied skew logics using a particular proof-theoretical methodology.

For each logic we have considered, we have devised a sequent calculus whose derivations represent maps of the free category with the relevant skew structure. Furthermore, we have identified a subcalculus of
normal-form derivations oriented at root-first proof search, with the property that every map is represented by exactly one derivation. This has given us for each logic a method to decide equality of two maps and
a method to enumerate without duplicates all maps between a pair of objects (this is a finite set).

We have found that, because they are so weak (generally dropping commutativity and some directions of unitality and associativity), skew logics provide excellent insights into the fine anatomy of
substructural logics. In particular, they explain which ingredients contribute to which characteristics of the stronger more familiar substructural logics.

We started our project with purely multiplicative logics, but Niccolò Veltri and Cheng-Syuan Wan have also analyzed a combination of multiplicative connectives with additives.