Réalisabilité et forcing généralisé en théorie des ensembles

Jean-Louis Krivine

La fameuse correspondance de Curry-Howard entre les preuves et les programmes fut initialement découverte pour une logique très restreinte : le système des types simples, basé sur la logique propositionnelle intuitionniste, avec → pour seul connecteur. J.-Y. Girard l’a étendue, en 1970, à la logique intuitionniste du second ordre, sous le nom de système F. Le lien avec les langages de programmation fut établi par J. Reynolds.

En 1990, cette correspondance fut étendue à la logique classique, à la suite de Felleisen et Griffin qui s’aperçurent que la loi de Peirce correspondait aux instructions de contrôle des langages de programmation fonctionnels. Depuis lors sont apparus bien des systèmes de types pour étendre la correspondance de Curry-Howard à la logique classique du second ordre. Restait le problème d’étendre cette correspondance à la théorie des ensembles de Zermelo-Frænkel en logique classique ; c’est le sujet du présent exposé.

Pour ce faire, on construit inductivement des modèles de réalisabilité, comme dans la construction bien connue du forcing. On montre que chaque axiome de ZF (sauf l’axiome du choix) est alors réalisé ; on obtient ainsi un système de types dans lequel on peut formaliser toutes les preuves de théorie des ensembles, et en extraire des programmes qui sont des termes d’un λ-calcul étendu avec des instructions de contrôle. Dans ce système, la propriété de normalisation est “ essentiellement vraie ”, dans le sens où l’on obtient des calculs corrects sur les types de données. Bien entendu, il est faux que tout terme typé soit normalisable, puisque, par exemple, l’opérateur de point fixe Y est typé par l’axiome de fondation.

Cette construction est effectivement une généralisation du forcing, les modèles de réalisabilité étant l’analogue des modèles Booléens du forcing usuel. Comme on travaille en logique classique, il est ensuite facile de les transformer en modèles ordinaires de ZF. Les modèles ainsi obtenus sont des objets assez fascinants, qui sont profondément différents des modèles de forcing. Ils posent beaucoup de problèmes intéressants. Tout d’abord, ils ont toujours des entiers non standard (sauf dans un “ cas dégénéré ”, qui est le forcing usuel), et ce ne sont donc pas des extensions finales du modèle original de ZF C. De plus, bien que je ne l’aie pas encore démontré, il est très vraisemblable qu’ils ne satisfont jamais l’axiome du choix.

J.-L. Krivine. Typed lambda-calculus in classical Zermelo-Frænkel set theory. To appear in Archiv for Math. Logic.

Preprint at www.logique.jussieu.fr/www.krivine.

Address: Université Paris VII, Paris, France

E-mail: krivine@logique.jussieu.fr