Jean-Louis Krivine (PPS)

Réalisabilité classique et théorie des ensembles

Résumé: Tous les résultats de consistance relative en théorie des ensembles ont été obtenus en construisant des modèles de ZF, à partir d'un modèle donné, par deux méthodes:

1. Les "modèles intérieurs", dont le plus connu est l'univers constructible (Gödel, 1940)
2. Le "forcing" (Cohen, 1963)

Ces deux constructions ne changent pas la classe des ordinaux du modèle initial.

La technique de "réalisabilité classique", mise au point pour étudier la correspondance preuves-programmes, se révèle être un troisième méthode, qui donne des modèles de ZF complètement différents. En particulier, les ordinaux - et même les entiers - sont changés.

On montre, de cette façon, un résultat de consistance relative qu'on ne peut obtenir par les méthodes usuelles, concernant le "choix dépendant" et de curieuses propriétés de R.