LFCS Seminar: Thursday 3 September: Tarmo Uustalu

In detail:

Tarmo Uustalu, Reykjavik University

https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcs.ioc.ee%2F~tarmo%2F&data=05%7C02%7C%7C15b32a34812040270fe308df076567b8%7C2e9f06b016694589878910a06934dc61%7C0%7C0%7C639237804296415086%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=KfSiFaHTLQ0mbmkw2%2BlXfuK7QcxhgSE4xWUQiCI%2BEo0%3D&reserved=0

  Thu, 03 Sep, 4.10pm

  Venue: Appleton Tower AT 2.14 (note unusual place and day)

Title: Substructural intuitionistic modal logics, sequent calculi, multicategories and representability

Abstract: This is a talk on the structural proof theory of substructural intuitionistic modal logics defined by categorical semantics. We will consider substructural intuitionistic versions of K, T, K4 and S4 with multiplicative verum, conjunction and a box modality. We take them to be defined by semantics in terms of monoidal categories with a strong monoidal endofunctor, a copointed endofunctor, a semicomonad or a comonad, optionally (quasi-)idempotent.

I will show that these logics admit elegant cut-free sequent calculi where the antecedent of a sequent is a list of formulae labelled by natural numbers for box-depths. The equations governing the categorical models all translate into eta- and commutative conversions. With focusing, we achieve subcalculi that keep exactly one representative of each equivalence class of proofs, allowing us to easily see that the (quasi-)idempotent variants of these logics enjoy Mac Lane type coherence: their free models are thin.

I will also demonstrate that the designs of these sequent calculi are directly justified by equivalent semantics of these logics in terms of representable multicategories for suitable notions of

(generalized) multicategory and representability: they are presentations of the free such representable multicategories.

I will briefly discuss adding linear implications.

This is joint work with Michel Smykalla, Niccolò Veltri and Cheng-Syuan Wan.