Soutenance de thèse de Guillaume GEOFFROY

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 Gimel2, 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ù Gimel2 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 est complète pour Gimel2, 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 Gimel2 est élémentairement équivalente à B. Deux autres résultats montrent que Gimel2 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 Gimel2). 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.

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 Gimel2 is the Boolean algebra with to elements. This document defines new tools for studying realizability models and exploits them to derive new results. One such result is that, as far as first-order logic is concerned, the theory of Boolean algebras is complete for Gimel2, meaning that for each Boolean algebra B (with at least two elements), there exists a realizability model in which Gimel2 is elementarily equivalent to B. Next, two results show that Gimel2 can be used as a tool to study denotational models of programming languages (each one of them takes a particular denotational model and classifies its degrees of parallelism using Gimel2). Moving to set theory, another results generalizes Jean-Louis Krivine's technique of realizing the axiom of dependant 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.