ICE-TCS seminar: Tarmo Uustalu
Ultrasubstructural logics
ICE-TCS seminar #349
Date and time: Monday, 24 January 2020, 11:50-12:35
Location: Room M108
Speaker: Tarmo Uustalu, Reykjavik University, Iceland and Tallinn University of Technology, Estonia
Title: Ultrasubstructural logics
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, a.k.a. 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.
But there are good reasons to consider even more restricted logics! In this talk, we look at particular variety of those. 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. 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 Niccolò Veltri (Tallinn University of
Technology) and Noam Zeilberger (LIX, École Polytechnique).
