Skew Everything! Diving Deep Under Substructural Logics
Tallinn University of Technology
Abstract:
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).