Est-il possible de comprendre les mathématiques classiques de ZF d’un point de vue constructif?

Peter Aczel

Le but du programme de Hilbert (PH) était d’amener à une réponse affirmative à une question de ce type lorsque “constructif” est remplacé par “finitiste”. Lorsque le PH fut conçu, la distinction entre ces points de vue n’était pas encore claire. Aujourd’hui nous concevons le finitisme comme un point de vue restreint, où les abstractions du constructivisme ne sont pas permises. A présent on admet, généralement, que les résultats d’incomplétude de Gödel montrent que le PH originel n’est pas réalisable. Des variants du PH ont été formulées, et une grande quantité de résultats ont été obtenus, spécialement en théorie de la démonstration, qui réduisent certains fragments des mathématiques classiques à des systèmes acceptables d’un point de vue constructif, ou même finitiste. Les techniques de la théorie de la démonstration ont été récemment raffinées —particulièrement par le travail de Michael Rathjen— à un point tel qu’on peut espèrer que certains de ses outils pourraient s’applique même à l’arithmétique du second ordre (PA_{2}). Mais, à cause de l’extrême complexité de ce travail et des doutes sur le caractére constructif des systèmes auxquels PA_{2} pourrait être réduit, on peut se démander si cette ligne de travail amène vraiement à une “compréhension” constructive des mathématiques classiques. Je veux poursuivre ici une autre direction.

Bien sûr, le problème est la complète imprédicativité de PA_{2} et des systèmes encore plus forts, tels que ZF. Dans cette conférence je discuterai le statut de l’imprédicativité dans le cadre de ma formalisation préférée des fondements des mathématiques constructives, la Théorie Constructive des Types (TCT) de Martin-Löf. Je reviendrai sur mon travail sur l’interpretation de la théorie constructive des ensembles CZF et certaines de ses extensions en théorie des types, et je discuterai les manières de renforcer TCT afin d’obtenir des systèmes capables d’interpréter ZF. La première approche, la plus crue, est de rajouter la loi du tiers exclu au traitement de Curry-Howard de la logique en TCT. Une deuxième approche, plus fine, consiste à rajouter à TCT une version de l’axiome de réducibilité de Russell et à utiliser la réduction, due à Friedman, de ZF à IZF par la double négation. Une troisième approche consiste à rajouter des axiomes pour une type imprédicatif Prop, comme dans le Calcul des Constructions de Huet-Coquand. Mais le problème reste encore ouvert de savoir si cette dernière extension est assez forte pour interpréter IZF, et donc ZF.

Enfin, je veux présenter des arguments montrant que la deuxième approche ouvre une voie plus cohérente que la ‘conception itérative classique’ pour comprendre ZF. Bien que cette approche ne soit pas complétement constructive, je crois qu’elle pourrait indiquer un chemin approprié pour obtenir une “compréhension” constructive des mathématiques classiques.

Address: Department of Computer Science, University of Manchester, Manchester M13 9PL, UK

E-mail: petera@cs.man.ac.uk