What is a Good Sequent Calculus?

old_uid9567
titleWhat is a Good Sequent Calculus?
start_date2011/01/24
schedule17h30-19h30
onlineno
summaryIn his doctoral thesis of 1935, the young and brilliant student Gerhard Gentzen introduced what is today known as sequent calculus. Firstly Gentzen formulated a sequent calculus for classical logic, and later he adapted it to the case of intuitionistic logic. Over the last eighty years the sequent calculus has been the central interest of several illustrious proof theorists. This has given rise to a broad literature and numerous results. Recently the structure of the sequent calculus has been extended and modified in order to be applied to new logics such as modal logics or substructural logics. In front of this situation the following question has naturally arisen: is any modification allowed? Philoso- phers as well as computer scientists (e.g. Avron (1996); Sambin et al. (2000); Schroeder-Heister (2007);Wansing (1998)) have been trying to answer this ques- tion in the negative. Our aim in this talk is to contribute to this debate. More precisely, we will propose and argue for a number of properties that sequent calculi should satisfy in order to be considered as good. Moreover we will show what is takes to have a good sequent calculus for the modal Hilbert system S5. We will thus provide a solution to a long-standing open problem.
responsiblesPataut, Dubucs, Panza