LIMITATION DES MÉTHODES

n'apparaît que l'addition comme fonction mathématique : lorsque ®x est ainsi constitué, l’axiome général est alors déduisible à partir de l’axiome élémentaire. Ainsi se manifeste que l’axiome d’induction totale n’accroît le formalisme que dans la mesure où la proposition sur laquelle il porte est impossible à y décider : mais alors la méthode des champs est aussi impuissante à démontrer sa non contradiction.

Il est assez remarquable que toutes ces démonstrations de non contradiction, quoique portant sur des formalismes d’ampleurs différentes, échouent également devant l’axiome général d’induction complète. Là pourtant, dit HILBERT, «se trouve la véritable source du concept de variable mathématique » (:), l’irréductible intervention de l'infini : la métamathématique n’est efficace que si elle l’atteint. Mais alors s’impose une comparaison — qu'écartait la distinction trop tranchée de science et métascience — entre la puissance des moyens mis en œuvre dans la théorie fondée et par la théorie qui fonde. L’induction complète élémentaire joue le rôle essentiel pour von NEUMANN et pour HER- BRAND : chez l’un 1l y a double induction, sur le nombre des symboles 5, I, < dont les subordinations mutuelles donnent un système fini de matrices, et sur les substitutions dans chaque matrice des formules déjà réduites, chez l’autre il y aussi bien induction pour la construction progressive des champs que pour celle des propositions dont la négation est impossible à satisfaire. En quoi ces démarches se distinguent-elles des démarches licites dans les formalismes qu’elles fondent ? HILBERT s'était contenté d’une délimitation extrinsèque de la zone intuitive : les raisonnements arithmétiques qu’il y autorisait étaient simplement

(x) HizsErT (XIII), p. 321. /

144 THÉORÈME DE GÔDEL

signalés au passage dans l’indivisible mouvement de la pensée concrète, sans que soit envisagé pour celle-ci un essai de codification de procédés par essence imprévisibles. Mais les exemples précédents montrent que leur utilisation se trouve déterminée par la matière à laquelle ils s'appliquent. D'où l'essai à la fois de préciser ce rapport et, pour atteindre le formalisme complet au moins de la théorie des nombres, d'enrichir la notion de raisonnement en termes finis, borné jusque-là à des considérations de combinatoire. A la première question répond le théorème de GÔDEL (1) — avec le critère négatif qu’il fournit —, à la deuxième la dernière démonstration de non contradiction tentée par GENTZEN.

L'idée d’une systématisation — au besoin d’une formalisation — de démarches de la métascience se trouve déjà, par exemple, dans les travaux de l’école polonaise (2) qui superpose langue et métalangues — en échelle indéfinie — chaque degré contenant la syntaxe (c’est-à-dire axiomes et règles d’enchaînement) du degré immédiatement inférieur. Mais on va de systèmes moins riches à systèmes plus riches, les subsumant : de leur considération ne peut résulter aucune solution pour le problème du fondement tel que le pose HYLBERT. L'originalité de GÜDEL est d’avoir effectué l’opération inverse, en essayant de déterminer ce qui, des procédés de la métalangue, peut être formalisé dans la langue. L'entreprise procure ainsi une analyse de la notion brute de raisonnement intuitif. En prenant comme langue l’arithmétique ordinaire, on peut coordonner de façon biunivoque aux nombres entiers tout le matériel symbolique, grâce à l'unicité de décomposition d’un nombre en ses facteurs premiers : les signes logiques (constantes, variables) sont repré-

(x) GÔDEL (IT), p. 173.

(2) Lukasrewicz et surtout TARSKI qui a fait un historique et un exposé systématique de ses travaux (indépendants de ceux de GÔDEL et en partie antérieurs), in TarskI (IV). Cf. aussi CARNAP (IV).

THÉORÈME DE GÔDEL 145

