XI X

i étant un individu quelconque. 20 La règle de généralisation la conserve : étant donné l'identité de traitement entre variables générales non dominées et variables libres, la chose est immédiate lorsqu'il y a généralisation dans une proposition ne comportant pas de x. Dans le cas contraire suivant l'étendue plus ou moins grande choisie pour le nouveau I, la variable qu'il lie se trouvera ou non subordonnée

THÉORÈME D’HERBRAND 137

à des variables restreintes. Il n’est pas évident que le traitement donne alors le même résultat. Tout revient à prouver que si:

> LxN D

@ et 8 comportant un nombre quelconque d’autres variables), soumis au traitement procure une identité du calcul des propositions, il en est de même pour :

et réciproquement. Sous la première forme les variables générales figurant dans 8 sont remplacées par des fonctions d'indices f(u, v,...t),.… o(w, v, .… t) indépendantes de x ; sous la deuxième forme, x apparaît dans leur argument.

a) Si la deuxième forme de la proposition donne une identité, la proposition individualisée est vraie quelles que soient les valeurs logiques attribuées aux prédicats où figurent les individus donnés par f(u, v, ..….{, x)... + (w, v,t x), donc elle le reste si on donne la même valeur logique aux prédicats lorsque f, .… + ne diffèrent dans leur argument que par l'individu substitué à x ; on retrouve alors la disjonction correspondant à la première forme de la proposition initiale : elle est donc aussi une identité.

b) Si la deuxième forme, à l’étape #, ne donne pas une identité : il y a un système de valeurs logiques rendant fausse la réduite correspondante. On peut prendre pour la réduite de la 1re forme à la n°” étape les mêmes individus (elle en comportait moins puisque certaines de ses fonctions d'indices ont une variable de moins dans leur argument) : si la nouvelle réduite n’est pas une identité, la première non plus en vertu de :

An VNABNVN..NAi, > AuVARVN.V AY NN

Tout revient donc à comparer dans les réduites deux propositions partielles :

138 THÉORÈME D'HERBRAND

(1) At V Ato V ... V Ain V Bt 1re forme (2) Aù V Bi V Ai V Bi V...V Aix V Bix 22 forme

Le système de valeurs logiques donnant à la réduite totale sous la deuxième forme la valeur Faux peut donner à (2) : soit la valeur Vrai, alors c’est : ou un des 47, qui a cette valeur logique (:) et on fait

Fm, .5,) = fi. 8, ) ou un des Bi;, soit Br; et on fait :

fs 8) = 1 (ed + tt):

soit la valeur Faux on fait

Ge di) = HG, ed à) (puisque tous les By, sont faux).

L'utilisation des autres règles (substitution, séparation) conserve évidemment la propriété : règles du calcul des propositions, leur application aux réduites ne peut changer la valeur logique du résultat. Si on les applique aux propositions avant la réduction elles ne peuvent entraîner que des allongements de disjonction avec accroissement de l’argument de fonction d’indice. On se retrouve exactement dans la situation envisagée plus haut. En effet quelle que soit la valeur logique attribuée à la réduite plus longue il est toujours possible d’obtenir la même pour la réduite plus courte. L’allongement n’a d'efficacité que dans la mesure où, grâce aux fonctions d’indice, une variable restreinte et une variable générale se trouvent représentées dans le même prédicat (situé à deux places différentes) par le même individu : mais ceci n’est possible justement que dans les cas de subordination authentique, et non de subordination fictive comme celle qu’entraînent ces règles. — Tel est le sens véritable du traitement défini par HERBRAND : essayer grâce aux

(x) 7 représente un indice quelconque entre 1 et N.

THÉORÈME D'HERBRAND 139

fonctions d’indices toutes les identifications possibles entre variables restreintes et variables générales de façon à découvrir sous les changements de symbole que l'application des règles du calcul des prédicats a provoqués, le caractère identique de la proposition. Toute identité de la forme

EI Axy

devient en effet une identité

HXxYy

l’artifñice des fonctions d'indices n’a pour but que de la rétablir.

L'application aux problèmes de la non contradiction d’une théorie est immédiate : si la conjonction de ces axiomes peut être satisfaite par le processus précédent, la théorie n’est pas contradictoire. Pour les axiomes de la théorie des nombres : axiome de PEANO, tous les schémas (sans variable de type 2) de définition par récurrence, on voit que leur conjonction avec l’axiome du calcul des prédicats est satisfaisable. Les fonctions mathématiques sont — comme les fonctions d'indices — remplacées par un individu particulier pour chaque valeur particulière de leur argument. Si l’on considère sx comme une fonction, on voit que le processus de satisfaction ne laisse plus subsister que le prédicat — entre des individus dans l’énoncé des axiomes : les individus engendrés par s coïncident avec le système des entiers ; si l’on convient que z — 7 n’a la valeur Vrai que si z et 7 sont identiques, la conjonction des axiomes est satisfaite dans le champ et l’on retrouve l’arithmétique ordinaire ; en particulier la détermination des valeurs des fonctions mathématiques pour un argument donné s’effectue par les calculs ordinaires. Les axiomes d’une définition récurrente ne peuvent jamais introduire de contradiction puisqu'ils ne comportent chaque fois qu’une égalité entre deux fonctions dont

