Réalisabilité classique : nouveaux outils et applications

Guillaume Geoffroy
I2M, Aix-Marseille Université
/user/guillaume.geoffroy/

Date(s) : 29/03/2019   iCal
14 h 00 min - 17 h 00 min

Soutenance de thèse


Réalisabilité classique : nouveaux outils et applications
La réalisabilité classique de Jean-Louis Krivine associe à chaque modèle de calcul et chaque modèle de la théorie des ensembles un nouveau modèle de la théorie des ensembles, appelé modèle de réalisabilité, d’une façon similaire au forcing. Chaque modèle de réalisabilité est muni d’une algèbre de Boole caractéristique gimel 2, dont la structure donne des informations sur les propriétés du modèle de réalisabilité. En particulier, les modèles de forcing correspondent au cas où gimel 2 est réduite à l’algèbre de Boole à deux éléments.

Ce travail présente de nouveaux outils pour manipuler les modèles de réalisabilité et donne de nouveaux résultats obtenus en les exploitant. L’un d’entre eux est qu’au premier ordre, la théorie des algèbres de Boole à au moins deux éléments est complète pour gimel 2, au sens où pour toute algèbre de Boole B (à au moins deux éléments), il existe un modèle de réalisabilité dans lequel gimel 2 est élémentairement équivalente à B. Deux autres résultats montrent que gimel 2 peut être utilisée pour étudier les modèles dénotationnels de langage de programmation (chacun des deux part d’un modèle dénotationnel particulier et classifie ses degrés de parallélisme à l’aide de gimel 2). Dans le domaine de la théorie des ensembles, un autre résultat montre que la technique de Jean-Louis Krivine pour réaliser l’axiome des choix dépendants à partir de l’instruction quote peut se généraliser à des formes plus fortes de choix. Enfin, un dernier résultat, obtenu en collaboration avec Laura Fontanella, accompagne le précédent en adaptant la condition d’antichaîne dénombrable du forcing au cadre de la réalisabilité, ce qui semble semble ouvrir une piste prometteuse pour résoudre le problème de la réalisation de l’axiome du choix complet.

Mots clés : Logique, réalisabilité classique, théorie de la démonstration, sémantique dénotationnelle, lambda-calcul.

Classical realizability: new tools and applications
Jean-Louis Krivine’s classical realizability defines, from any given model of computation and any given model of set theory, a new model of set theory called the realizability model,in a similar way to forcing. Each realizability model is equipped with a characteristic Boolean algebra (gimel2), whose structure encodes important information about the properties of the realizability model. For instance, forcing models are precisely the realizability models in which gimel 2 is the Boolean algebra with to elements.

This document defines new tools for studying realizability models and exploits them to de-rive new results. One such result is that, as far as first-order logic is concerned, the theory of Boolean algebras with at least two elements is complete for gimel 2, meaning that for each Boolean algebra B (with at least two elements), there exists a realizability model in which gimel 2 is elementarily equivalent to B. Next, two results show that gimel 2 can be used as a tool to study denotational models of programming languages (each one of them takes a particular denotational mode land classifies its degrees of parallelism using gimel 2). Moving to set theory, another results generalizes Jean-Louis Krivine’s technique of realizing the axiom of dependent choices using the instruction quote to higher forms of choice. Finally, a last result, which is joint work with Laura Fontanella, complements the previous one by adapting the countable antichain condition from forcing to classical realizability, which seems to open a new, promising approach to the problem of realizing the full axiom of choice.

Membres du jury :


Directeur
– Laurent Regnier – Professeur, Aix-Marseille Université
Rapporteurs
– Thomas Streicher (Technische Universität Darmstadt)
– Alexandre Miquel (Montevideo, Uruguay)

Examinateurs
– Mirna Dzamonja (U. East Anglia, Norwich, UK)
– Jean-Louis Krivine (Paris 7)
– Colin Riba (ENS Lyon)
– Nicolas Tabareau (INRIA, Nantes)
– Matteo Viale (Turin)

Liens :
theses.fr
Fiche de l’ED184

 

Emplacement
Campus St Charles, Marseille

Catégories



Retour en haut 

Secured By miniOrange