sentés par des nombres (leurs numéros) ; les formules ou suites de signes et les raisonnements ou suites de formules, par le produit des # premiers facteurs premiers affectés comme exposants des nombres (numéros) correspondant aux signes — ou formules — de la suite. La coordination est évidemment biunivoque (1). Dès lors les concepts et les relations de la métascience deviennent des concepts et des relations arithmétiques, ils portent sur les numéros des formules. Il est possible d’en codifier la définition grâce au schéma de la récurrence ordinaire (2) : on voit que les fonctions de vérité du calcul des propositions (+ V, À, -) se transforment immédiatement en fonctions récurrentes si l’on remplace les propositions par des nombres. Pour les principales propriétés ou relations métamathématiques, GÔDEL donne l’exemple effectif de leur traduction arithmétique : pour un signe, figurer dans une formule sera « être l’exposant du #*”* terme dans le produit de facteurs premiers représentant la formule » ; aux axiomes correspondent des numéros calculables, être un axiome sera donc la fonc-

(1) GÔDEL coordonne aux signes :

IV (re), ester © respectivement les numéros :

5 7 9: 11,13, 3€t1 Toute variable de type # est représentée par un nombre premier > 13 élevé à la puissance n. La formule Il #s (#3) qu'il écrit #3 I (#2) X4 aura donc pour numéro, déterminé de façon univoque, le produit : 217,39. 511,719? 1118.

(2) On appellera fonction récurrente toute fonction obtenue soit par substitution dans une fonction récurrente déjà définie d’autres fonctions aussi définies — soit grâce au schéma suivant :

