Search

International audience; In this paper we provide the first game semantics for the constructive modal logic CK. We first define arenas encoding modal formulas, we then define winning innocent strategies for games on these arenas, and finally we characterize the winning strategies corresponding to proofs in the logic CK. To prove the full-completeness of our semantics, we provide a sequentialization procedure of winning strategies. We conclude the paper by proving their compositionality and showing how our results can be extend to the constructive modal logic CD.

This thesis can be ideally placed at the intersection of three research topics: conditional logics, proof theory and neighbourhood semantics. The family of logics under scope stems from the works of Stalnaker and Lewis, and extends classical propositional logic by means of a two-place modal operator, which expresses a fine-grained notion of conditionality. The semantics of these logics is modularly defined in terms of neighbourhood models. The research aim is to investigate the proof theory of conditional logics, by defining sequent calculi for them. The proof systems introduced are extensions of Gentzen’s sequent calculus; they are either labelled, defined by enriching the language, or internal, which add structural connectives to the sequents. Moreover, the calculi are standard: they are composed of a finite number of rules, each displaying a fixed number of premisses. The thesis is organized in six chapters. Chapters 1 contains an axiomatic and semantic overview of conditional logics, while Chapter 2 is a short introduction to proof theory. The original contributions to the subject are presented in chapters 3 – 6. Chapter 3 introduces labelled calculi based on neighbourhood models for preferential conditional logics, and Chapter 4 presents different internal proof systems covering counterfactual logics, a subfamily of preferential logics. Chapter 5 analyses the relationship between proof systems by presenting a mapping between a labelled and an internal calculus. Finally, the proof-theoretic methods developed for conditional logics are applied in chapter 6 to the multi-agent epistemic logic. Tämä väitöskirja sijoittuu ideaalisesti kolmen tutkimusaiheen risteykseen: konditionaalien logiikka, todistusteoria, ja ympäristösemantiikka. Katettujen logiikoiden perhe periytyy Stalnakein ja Lewisin töistä ja laajentaa klassillista lauselogiikkaa kaksipaikkaisen modaalioperaattorin kautta. Se ilmaisee hienojakoisen konditionaalisuuden käsitteen. Näiden logiikoiden semantiikka määritellään modulaarisesti ympäristösemantiikan termein. Tutkimuksen tavoitteena on selvittää konditionaalien logiikan todistusteoriaa määrittelemällä niille sekvenssikalkyyleita. Esitellyt todistussysteemit ovat Gentzenin sekvenssikalkyylin laajennuksia; ne ovat joko merkeillä varustettuja, joihin päädytään kielen rikastuksella, tai sisäisiä, joihin päädytään lisäämällä sekvensseihin rakenteellisia konnektiiveja. Nämä laajennukset ovat myös standardikalkyyleja: ne muodostuvat äärellisestä määrästä sääntöjä, joissa jokaisessa on kiinteä määrä premissejä. Väitöskirja muodostuu kuudesta kappaleesta. Kappale 1 sisältää aksiomattisen ja semanttisen katsauksen konditionaalien logiikkaan, ja kappale 2 on taas lyhyt johdatus todistusteoriaan. Uudet tutkimuspanokset aiheeseen on esitetty kappaleissa 3-6. Kappale 3 esittää ns. merkityt sekvenssikalkyylit joiden perustana on preferentiaalisten konditionaalien logiikan ympäristömallit, kappale 4 esittää erilaisia sisäisiä todistussysteemejä jotka kattavat kontrafaktuaalien logiikat, jotka ovat preferentiaalisten logiikoiden alaperhe. Kappale 5 analysoi eri todistussysteemien välisiä suhteita merkkikalkyyylien ja sisäisten kalkyylien välisen kuvauksen kautta. Kuudennessa ja viimeisessä kappaleessa sovelletaan konditionaalien logiikalle kehitettyjä todistusteoreettisia metodeja useamman agentin episteemiseen logiikkaan. La thèse se place à l’intersection de trois sujets de recherche : logiques conditionnelles, théorie de la démonstration et sémantique de voisinage. La famille de logiques conditionnelles considérées provient dès ouvrages de Stalnaker et Lewis. Elle est une extension de la logique classique propositionnelle avec un opérateur modal à deux places, qui exprime une notion affinée de conditionnalité. La sémantique de ces logiques est définie en termes de modèles de voisinage. Le but de la recherche est d'étudier la théorie de la démonstration des logiques conditionnelles, en précisant leur calculs des sequents. Les calculs définis sont des extensions du calcul des sequents de Gentzen ; ils sont étiquetés, c’est à dire définis en enrichissant le langage, ou internes, qui rajoutent des connecteurs structurels aux sequents. La thèse est organisée en six chapitres. Le chapitre 1 présente les axiomes et la sémantique des logiques conditionnelles et le chapitre 2 introduit la théorie de la démonstration. Les contributions originelles au sujet sont traitées dans les chapitres 3 – 6. Le chapitre 3 introduit des calculs de sequents étiquetés basés sur la sémantique de voisinage pour les logiques conditionnelles préférentielles. Le chapitre 4 présente différents systèmes internes de calcul pour les logiques counterfactuelles, une sous-famille des logiques préférentielles. Le chapitre 5 analyse la relation parmi les systèmes de preuve en présentant les deux côtés d’une traduction entre un calcul étiqueté et un calcul interne. Finalement, au chapitre 6, les méthodes de la théorie de la démonstration conditionnelle sont appliquées à une logique épistémique multi-agente.

