Ecole Doctorale

Mathématiques et Informatique de Marseille

Spécialité

Informatique

Etablissement

Aix-Marseille Université

Mots Clés

Théorie de la démonstration,Logiques conditionelles,Logiques modales,Logiqes epistemiques,

Keywords

Proof Theory,Conditional logics,Modal logics,Epistemic logic,

Titre de thèse

Théorie de la démonstration des logiques conditionnelles
On the proof theory of conditional logics

Date

Vendredi 8 février 2019 à 10:00

Adresse

Campus Saint Charles 3 place Victor Hugo, 13003 Marseille (France) Amphithéâtre de Science Naturelles

Jury

Directeur de these M. Nicola OLIVETTI Aix-Marseille University
Rapporteur M. George METCALFE Mathematisches Institut - University of Bern
Rapporteur Mme Sonja SMETS Institute of Logic, Language and Computation, University of Amsterdam
CoDirecteur de these Mme Sara NEGRI Faculty of Arts, University of Helsinki
Examinateur M. Luigi SANTOCANALE Aix-Marseille Université
Examinateur M. Didier GALMICHE Université de Lorraine
Examinateur M. Philippe BESNARD Université Paul Sabatier
Examinateur Mme Heta PYRHöNEN Faculty of Arts - University of Helsinki

Résumé de la thèse

La thèse se place à l'intersection de trois thèmes de recherche : logique conditionnelles, théorie de la démonstration et sémantique de voisinage. En general, les logiques conditionnelles sont des systèmes formels qui représentent une forme de conditionnalité plus affiné que l'implication matérielle de la logique classique. Dans cette thèse on s’intéresse à l'analyse des logiques conditionnelles définies au moyen d'un opérateur modal à deux places qui, selon le système, peut se lire comme un contrefactuel, comme exprimant une inférence non-monotone, ou une forme de croyance conditionnelle. Cet approche modale aux logiques conditionnelles a été introduit par Robert Stalnaker et David Lewis. Dès leur ouvrages, ces systèmes ont été diffusément étudié, pour la plupart d'un point de vue sémantique ; jusqu'à des temps récents, peu était connu sur la théorie de la démonstration de ces systèmes. La théorie de la démonstration est la discipline qui étudie les preuves en tant que objets (démonstrations) dans systèmes formels. On s’intéresse ici au calcul des sequents, un formalisme particulièrement riche et expressif introduit par Gerhard Gentzen. La sémantique de voisinage est une sémantique topologique dont les modèles sont constitués par des éléments (les mondes possibles) groupés en voisinages. Les modèles de voisinage sont plus expressifs que les modèles de Kripke, et peuvent être utilisés pour définir d'une façon modulaire et efficace la sémantique d'une grande famille logiques conditionnelles (et modales). L'objectif de cette thèse est d'étudier la théorie de la démonstration des logiques conditionnelles. En particulier, on s’intéresse à la logique conditionnelle PCL (Preferential Conditional Logic) et à la logique conditionnelle V (logic of Variably strict conditionals, Lewis). On présente des systèmes de preuve originaux, dans la forme de calcul de sequents, pour PCL, V et leur extensions. Les systèmes de preuve qu'on introduit peuvent être qualifiés comme extensions standard du calcul des sequents proposé par Gentzen pour la logique classique propositionnelle. Standard signifie que les calculs sont composés par un nombre fini et fixé de règles, chacune avec un nombré fini et fixé de permises. En plus, les calculs des sequents présentés sont classés soit comme étiquetés soit comme internes. Les calculs étiquetés enrichissent le langage du calcul avec des variables syntactiques, les étiquettes (labels), qui représentent les éléments de la sémantique. Içi on utilise la sémantique de voisinage. Les calculs internes, au contraire, enrichissent la structure des sequents en ajoutant des connectives méta-théorétiques. La thèse est organisé sen six chapitres. Le chapitre 1 présente les logiques conditionnelles, avec une discussion des principaux axiomes et systèmes de sémantique. Dans le chapitre 2 on introduit les calculs des sequents pour la logique propositionnelle et pour certaines logiques modales. Les chapitres 3, 4, 5 et 6 représentent des contributions originelles au sujet. Le chapitre 3 introduit une famille de calculs de sequents étiquetés basée sur la sémantique de voisinage. Ces calculs capturent d'une façon modulaire la logique PCL et tous ses extensions, y compris V. Le chapitre 4 est dédié aux systèmes de preuves internes ; différents calculs de sequents pour V et ses extensions y sont présentés. Le chapitre 5 analyse la relation entre systèmes de preuve étiquetés et internes pour logiques conditionnels. Enfin, le chapitre 6 étudies un système de logique conditionnelle qui, dans sa version multi-agente, exprime la notion épistémique de croyance conditionnelle (CDL, Conditional Doxastic Logics). Pour cette logique, un calcul des sequents étiqueté est introduit, toujours basé sur la sémantique de voisinage. Ce chapitre contient donc une application des méthodes développés pour les logiques conditionnelles au domaine des logiques épistémiques et multi-agentes.

