Substructural Logics à la Lambek: Proof Theory and Categorical Semantics (12 hours)

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.

The schedule for the minicourse is as follows - for updates please see https://www.logicverona.it/

• Monday, 21st: 2 hours, 11:30–13:30 in Aula D
• Tuesday, 22nd: 2 hours, 8:30–10:30 in Aula C
• Friday, 25th: 3 hours, 15:30–18:30 in Aula B
• Monday, 28th: 2 hours, 11:30–13:30 in Aula D
• Tuesday, 29th: 2 hours, 8:30–10:30 in Aula C
• Wednesday, 30th: 1 hour, 10:30–11:30 in Aula M