fo)=e f(n+1) = 4% (x, f(") e et à étant des fonctions récurrentes déjà introduites. Les fonctions récurrentes forment donc une suite bien ordonnée, la 1r€ étant l’addition (définie grâce à la fonction du suivant). Une relation récurrente est une équation entre fonctions récurrentes.

146 THÉORÈME DE GÔDEL

tion de disjonction entre eux ; de même pour la proposition 4, être «conséquence immédiate » d'une proposition b (par application des règles d’implication ou de généralisation) sera relation récurrente entre le nombre de a et celui de b; être un «dessin démonstration » est pour un nombre la propriété de se décomposer en facteurs premiers dont chacun a pour exposant le nombre correspondant à un axiome ou à une proposition conséquence immédiate d’une proposition dont le nombre est exposant d’un des facteurs précédents. « Etre enfin une démonstration x pour une proposition y » (en abrégé xDy) est, entre deux nombres, la relation que dans le développement du premier, x — qui possède déjà la propriété «être un dessin démonstration » — le dernier facteur a pour exposant le second y. Toutes ces relations sont rigoureusement récurrentes — au sens précisé plus haut — d’où la double conséquence : qu’elles appartiennent bien à la métamathématique finie, puisqu’étant donné le ou les nombres sur lesquels elles portent, on peut constater par un calcul fini si elles sont ou non vérifiées par eux, d'autre part qu’elles peuvent être formalisées dans un système exprimant l’arithmétique. Pour le système des Principia mathematica — dont le matériel symbolique est supposé préalablement numérisé par les procédés indiqués plus haut — GÔDEL précise la 2° conséquence en démontrant le fhéorème I : à toute relation récurrente R (x, x … x,) de l’arithmétique ordinaire entre les nombres %,% ... %, Correspond dans le système formel un nwméro (de signe) 7 tel que, si on remplace dans son développement en facteurs premiers les exposants représentant les variables par les numéros des nombres (1) Ka, La Xs JA vérité == où la fausseté =— arithmétique de KR(%, %X2 .… %,) entraîne pour 7 ainsi transformé —— ou pour sa négation — l'existence d’une démonstration formelle

(1) Les nombres ordinaires sont exprimés dans un système comme celut des Principia par une formule: par exemple 4 s'écrit ssss o. Dans le système numérisé, 4 aura donc pour numéro 2%.3%.5%.7%.II1

THÉORÈME DE GÔDEL 147

dans le système. C’est évidemment la conséquence du fait que les axiomes du système considéré permettent de décider pour toute relation arithmétique récurrente entre # nombres si elle est vraie ou non (1). On peut l'écrire en abrégé sous forme de la double implication sntuitive (2) (il ne s’agit de rien de formel puisque nous mettons en rapport une expression d’arithmétique ordinaire avec une expression appartenant à un système formel) :

(1) R(%:...%:) 3 Démonstrabil. 7 (Nx,...Nx,) (2) © R(x...x) 2 Démonstrabil. de Nég. r (Nx,...Nx,)

La propriété Démonstrabil., étant une propriété du numéro (transformé par la substitution), est une des relations de la métalangue définies plus haut comme relation arithmétique récurrente, donc à son tour exprimable dans la langue. Ceci posé, considérons la relation «x n’est pas une démonstration pour la proposition y à une variable lorsqu'on fait celle-ci égale au numéro (*) du nombre y » ; en abrégé :

(3) © x D (Ny)

C’est comme on l’a vu une simple relation arithmétique

(1) GôDEL (IT), p. 186 n. La démonstration exacte «ne présente pas de difficulté de principe, ajoute-t-il, mais est assez compliquée » — il se contente de l’esquisser dans son mémoire en procédant par induction complète pour des relations récurrentes de la forme #3 = + (#1...#n) (9 étant une fonction récurrente).

(2) Pour éviter toute confusion nous employons des signes spéciaux (qui sont de simples abréviations) : 2 pour implique, © pour la négation, (x), pour exprimer: pour tout x. Enfin à droite de l'implication (1), où il s’agit de notions de la métalangue, Nx signifie le numéro du nombrex et r (Nx,... Nan): le numéro qu’on obtient pour 7 lorsqu'on a substitué aux numéros des variables les numéros Nx,, Nxo, .… Nxn.

(3) y est dans le formalisme considéré un numéro : celui-ci comme nombre entier est représenté à son tour dans le formalisme par une formule qui a pour numéro Ny : on voit ici la traduction de la syntaxe (désignation de la formule y) dans la langue. La théorie des types est respectée: y est une variable de type 2 (on la représentera par un nombre premier à là puissance 2) mais Ny est un individu de type 1 qui peut donc figurer dans y comme argument.

148 THÉORÈME DE GÔDEL

récurrente entre les nombres x et y. Elle entraîne, d’après le théorème précédent, pour elle (ou sa négation) la démonstrabilité dans le système d’une proposition (en signes du système) 7 (Nx, Ny) (ou de sa négation). Soit p le numéro de la généralisation de 7 par rapport à la première variable ; si nous substituons p à y, le théorème I nous donne les deux implications intuitives :

x D p(Np) 5 Démonstrabil. de Neg 7 (Nx, Np) (5)

S'il existait une démonstration x pour la généralisation de 7(Np) par rapport à la première variable, c’est-à-dire p(Np), on aurait en même temps dans le système en vertu de (5) une démonstration de la négation de(Np) pour la valeur Nx de la 1re variable : le système serait contradictoire. La non contradiction du système entraîne l'impossibilité d’y démontrer p(Np) : la proposition p(Np) a d’ailleurs pour sens — d’après les définitions données — l'affirmation de sa propre indémonstrabilité (il n’y a pas de démonstration pour la proposition numéro p, lorsqu'on y fait la variable égale au numéro de cette proposition) : elle est intuitivement vraie (1). Les raisonnements précédents n’ont fait qu'enchaîner des relations récurrentes : ils sont à leur tour formalisables dans la théorie. On peut écrire — si l’on représente la non contradiction de la théorie par

(x) © xD (0 0)

(il n’y a pas de démonstration pour 0:<0) — l’implication, formelle cette fois :

&@oxD(0Æ0)+(x)xxDp(Np) (6)

(x) On voit d’ailleurs que puisque pour tout x © 4 D p (Nh), l'implication (4) donne pour tout x Démonstrabil de 7 (Nx, Np) :

aucun exemple ne peut réfuter p (Np).

THÉORÈME DE GÔDEL 149

où l’on suppose tous les signes d’abréviation utilisés ici, qui représentent des notions de la syntaxe, remplacés par les signes de la théorie qui les traduisent. Mais alors le second membre devient en vertu de (3) la généralisation de 7 (Nx, Np) par rapport à la 1'e variable, c’est-à-dire par définition p(Np) : s’il y avait dans la théorie une démonstration formelle de sa non contradiction, l'implication (6) permettrait d’en tirer une démonstration de p(Np), ce qui est impossible.

Le raisonnement précédent s'applique non seulement au système des Principria, mais à tout système tel que :

1° la classe des axiomes et des règles soit définissable par récurrence (c’est-à-dire au moyen de relations récurrentes aussitôt que l’on remplace les signes par des nombres) ; 2° toute relation récurrente soit exprimable dans le système (à la façon du théorème I). Tel est le cas de tout formalisme, assez vaste pour contenir l’arithmétique et pourvu d’un nombre fini d’axiomes ou de schémas d’axiomes: en particulier des systèmes de ZERMELO-FRAENKEL et von NEUMANN pour la théorie des ensembles, du système von NEUMANN pour la mathématique classique. — GÔDEL introduit en outre la propriété d’e-non contradiction pour un système: impossibilité d’y démontrer à la foisune proposition à une variable (du type 2) pour chaque valeur (numérique) de cette variable, et la négation de la généralisation de cette proposition (1). Comme 7 (Nn, Np) (dont p(Np) est la généralisation) est démontrable pour toute valeur de x, la Nég p(Np) ne doit pas être démontrable si le système est «-non contradictoire : p(Np) est donc impossible à décider dans le système. Un système d’axiomes satisfaisant aux conditions x et 2 et w-non contradictoire est donc nécessairement

(1) Un système peut donc être non contradictoire et w-contradictoire : il suffit d'ajouter aux axiomes du système formel considéré Nég p (ND) ; le système est w-contradictoire et il est cependant impossible d’y démontrer p (Np) (il est donc non contradictoire).

J. CAVAILLÈS 10

150 THÉORÈME DE GÔDEL

non saturé ; on peut y prendre en particulier comme proposition impossible à décider, l’affirmation de sa non contradiction.

La raison de ce résultat doit être cherchée dans le fait «que la formation de types de plus en plus élevés se poursuit dans le transfini, tandis qu’il en existe au plus un infi- ‘nité dénombrable dans chaque système » (1). La définition d’un système ne peut, en effet, poser qu’une infinité dénombrable de signes (donc de types), et HILBERT a donné pour les fonctions l’exemple d’une construction récurrente transfinie de types (2?) : si haute que soit la borne supérieure (nombre ordinal de la classe IT), elle pourra toujours être dépassée. Mais c’est une possibilité intuitive : on ne voyait pas la conséquence pour la non saturation parce qu’on imaginait poser seulement ainsi un nouveau système. C’est la théorie des types qui masque sa propre insuffisance : dans une proposition les variables ont toujours un type déterminé, appartenant au système, une proposition portant sur tous les types (ou énonçant qu’une relation est vraie pour des variables de tous les types) — donc de type immédiatement supérieur à ceux-ci — fait partie de la syntaxe et non du système. D’une façon générale, le caractère w impossible à démontrer » n’est pas définissable (n'appartient pas à la syntaxe). Von NEUMANN le remplaçait par l’appréciation psychologique « il est très invraisemblable qu’on puisse jamais démontrer que... ». Il faut, pour sortir du vague, que l’on rencontre une proposition dont la démonstrabilité entraîne contradiction, c’est-à-dire qu’on formalise la syntaxe dans la langue : d’où le choix que fait GôDEL de la proposition p(Np) pour atteindre la non saturation ().

(1) GÔDEL, loc. cit., p. 191 n.

(2) V. supra, chap. III..

(3) C’est la seule pour laquelle la démonstration réussisse : sans formali-

sation de syntaxe dans le système, il n’y a pas de démonstration directe de non saturation.