Soutenance de thèse de GAO Han
Titre de thèse
Combinaison des logiques modales et de la logique intuitionniste : calculs structurés et nouvelles logiques
Combining Modal logics and intuitionistic logic: structured calculi and new logics
Résumé de la thèse
La logique intuitionniste constitue une alternative fondamentale à la logique classique, excluant certains principes classiques, tandis que la logique modale est une extension significative de la logique propositionnelle classique, enrichissant le langage propositionnel par des modalités. Concernant leur combinaison, dans le cadre intuitionniste de la logique modale, divers systèmes ont émergé dans la littérature, donnant lieu à un paysage encore plus riche et varié que celui de la logique modale classique. Dans cette thèse, nous étudions différentes logiques modales, avec un intérêt particulier pour la logique modale intuitionniste et sa théorie de la démonstration. Bien que notre intérêt principal porte sur la logique modale intuitionniste, nous considérons également certaines autres variantes de la logique modale qui sont pertinentes dans le contexte plus large de notre étude.
Le corps principal de cette thèse est divisé en quatre parties. La première partie fournit un cadre général aux résultats présentés dans cette thèse. Nous commençons par un aperçu des concepts fondamentaux de la logique intuitionniste et de la logique modale, en considérant à la fois leurs aspects sémantiques et de théorie de la preuve. Nous présentons ensuite l'état de l'art dans le domaine de la logique modale intuitionniste, en passant en revue plusieurs systèmes logiques bien connus dans la littérature, incluant leur sémantique, leur axiomatisation et les calculs de séquents existants. Nous discutons également certains critères proposés pour déterminer ce qui constitue une « bonne » logique modale intuitionniste.
Les trois parties suivantes contiennent les résultats originaux de cette thèse.
La deuxième partie est consacrée à deux logiques nouvellement introduites, FIK et LIK. D'un point de vue sémantique, dans les modèles de Kripke bi-relationnels, les modalités de FIK sont interprétées de la même manière que dans IK de Simpson, tandis que dans LIK, elles suivent l'interprétation propre à la logique modale classique. Nous présentons des systèmes d'axiomes de style Hilbert pour ces deux logiques et établissons leur complétude, ainsi que celle de plusieurs de leurs extensions obtenues par l'ajout d'axiomes issus du cube modal standard. Dans la troisième partie nous proposons un cadre théorie de la preuve appelé calcul des séquents bi-imbriqués (bi-nested sequent calculus), qui constitue un outil unifié applicable à un large éventail de logiques modales intuitionnistes, incluant des logiques connues issues de la littérature ainsi que les deux nouvelles logiques que nous avons proposées. Pour obtenir des calculs bi-imbriqués adaptés à des logiques caractérisées par des conditions de cadre différentes, nous proposons des règles appropriées capturant les interactions entre les deux relations d'un cadre bi-relationnel. Nous définissons ensuite une stratégie de recherche de preuve adaptée à ces calculs qui garantie leur terminaison et par conséquent nous fournit une preuve de la décidabilité des logiques. Nous prouvons leur complétude sémantique en montrant que tout échec dans la recherche de preuve d'une formule donne directement lieu à un contre-modèle fini de celle-ci.
Enfin, dans la quatrième partie, nous appliquons des techniques preuve-théoriques similaires à d'autres systèmes de logique modale. Nous examinons une logique épistémique à agent unique pour le raisonnement éthique ainsi qu'une famille de logiques modales constructives dans un cadre paraconsistant. Nous fournissons des calculs de séquents complets par lesquels nous montrons que ces logiques sont décidables.
Thesis resume
Intuitionistic logic is a fundamental alternative to classical logic excluding some classical principles, whereas modal logic is a significant extension of classical propositional logic that enriches propositional language with modalities. With regard to their combination, in the intuitionistic setting of modal logic, various systems have emerged in the literature, leading to a landscape that is even richer and more diverse than that of classical modal logic. In this thesis, we investigate various modal logics, with a primary focus on intuitionistic modal logic and its proof theory. While our main interest lies in intuitionistic modal logic, we also consider some other variants of modal logic that are relevant to the broader context of our study.
The main body of this thesis is divided into four parts. The first part provides a general background for the results contained in this thesis. We begin with an overview of some fundamental concepts of intuitionistic and modal logic, considering both their semantic and proof-theoretic aspects. Then we introduce state of the art in the field of intuitionistic modal logic, reviewing several well-known logic systems in the literature, including their semantics, axiomatization and existing sequent calculi. We also discuss possible criteria that have been proposed to justify what makes a so-called `good' intuitionistic modal logic.
The next three parts contain the original results in this thesis. The second part is devoted to two newly introduced logics, FIK and LIK. From a semantic perspective, in bi-relational Kripke models, the modalities in FIK are interpreted in the same way as in Simpson's IK, whereas in LIK they follow the same interpretation of classical modal logic. We present Hilbert-style axiom systems for both logics as well as with several extensions of them with axioms from the standard modal cube, then establish their completeness. In the third part we propose a proof-theoretic framework called bi-nested sequent calculus, which is a unified tool and can be applied to a wide range of intuitionistic modal logics, including known logics from the literature and the two new logics we propose. In order to obtain bi-nested calculi for logics with different frame conditions, we propose suitable rules that capture the interactions between the two relations of a bi-relational frame. We then define a suitable proof search strategy for these calculi which ensures termination, whence providing a proof of the decidability of these logics. Moreover, we prove their semantic completeness by showing any failed proof search for a formula directly yields a finite countermodel of it.
Lastly, in the fourth part, we apply similar proof-theoretic techniques to some other modal logic systems. We investigate into a single-agent epistemic logic for ethical reasoning as well as a family of constructive modal logics in a paraconsistent setting. We provide complete sequent calculi by which we show these logics are decidable.