Niccolò Veltri, Tallinn University of Technology
Skew everything! Diving deep under substructural logics
In structural proof theory, we study logics weaker than intuitionistic conjunctive(-implicational) logic in whose sequent calculus presentation one or several of the standard structural rules are not available. In relevant logic, weakening is not allowed, in affine logic, contraction is forbidden. In linear logic, one has neither. Sometimes even exchange is not there, like in non-commutative linear logic and Lambek’s syntactic calculus. These logics, often called substructural, or more precisely their proof systems with their appropriate notions of equality of derivations, axiomatize monoidal (closed) categories and superstructures thereof.
In the sequent calculus of a substructural logic, it is natural to think of formulae in the antecedent as types of resources at our disposal, while the formula in the succedent is a task that needs to be fulfilled with the resources at hand. Under this interpretation, the structural rules tell us how resources can be manipulated and consumed. In intuitionistic logic, resources can be permuted, deleted and copied. In linear logic, they can be neither deleted nor copied, but they can be permuted. In non-commutative linear logic, resources cannot be permuted, so they must be consumed in the order they occur in the antecedent.
In this talk, we look at a more restricted class of substructural logics. Let me call them ultrasubstructural for today. In the sequent calculi of those logics, antecedents consist of a stoup, which is an optional formula, and a context, a list of formulae. A typical restriction is that a left logical rule can only be applied in the stoup position. Under the resources-as-formulae correspondence, resources in these systems are allowed to be decomposed only when positioned in the stoup. I claim that these logics are interesting both from the structural proof theory point of view as well as for category theorists since they correspond to skew variations of monoidal (closed) categories.
This is joint work with Tarmo Uustalu (Reykjavik University) and Noam Zeilberger (LIX, École Polytechnique).