140 THÉORÈME D'HERBRAND

l’une (à gauche) est représentable par un individu arbitraire: il suffit de prendre le même que celui que fournit la fonction de droite déjà définie. Le processus de satisfaction coïncide donc exactement avec les démarches de l’arithmétique naïve.

Reste l’axiome d’induction complète. Mais il y figure une variable de type 2 et la satisfaction n’a été définie que pour des propositions avec variables (ou individus) de types x, et individus de type 2 : la fixation du cours de valeurs logiques d'un individu de type 2 pour toutes les individualisations possibles de ses variables de type 1 étant l'épreuve de la non contradiction de sa définition formelle. On conçoit l’extension du procédé au type supérieur : mais il faudrait pouvoir passer en revue tous les individus de type 2 substituables à la variable dans la théorie envisagée. Or, la situation n’est pas la même : dans le type 1 d’une part il n’y a pour une théorie donnée qu’un nombre fini de moyen d’engendrer des individus (signes présents dans les axiomes effectivement formulés) ; d'autre part, pour chaque individu, définition formelle et construction coïncident (l'individu n'est que 1 ou de forme s … sr). Au contraire un individu de type 2 est une expression formelle où figure la variable libre de type 1 : sielle est correcte comme structure (pourvue de sens), son énoncé même distingue l'individu (il est sa définition) mais ne le détermine pas ; il faut en outre, pour toute individualisation de sa variable, un moyen de décider sa vérité ou sà fausseté si c’est une proposition, de calculer sa valeur si c’est une fonction mathématique. Or, la satisfaction dans un champ suppose que, pour une individualisation des variables, 1l ne reste plus qu’un problème du calcul des propositions à résoudre (répartition des valeurs logiques entre les prédicats, ici de type 3) pour attribuer la valeur Vrai à la proposition examinée : à chaque type considéré elle exige donc que tous les problèmes des types précédents soient résolus dans le formalisme. Ainsi dans l’arithmétique

THÉORÈME D'HERBRAND I4I

définie plus haut — avec même un nombre fini de fonctions mathématiques — il faudrait, pour envisager la satisfaction de l’axiome d’induction complète, supposer décidées toutes les propositions où figurent ces fonctions (toute proposition complexe étant une architecture avec pour éléments des égalités entre deux fonctions ou entre une fonction et la variable, ou un individu, de type 1). Dès qu’intervient la multiplication il est donc impossible de satisfaire l’axiome.

La restriction est cependant moindre que dans le cas de la méthode des réduites. On peut admettre dans le formalisme autant de définitions récurrentes de fonctions qu’on voudra (sans variables de type 2) à condition de n’ajouter à ces axiomes que l’axiome d’induction complète élémentaire, ou l’axiome général où ne figure que l’addition. Dans le premier cas le prédicat æx est évidemment décidable pour toute individualisation de la variable puisqu'il ne comporte qu’une architecture avec les seules constantes À, V, — (sans quantificateur), à partir d'équations entre fonctions récurrentes déjà définies (ou entre de telles fonctions et la variable de type 1). Avec intervention des quantificateurs (2€ cas) on a vu qu’une décision est toujours possible. HER- BRAND démontre que ‘ans les deux cas l’axiome est une conséquence de définitions récurrentes de fonctions. Dans le premier cas il suffit d'introduire pour tout prédicat décidable æx la fonction u,x telle que si z est le plus petit individu pour lequel &x est faux on ait :

RAM OMDOU re Det ua te 1 POUR x 2 1.

C’est une fonction récurrente; les axiomes la définissant sont satisfaits quelle que soit la valeur logique attribuée à ®x à condition de remplacer partout æx par du,x : le champ de leur satisfaction se trouve ainsi caractérisé. Il est impossible d'y satisfaire la négation de l’axiome élémentaire d’induc-

tion :

142 THÉORÈME D’'HERBRAND

2 I [Do À (— x V Dsx) À — dy).

L' On voit en effet que, si on remplace x et y par uœx et uæy, quel que soit le choix de l’individu fixe 7 pour y, on se heurte à une impossibilité : sij <t1ona:

PO À (— PuyX V Puysx) À — Po

si j > 1, lorsque, dans la construction de la conjonction de satisfaction, on arrive à sx — 1, on a :

DO A (— Po V Pi) À — D?

En vertu du théorème d'HERBRAND, l'implication :

AIX [— Do V (Ex À — Psx) V Py] ,

(où X représente les axiomes définissant u&x) est donc une identité logique, l’axiome d’induction totale élémentaire est conséquence des définitions par récurrence (1). On a vu plus haut la méthode pour décider de toute proposition où

(1) On peut donner une démonstration formelle, Les axiomes définissant x s'énoncent (nous écrivons, pour alléger, u x au lieu de u@#) : MO \ [POA = PP SXAUX — 0] > p sx — 5% mn [PoA— PsrAurx = 0] > pusx = y UY = Sy > UKSyY = 5y À y — 0 On en tire sans peine :