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

Relatore:  Tarmo Uustalu - Reykjavik University & Tallinn University of Technology
  lunedì 21 ottobre 2024 alle ore 11.30 (see abstract for further dates)

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

Referente
Peter Michael Schuster

Referente esterno
Giulio Fellin

Data pubblicazione
2 ottobre 2024

Offerta formativa

Condividi