Le contenu calculatoire de la théorie des ensembles – COCONTENS

COCONTENS est un projet interdisciplinaire qui combine techniques de théorie des ensembles et d’informatique théorique.
L’objectif principal du projet est d’étudier le contenu calculatoire de la théorie des ensembles à travers la réalisabilité. La réalisabilité est une branche de la logique qui vise à extraire le contenu calculatoire des théories mathématiques en établissant une correspondance formule-programmes (ce procès est au cœur de l’extraction de programmes dans les assistants de preuves tels que Coq). Inventée par Kleene dans le cadre de la recherche sur le constructivisme, la réalisabilité a évoluée jusqu’à englober d’abord la logique classique, puis la théorie des ensembles, ZF, grâce aux travaux de J-L Krivine. La technique de Krivine généralise la méthode de Forcing et nous permets d’extraire le contenu calculatoire de la théorie ZF. Si cette méthode fonctionne bien avec ZC, l’Axiome du Choix, AC, est plus problématique. En 2003, Krivine montra qu’on peut réaliser une version non extensionnelle de AC en considérant l’instruction `quote’ de LISP, cela lui permit de réaliser le Choix Dépendant, DC, qui corresponds à une version dénombrable d’AC. En suite, Fontanella et Geoffroy montrèrent qu’il est possible de réaliser également des versions non dénombrables d’AC en considérant des programmes qui généralisent `quote’. Dans un article très récent (Jan 2021), Krivine montre qu’il y a un modèle de réalisabilité pour l’AC complet, néanmoins il n’est pas clair dans ce modèle quel programme réalise AC. En continuation avec ces résultats, ce projet est centré sur 3 objectifs principaux:
1. Extraire le contenu calculatoire de AC en individuant un programme qui le réalise
2. Extraire le contenu calculatoire d’autres axiomes ou principes dont la cohérence avec ZF se montre par Forcing (ex. CH, notCH, MA…)
3. Extraite le contenu calculatoire d’autres axioms dont la cohérence avec ZF se montre par des modèles internes (ex. V=L)