Giovanni Cinà
(ILLC)
Proof Theory in the Light of Categories
April 5th at 17:30, in Science Park 107 F1.15
In this talk we will provide motivations and examples to justify the following conjecture:
Every "properly designed" sequent calculus can be expressed in Category Theory.
The presentation is divided in two parts. We will begin introducing some formalisms from Proof Theory, namely Hilbert calculi, natural deductions, sequent and display calculi. We will explain what is gained in stepping from the first to the last, especially underlying the progression from global to local and modular rules and its relevance for cut-elimination. As a case study, we analyze the shape of the rules of a specific calculus and notice that they are essentially of three kinds.
In the second part we will introduce the core notions of Category Theory, remaining at an intutive level. We will stress that, when a suitable framework is defined, the connectives of a logic can be seen as functors. This leads us to the identification of the three kinds of inference rules with the properties of functoriality, naturality and adjointness. We conclude analyzing the categorical reformulation of some known propositional logics.
The talk is accessible also for those with no background in Proof Theory and Category Theory.