Spécialité : Informatique
Laboratoire : LIPN
Directeur de thèse : Damiano Mazza
Réalisabilité et interprétation calculatoire de l’axiome du choix
Dans ma thèse, j’explore l’axiomatisation des mathématiques à travers l’informatique. Mon objectif principal est de découvrir un équivalent computationnel de l’Axiome du Choix, un principe fondamental des mathématiques du quotidien. Pour ce faire, j’utilise une technique récente appelée réalisabilité, qui nous permet d’associer des théorèmes mathématiques à des programmes, appelés réalisateurs. Cette méthode a été initialement développée dans les années 1940 par Stephen Cole Kleene, un pionnier des mathématiques constructives, pour l’étude de l’arithmétique. Elle a ensuite été adaptée par Jean-Louis Krivine à la théorie des ensembles classique, une axiomatisation mathématique largement acceptée. Au cours des deux dernières décennies, Prof. Krivine a réalisé plusieurs avancées en associant des programmes aux axiomes de cette théorie. Récemment, il a démontré l’existence d’un algorithme lié à l’Axiome du Choix. Cependant, le programme explicite n’a pas pu être extrait de la preuve. L’objectif ultime de ma thèse est de présenter un réalisateur explicite pour cet axiome. Cette démarche promet d’améliorer notre compréhension de ce principe mathématique essentiel.
Realizability and computational interpretation of the Axiom of Choice
In my thesis, I investigate the axiomatization of mathematics through the lens of computer science. My primary objective is to uncover a computational counterpart to the Axiom of Choice, a significant principle in everyday mathematics. To achieve this, I employ a recent technique known as realizability, which allows us to associate mathematical theorems with programs, referred to as realizers. This method was originally developed in the 1940s by Stephen Cole Kleene, a pioneer in constructive mathematics, for the study of arithmetic. It was later adapted by Jean-Louis Krivine for classical set theory, a widely-accepted mathematical axiomatization. Over the past two decades, Prof. Krivine has achieved several breakthroughs by associating programs with axioms of this theory. Recently, he demonstrated the existence of an algorithm linked to the Axiom of Choice. However, the explicit program could not be extracted from the proof. The ultimate goal of my thesis is to present an explicit realizer for this axiom. This endeavor holds the promise of enhancing our comprehension of this pivotal mathematical principle.