Sonia Marin will defend her PhD thesis entitled « Modal proof theory through a focused telescope » on Tuesday, January 30^th at 3pm in Amphithéâtre Sophie Germain (bâtiment Turing).

Abstract: In this thesis, we consider the proof theory of modal logic to illustrate two uses of the synthetic inference rules extracted from focused proof systems. From one side of the “telescope”, focusing allows us to analyse the internal machinery of inference rules. We show first how to emulate Simpson’s labelled sequent calculus for intuitionistic modal logic with Liang and Miller’s focused sequent calculus for first-order logic, therefore extending the result of Miller and Volpe to the intuitionistic case. Then, we propose a similar encoding though for ordinary (unlabelled) sequent calculus via an intermediate focused framework based on Negri’s labelled sequent calculus. From the other side of the “telescope”, focusing allows us to observe more global behaviours in proofs. In particular, we give completeness proofs for two nested sequent calculi for both classical and intuitionistic modal logic, first for a focused version, and then for a system merely based on synthetic inference rules. These rules only retain the transitions between big steps of reasoning forgetting most of the focused rules, which renders the system presentation clear and elegant while also simplifying the cut-elimination and completeness proofs.