LE TIERS EXCLU INOFFENSIF

ter de contradiction dans un système d’axiomes déjà non contradictoire. Si, par exemple, I — X (x) mène à une absur- La

dité, en essayant de satisfaire progressivement la proposition dans un champ (où les axiomes de la théorie sont déjà satisfaits) on sera arrêté à un certain ordre, c'est-à-dire que l’on rencontrera un individu ? pour lequel X (2) est vrai (pour le système des valeurs logiques attachées au champ). Or toutes les démarches pour satisfaire une proposition dans un champ sont soumises aux conditions de l’intuitionnisme (elles sont même finies au sens HERBRAND) : celui-ci atteint donc le résultat > YX (x) que procurait le tiers exclu, simple

raccourci.

De même pour les axiomes d’e : dans le cas simple où on n’introduit qu’une seule fonction :, on voit qu'il est toujours possible de déduire des valeurs logiques attachées au champ I (où est satisfaite la conjonction : X, A % À … AY, des autres axiomes) un système de valeurs (définissant un champ IT) telles que

LA.AU AB(G)+B(sB(x)j (1

(où 2 est un individu) soit toujours vrai. Si 3 (x) n’est pas toujours vrai dans le champ primitif I (sans quoi il suffirait de conserver celui-ci), on remplace partout z par l'individu 7; du champ I d'ordre # pour lequel (;) est faux (1) ; on obtient alors une satisfaction de la conjonction (1) dans le champ I d'ordre 2n (l’ordre du champ est doublé puisque 2 était unindividu d’ordre o et que est d'ordre #; on voit que # (1) devient 8 (1) donc est faux). Les propositions élémentaires où intervenait ? se transforment en propositions portant sur des individus du champ I : il suffit de leur attribuer comme valeurs logiques celles qu’elles reçoivent ainsi transformées, pour satisfaire (1) dans le nouveau champ II. -— S'il est inof-

(x) L'ordre du champ où est satisfaite une proposition est le numéro du stade de l'opération progressive de satisfaction (v. ci-dessus p. 133).

DÉMONSTRATION GENTZEN 157

fensif l’axiome introduisant « est d’ailleurs inefficace : il ne permet pas de décider une proposition € qui ne pouvait l'être sans lui. En effet, puisque les valeurs logiques du champ II sont déterminées par celles du champ I, à chaque étape de la construction de celui-ci, les deux systèmes de valeurs satisfaisant également les axiomes et dont l’un rend € vrai et l’autre faux, déterminent pour II deux autres systèmes produisant le même résultat. La fécondité des < n’apparaît que lorsqu'ils portent sur le type 2 (ou supérieur), c'est-à-dire quand la construction finie des champs n’est plus possible.

La possibilité d’une traduction directe dans la mathématique intuitionniste — si elle manifeste l’ineffcacité des interdictions de celle-ci (quand on s’en tient au type 1), — ne peut donc procurer une démonstration de non contradiction. D'une part il n’y a pas d’extension possible à l’analyse, d'autre part pour la théorie des nombres (avec axiome général d’induction complète) la garantie de l'évidence intuitionniste paraît insuffisante si l’on s’en tient au point de vue hilbertien avec ses exigences finitistes telles que HER- BRAND les formule. La traduction GüDEL met d’ailleurs en lumière un point faible de la doctrine intuitionniste, qui mêle comme sources de certitude évidence intuitive et raisonnements logiques ; s’il y a un critère absolu il doit être unique, si c’est l’intuition on ne doit pas pouvoir, par exemple, appliquer le signe d’absurdité à des propositions générales.

GENTZEN (1) définit un constructionnisme en des termes assez voisins de ceux dont se servait HERBRAND : on peut dépasser le fini à condition de ne considérer jamais des collectivités « en soi », mais des moyens réglés d’engendrer tou-

(1) GENTZEN (Il), p. 520.

158 DÉMONSTRATION GENTZEN

jours de nouveaux individus dans un système caractérisé (et n’existant que) par ces procédés de construction. Ainsi pour la suite des entiers. C’est le rôle de cet infini potentiel de donner aux procédés métamathématiques à la fois une puissance suffisante et une sécurité plus grande que celle des formalismes examinés. À moindres frais on ne peut agir, et son intervention — telle que la conçoit GENTZEN — a l'avantage de localiser difficultés et doutes en un seul point, lorsqu'elle apparaît sous forme d’une induction transfinie, d’ailleurs rigoureusement limitée à un segment des nombres de la classe IT. Il est à priori plausible que la méthode puisse réussir puisqu’à chaque étape d’un raisonnement mathématique classique on ne considère jamais qu’un nombre fini d'objets, individus, concepts, résultats de raisonnements antérieurs : GENTZEN en donne une preuve détaillée pour la théorie des nombres complète.

Pour toute démonstration valable dans ce formalisme et mise sous une certaine forme canonique, il établit que : 10 il existe une opération de réduction bien déterminée (quoique comportant dans certains cas nécessairement une infinité de modalités différentes d'actualisation) qui la transforme en une nouvelle démonstration également valable et de forme également canonique ; 20 après un nombre fini de semblables réductions, la conclusion de la démonstration devient une proposition triviale (dans l’arithmétique intuitive sans variable) ; 3° seules les démonstrations valables jouissent des propriétés 1 et 2. La non-contradiction de l’arithmétique classique est donc assurée.

Les opérations de réduction consistent dans une sorte de démantèlement de l'architecture logique des propositions. En arithmétique tous les prédicats numériques sont immédiatement décidables, immédiatement calculables toutes les fonctions après substitution d’entiers déterminés aux variables ; le premier pas consistera donc à remplacer partout les variables libres par des nombres (avec bien entendu

DÉMONSTRATION GENTZEN 159

exception pour les variables portantes, lorsque dans la démonstration figurent une généralisation ou une induction complète). — GENTZEN introduit pour définir sa forme canonique les notions de séquence et d’intersection. La séquence élargit l'implication : « avec les hypothèses À, 5, CE, on a pu démontrer : D»