LA SATURATION

une nouvelle règle : si une proposition Y(x) (x étant une va-

riable de type 2) est vraie pour toute valeur numérique #

de x, on peut ajouter la généralisation I Y (x) aux axiomes. LA

Pour toute proposition de forme I YX(x) l’irréfutabilité (absence de contradiction avec les axiomes) entraîne alors la démonstrabilité : la saturation est bien atteinte, mais de façon factice : si la règle ne peut introduire de contradiction dans un système «-non contradictoire (1), elle détruit le formalisme en tant que tel (une démonstration n’est plus un dessin, ne s’effectue plus en un nombre fini de démarches). Les intuitionnistes l’admettent sans difficulté — elle exprime pour eux le seul sens du signe I — mais dans la mesure où il intègre l'infini à leurs raisonnements (suites libres de choix). Si l’on s’en tient à la Théorie de la démonsration, on ne peut « considérer comme définitive cette démarche » (2) ; elle seule pourtant pouvait sauver la saturation.

Pour les démonstrations de non contradiction. en revanche, le mal semblait moins irréparable ; GüDEL se défend d’avoir porté atteinte au point de vue de HILBERT : « Qu'il soit expressément noté que le théorème [précédent] (et les

(1) En revanche elle est inapplicable dans un système qui serait non contradictoire, mais w contradictoire comme le système vu plus haut lorsqu'on ajoute aux axiomes = p (Np). HILBERT n’a pas vu cette exception (Loc. cit.) parce qu’il considère non pas la non-contradiction en général, mais les méthodes utilisées jusque-là pour la démontrer, et croit encore à leur succès, c’est-à-dire à la possibilité de trouver un moyen pour « réduire » (c'est-à-dire transformer en démonstration arithmétique sans quantificateurs ni variables) toute démonstration formelle : le moyen donnerait alors le caractère de « vérité arithmétique intuitive » à une démonstration faite avec la nouvelle règle (si elle était représentable). Or c’est justement l’impossibilité d’un tel moyen universel de réduction que prouve le travail de GôDEL (s’il existait, tout système non contradictoire serait w-non contradictoire, puisque = pu Y (x) réduit donnerait - Y (n) (x étant un nombre quelconque),

donc ne serait pas proposition démontrable — ou axiome — % (#) l'étant pour tout #).

(2) BERNAYS, ibid.

FINITISME ET INTUITIONNISME 153

résultats correspondants...) ne sont en aucune façon en contradiction avec le point de vue formaliste de HILBERT. Car celui-ci suppose seulement l'existence d’une démonstration de non contradiction conduite avec des moyens finis et il serait concevable qu'il y ait des démonstrations finies qui ne se laissent pas formaliser dans P [le système des Principra ou les systèmes analogues satisfaisant aux conditions 1 et 2] » (1). Le théorème ne donne qu’un critère négatif, portant à la vérité contre les méthodes (combinatoires) employées jusque-là. Mais comment élargir la notion de raisonnement fini ? HERBRAND en avait donné la définition la plus précise : « on n’y considère qu’un nombre fini déterminé d'objets et de fonctions ; les définitions de celles-ci permettant de calculer leur valeur d’une manière univoque ; on n'affirme jamais l'existence d’un objet sans donner le moyen de le construire ; on n’y considère jamais l’ensemble de tous les objets x d’une collection infinie ; et quand on dit qu’un raisonnement est vrai pour tous les x, cela signifie que pour chaque x pris en particulier, il est possible de répéter le raisonnement général en question » (2). L’indétermination ne subsiste plus qu’à propos de la construction : on peut la concevoir comme une progression d'étapes chacune finie au sens précisé plus haut. II n’y a plus moyen d’embrasser du regard toutes les démarches — la conscience cesse d’être coextensive à leur succession, elle est du moins présente en chacune d'elles. On passe de la mathématique intuitive à la mathématique intuitionniste. Aussi bien HiL- BERT avait-il admis cette parenté entre la métamathématique et l’intuitionnisme dans la réponse qu'il faisait à celui-ci ; et BROUWER avait tenté de la préciser (*). Après le

(1) GÔDEL, loc. cit., p. 197.

(2) HERBRAND (IV), p. 3.

(3) L'accord se faisait sur les points suivants : a) « distinction entre l' éaification formelle des mathématiques et la théorie intuitive des lois de cette

154 TRADUCTION GÔDEL-GENTZEN

résultat de GôDEL il était naturel de chercher de ce côté : simultanément G6DEL d’une part (:), BERNAYS et GENTZEN d'autre part (?), réussirent une traduction de l'arithmétique classique dans l’arithmétique intuitionniste (formalisée par HEYTING) (°) : si les démarches de celle-ci sont inattaquables, la non contradiction de l’arithmétique classique est par là même prouvée (puisque toute proposition démontrable A À — A, par exemple, aurait sa traduction dans le système intuitionniste). GLIVENKO (‘) avait, en effet, déjà montré que toute expression du calcul classique des propositions construite avec les seuls signes — et A, si elle est valable dans ce calcul, est aussi démontrable dans le calcul intuitionniste. Il suffit donc de mettre toute proposition sous cette forme. Aïnsi le tiers exclu X V — YX devient — (— AA — - X). Comme on voit, l'interprétation seule diffère, mais il n’y a pas plus de propositions démontrables. En mathématique on admet (5) évidemment le tiers exclu

édification — avec reconnaissance que pour cette théorie la mathématique intuitionniste de l’ensemble des entiers est indispensable » ; b) « rejet de l’utilisation irréfléchie du tiers exclu... et sa limitation aux systèmes finis » ; c) « identification du tiers exclu avec le principe de la résolubilité de tout problème mathématique » ; d) « reconnaissance que la justification de la. mathématique formelle par la démonstration de non contradiction contient un cercle vicieux parce que cette justification repose sur l'application intuitive du tiers exclu (que de la non contradiction d’une proposition sa validité découle) ». BROUWER (VI). — Les affirmations c) et d) n’ont pas de sens pour HILBERT : la résolubilité de tout problème mathématique est un principe: régulateur de la métamathématique (préside à la constitution de nouveaux systèmes), le tiers exclu principe constitutif de la mathématique formalisée. Quant à la justification, elle n’a pas de rapport avec la preuve de validité d'un formalisme (propriété qui ne saurait convenir qu’à une proposition à l’intérieur d’un formalisme). On a vu les deux sens de la justification chez HILBERT et chez VON NEUMANN. Cf. là-dessus le commentaire de HEYTING (EV), p. 54-56.

(1) GÔDEL (III).

(2) Cf. BERNAYS, loc. cit., p. 212. .

(3) HEYTING (I), p. 42-50.

(4) GLIVENKO (I), p. 183-188.

(5) HEYTING (IT), p. 57-71.