Résumé
Vers 1870, Cantor démontre que le cardinal de l’ensemble ℝ des réels est strictement plus grand que celui de l’ensemble ℕ des entiers ; en d’autres termes, que l’infini continu (ℝ) est plus grand que l’infini dénombrable (ℕ). Il énonce l’hypothèse du continu (HC) : il n’existe pas de cardinal intermédiaire entre ℕ et ℝ. Cette conjecture restera longtemps ouverte, au point que Hilbert en 1901 en fait le premier de sa liste de 20 grands problèmes mathématiques. En 1938, Gödel montre que HC est cohérente avec la théorie des ensembles : on peut la prendre comme axiome car on ne peut pas démontrer sa négation. En 1964, Cohen établit que HC n’est pas démontrable car sa négation est cohérente. L’hypothèse du continu est donc indépendante de la théorie des ensembles.
Pour sa démonstration, Cohen a inventé une technique nouvelle de construction de modèles, le forcing, qui permet d’adjoindre à un modèle existant de nouveaux ensembles et de contrôler leurs propriétés via des approximations finies : les conditions de forcing. À partir de 2009, les travaux de Krivine, Miquel, Rieg, Jaber, Tabareau et Sozeau débouchent sur une toute autre présentation du forcing, internalisée en théorie des types sous forme de transformations de propositions et de leurs termes de preuve, dans le style des traductions doublement négatives du 4e cours. Ces transformations aident à imaginer le contenu calculatoire de la technique de forcing. Ainsi, le forcing intuitionniste tel que présenté par Jaber et al. peut se voir comme une transformation monadique, au sens du 5e cours, vers une monade d’entrées asynchrones où chaque terme peut à tout moment recevoir davantage de données provenant de l’extérieur.
En spécialisant les résultats précédents à des conditions de forcing qui sont juste des nombres entiers, on obtient une logique modale, appelée logique interne du topos des arbres par Birkedal et al., qui permet de définir des types récursifs généraux (non algébriques), tout en se plongeant par traduction dans la théorie des types. Cela rejoint les idées de step-indexing, objet du cours suivant.
