Vlasta Sikimic
(University of Belgrade)
On Purpose and Variations of Cut Elimination
March 14th at 17:30, in ILLC Seminar Room (F1.15)
Non-trivial cut elimination is a property that sequent calculi can have depending on the logic they are capturing. This property is useful for proving other results, such as the subformula property, decidability, coherence, interpolation, symmetry of connectives, etc. When expressed in a categorial setting, cut rule boils down to composition and its elimination procedure can be related to the notion of adjunction. In the talk these ideas will be explained and discussed together with the 'canonical' cut elimination available for Belnap's display calculi. Canonical cut elimination, also referred to as Belnap-style, is a smooth and modular cut elimination procedure that is verified by checking a minimal list of conditions. However, modularity is gained because of the multitude of structural connectives that display calculi have in contrast with standard Gentzen calculi.
The talk is intended to address a wide range of audiences, stressing the conceptual aspect of the key ideas. The introduction will provide some flavour of cut elimination in standard Gentzen system and its categorial encoding. The main part of the presentation is concerned with the Belnap-style cut elimination, as well as methodological suggestions and general conclusions. Finally, we will indicate questions that are open for further research.