Minicourse "Substructural Logics à la Lambek – Proof Theory and Categorical Semantics"

Substructural Logics à la Lambek: Proof Theory and Categorical Semantics
Tarmo Uustalu (Reykjavik University & Tallinn University of Technology)
October 21–30, 2024

Abstract
In the 1960s, Joachim Lambek pioneered an approach to substructural logics that unifies proof theory and category theory, motivated by linguistics. ‘Substructural’ means here that some basic principles like “A implies true,” “A implies A and A,” and “A and B imply B and A” do not hold. In sequent calculus terms, this corresponds to the absence of the structural rules of left weakening, contraction, and exchange, indicating that logic is more about resources than truth. What is now known as Lambek calculus is a noncommutative intuitionistic linear logic with a (multiplicative) conjunction and two implications, left and right.
In this minicourse, I will review this approach first on Lambek calculus and a number of variations of it. Then I will focus on skew logics—logics that are even weaker than substructural in that the conjunction connective is only semiunital and semiassociative.
The course will be self-contained. Basic knowledge of classical and intuitionistic logic (Hilbert-style systems and sequent calculi) is desirable for good intuitions. I will introduce the necessary ingredients of proof theory and category theory.

Timetable
Monday, 21: 11:30–13:30 in Aula D
Tuesday, 22: 8:30–10:30 in Aula C
Friday, 25: 15:30–18:30 in Aula B
Monday, 28: 11:30–13:30 in Aula D
Tuesday, 29: 8:30–10:30 in Aula C
Wednesday, 30: 10:30–11:30 in Aula M

Material
You can access the material here.