Voir la théorie de la démonstration de la logique modale à travers un télescope focalisé

In this thesis, we use in two ways the concept of synthetic inference rules that can be obtained from a focused proof system; from one side of the “telescope”, focusing allows us to analyse the internal machinery of inference rules; on the other side, it allows us to consider more global behaviours.In the first part, we review existing proof systems for modal logic, concentrating our efforts around the sequent calculus and its extensions. We underline the issues that drive the modal proof theory community, such as the usual distinction between labelled and unlabelled systems that we aim at deconstructing. We present these questions and concepts in parallel for classical and intuitionistic modal logic in chapter 2 and 3 respectively. We in particular go through Fitting’s indexed nested sequents, for which we demonstrated a new completeness result via cut-elimination.The second part recalls first the notion of focusing and of synthetic inference rules in chapter 4, then presents twoof our contributions in chapter 5 and 6. Firstly, we show 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. Secondly, we propose a similar encoding though for ordinary (unlabelled) sequent calculus via an intermediate focused framework based on Negri’s labelled sequent calculus.The third part reports on two other contributions, namely the completeness proofs of two nested sequent calculi for both classical and intuitionistic modal logic, first a focused version in chapter 7, and then a system merely based on synthetic inference rules in chapter 8. 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.Dans cette thèse, nous utilisons de deux manières le concept de règles d’inférence synthétiques pouvant être obtenues à partir d’un système de preuve focalisé; d’un côté du “télescope”, la focalisation nous permet d’analyser les mécanismes internes des règles d’inférence; de l’autre côté, elle nous permet de nous intéresser à leur comportement plus global.Dans la première partie, nous passons en revue les systèmes de preuves existants pour la logique modale en nous concentrant autour du calcul des séquents et ses extensions. Nous mettons en valeur les problématiques qui animent le domaine de la théorie de la démonstration de la logique modale, notamment en déconstruisant la distinction usuelle entre systèmes étiquetés et non-étiquetés. Nous présentons ces questions et concepts en parallèle dans les chapitres 2 et 3 pour la logique modale classique et intuitionniste respectivement. Nous détaillons en particulier le calcul des séquents emboîtés indexés de Fitting pour lequel nous avons démontré un nouveau résultat de complétude via élimination des coupures.La deuxième partie rappelle d’abord les notions de focalisation et de règles d’inférence synthétiques dans le chapitre 4, puis présente deux contributions dans les chapitres 5 et 6. Premièrement, nous démontrons comment émuler le calcul étiqueté pour la logique modale intuitionniste de Simpson à l’aide du calcul focalisé pour la logique du premier ordre de Liang et Miller, étendant ainsi les travaux de Miller et Volpe au cas intuitionniste. Deuxièmement, nous proposons un encodage similaire mais pour le calcul des séquents ordinaire (non-étiqueté) à l’aide d’une structure intermédiaire basée sur une version focalisée du calcul des séquents étiquetés de Negri. La troisième partie rapporte deux autres de nos contributions: les preuves de complétude de deux calculs de séquents emboîtés pour la logique modale (classique et intuitionniste), d’abord une version focalisée dans le chapitre 7, puis un système basé uniquement sur des règles d’inférence synthétiques dans le chapitre 8. Ces règles ne retiennent que les transitions principales du raisonnement et rendent invisibles la plupart des règles du calcul focalisé, ce qui rend la présentation du système claire et élégante et simplifie grandement les preuves d’élimination des coupures et de complétude