Thesis resume

This thesis can be ideally placed at the intersection of three research topics: conditional logics, proof theory and neighbourhood semantics. Generally speaking, conditional logics are formal systems apt to represent a kind of conditionality more fine-grained than classical material implication. In the present work we analyse conditional logics defined as extensions of classical propositional logic by means of a two-place modal operator which, depending on the logic under scope, can be read as a non-monotonic inference, as a counterfactual or as expressing a form of conditional belief. This modal approach to conditional logics was initially devised by Robert Stalnaker and David Lewis. Since their work these systems have been widely studied, mainly from a model-theoretic viewpoint; until recent years, however, little was known about their proof theory. Proof theory is the discipline which studies proofs within formal systems as mathematical objects (derivations). We are concerned with sequent calculus, a particularly rich and expressive formalism introduced by Gerhard Gentzen. Neighbourhood semantics is a topological semantics particularly relevant for our purposes. These models are constitued of elements (the possible worlds) grouped into neighbourhoods. Neighbourhood models are more expressive than Kripke models, and can be employed to define in a modular way the semantics of a wide family of conditional logics, as well as modal logics. The aim of this thesis is to investigate the proof theory of conditional logics. In particular, we consider conditional logic PCL (Preferential Conditional Logic) and conditional logic V (logic of Variably strict conditionals, Lewis). We present original proof systems in the form of sequent calculi for both PCL, V and their families. The introduced proof systems are standard extensions of Gentzen’s propositional calculus, where standard means that the systems are composed of a finite number of rules, each displaying a fixed finite number of premisses. Moreover, the calculi are either labelled or internal. Labelled calculi enrich the language by means of syntactic variables, the labels, representing elements of the model – in our case, neighbourhood semantics. Internal calculi enrich the structure of sequents by introducing additional meta-theoretic connectives. The thesis is organized in six chapters. Chapter 1 offers a presentation of conditional logics, along with a discussion of relevant axioms and semantics. Chapter 2 introduces sequent calculi for propositional and modal logics. Chapter 3, 4, 5 and 6 represent original contributions. Chapter 3 introduces a family of labelled sequent calculi based on neighbourhood models that captures in a modular way PCL and its extensions, including Lewis’ family of conditional logics (V and its extensions). Chapter 4 is devoted to internal proof systems for Lewis’ logics: it presents different families of sequent calculi for logic V and some of its relevant extensions. Chapter 5 analyses the relationship between labelled and internal proof systems for conditional logics. Finally, Chapter 6 studies a system of conditional logic which, in its multi-agent version, is suitable to express the epistemic notion of static conditional belief (CDL, Conditional-Doxastic Logic). For this logic, a labelled sequent calculus is introduced, again based on neighbourhood models. Thus, the chapter contains a application of the proof-theoretic methods developed for conditional logics in an epistemic and multi-agent setting.