This thesis can be ideally placed at the intersection of three research topics: conditional logics, proof theory and neighbourhood semantics. The family of logics under scope stems from the works of Stalnaker and Lewis, and extends classical propositional logic by means of a two-place modal operator, which expresses a fine-grained notion of conditionality. The semantics of these logics is modularly defined in terms of neighbourhoodmodels. The research aim is to investigate the proof theory of conditional logics, by defining sequent calculi for them. The proof systems introduced are extensions of Gentzen’s sequent calculus; they are either labelled, defined by enriching the language, or internal, which add structural connectives to the sequents. Moreover, the calculi are standard: they are composed of a finite number of rules, each displaying a fixed number of premisses.The thesis is organized in six chapters. Chapters 1 contains an axiomatic and semantic overview of conditional logics, while Chapter 2 is a short introduction to proof theory. The original contributions to the subject are presented in chapters 3 – 6. Chapter 3 introduces labelled calculi based on neighbourhood models for preferential conditional logics, and Chapter 4 presents different internal proof systems covering counterfactual logics, a subfamily of preferential logics. Chapter 5 analyses the relationship between proof systems by presenting a mapping between a labelled and an internal calculus. Finally, the proof-theoretic methods developed for conditional logics are applied in chapter 6 to a multi-agent epistemic logic.; La thèse se place à l’intersection de trois sujets de recherche : logiques conditionnelles, théorie de la démonstration et sémantique de voisinage. La famille de logiques conditionnelles considérées provient dès ouvrages de Stalnaker et Lewis. Elle est une extension de la logique classique propositionnelle avec un opérateur modal à deux places, qui exprime une notion affinée de conditionnalité. La sémantique de ces logiques est définie en termes de modèles de voisinage.Le but de la recherche est d’étudier la théorie de la démonstration des logiques conditionnelles, en précisant leur calculs des sequents. Les calculs définis sont des extensions du calcul des sequents de Gentzen ; ils sont étiquetés, c’est à dire définis en enrichissant le langage, ou internes, qui rajoutent des connecteurs structurels aux sequents. La thèse est organisée en six chapitres. Le chapitre 1 présente les axiomes et la sémantique des logiques conditionnelles et le chapitre 2 introduit la théorie de la démonstration. Les contributions originelles au sujet sont traitées dans les chapitres 3– 6. Le chapitre 3 introduit des calculs de sequents étiquetés basées sur la sémantique de voisinage pour les logiques conditionnelles préférentielles. Le chapitre 4 présente différents systèmes internes de calcul pour les logiques counterfactuelles, une sous-famille des logiques préférentielles. Le chapitre 5 analyse la relation parmi les systèmes de preuve en présentant les deux cotés d’une traduction entre un calcul étiqueté et un calcul interne. Finalement, au chapitre 6, les méthodes de la théorie de la démonstration conditionnelle sont appliquées à une logique épistémique multi-agente.