I) ACKERMANN (I

(2) Von NEUMANN (II). Le procédé avait été déjà repris par J. Kônic à qui von NEUMANN en attribue la paternité : « La 1re idée de démontrer la non contradiction des mathématiques par une valuation vient de J. Kô- NIG (1)... La notion de valuation partielle repose sur des idées de HILBERT.» ‘Von NEUMANN (II), p. 22.

(3) Zbid., p. 22 n.

dant pour le domaine que formalisait Hit BERT en 1904 : il suffit de placer dans la 1re classe toutes les équations numériques intuitivement vraies (la décision est toujours possible, il suffit de compter) et leurs combinaisons (au moyen des constantes logiques) auxquelles le calcul des propositions donne la même valeur logique : la théorie des fonctions de vérité montre queles trois conditions sont satisfaites. C'est en référence avec cette valuation intuitive que l’on essaiera de définir les autres : on voit le progrès sur le mémoire de 1904 : son point d’aboutissement devient point de départ.

Von NEUMANN remplace l'impossible valuation générale par une valuation partielle : une règle qui, pour tout système fini d’axiomes, procure une répartition satisfaisant aux trois conditions. On voit que la 17e seule caractérise la valuation par rapport aux axiomes choisis. L’exigence suffit : si 0 < 0, où À À — À étaient démontrables dans la théorie totale ce ne pourrait être (comme dans toute démonstration) qu’au moyen d’un nombre fini d’axiomes et, par rapport à eux, la valuation serait impossible. La règle de valuation partielle ici est déterminée par un procédé de réduction partielle : pour tout système fini d’axiomes on a un moyen de coordonner à toute proposition une proposition numérique, sa réduite, la valuation intuitive de celle-ci entraîne la valuation partielle des propositions primitives. Von NEu- MANN ne mène à bien sa démonstration que pour un formalisme réduit au type 1 (avec la fonction < pour ce type, donc la possibilité de définir les individus de type 2). L'essentiel pour la valuation est la satisfaction de la condition 1°: pour les axiomes ordinaires de l’arithmétique (axiomes de PEANO) il n’y a pas de difficulté (au moins dans le type 1) (*). C'est

(1) L'axiome d’induction complète est restreint alors, à son usage élémentaire : impossibilité de coordonner à x:(£) dans (6) des propositions où interviennent des variables liées (il faudrait, pour cela, soit l’axiome de réductibilité, soit la fonction: e de type 2 3).

sur l’axiome schéma du calcul des prédicats — pris sous la forme (8) — que doit porter tout l'effort de la démonstration. En effet :

(ÿ) + À (e. À (x) (8) bis

représente une infinité d’axiomes qu’on obtient en remplaçant respectivement À et ; par des expressions de complication arbitraire (où interviennent déjà des €, avec aussi comme abréviation des IT et ? enchevêtrés les uns dans les autres autant qu’on voudra). La règle de réduction sera alors partielle : à tout système d’un nombre fini p d’actualisations du schéma, elle permet de coordonner p propositions numériques intuitivement vraies. On procède par induction. Il suffit de considérer l’édification progressive dans la théorie des formes À et 7 : elle se produit par insertion de formules déjà construites dans des matrices des relations de subordination établies entre les places vides par des quantificateurs II, X et par < disposés suivant un certain schéma ; pour un nombre fini de ces signes (c’est le cas dans un système fini d’axiomes), il n’y aura donc qu’un nombre fini de semblables schémas (toutes les combinaisons possibles de subordination et d’enjambement) : en insérant dans leurs places vides et pour 7 des formules déjà réduites on pourra choisir pour e,À (x) un nombre qui rende l’axiome numériquement vrai. On voit que le processus exige une double induction complète : il faudra, pour chaque matrice de examiner toutes les répartitions possibles de formules réduites entre ses places vides et, chaque fois, insérer à la place de la variable tous les 7 possibles déjà réduits. Comme les matrices À sont classées — et progressivement réduites — d’après le nombre de signes qui y interviennent, on voit que, d’une part, les ; substituables étant de classe forcément inférieure seront toujours préalablement réduits et que, d'autre part, les deux inductions sont chacune finie. On est donc sûr d'arriver au but. Le moment essentiel de la réduction con-

siste à donner son sens concret au schéma (8) brs : j toutes réductions effectuées, étant un nombre, on prendra s, égal au plus petit j pour lequel Y(;) soit intuitivement vrai (si Y (1) est faux pour toutes les substitutions, on pose &; — © avec la convention À( œ) intuitivement faux). C’est une suite de tâtonnements dont la considération de la structure des propositions garantit qu’elle trouve un terme. ACKERMANN avait essayé un procédé analogue pour le schéma général, mais, comme le montre von NEUMANN, ses raisonnements ne tenaient pascompte des complications produites par la présence de types multiples (à cause des variables Subordonnées). Les règles de substitution dans le cas de type supérieur, par exemple dans le cas d’une fonction f(x) où intervient la variable libre x ne permettent pas l’extension du procédé des tâtonnements successifs. Von NEUMANN espérait cependant y atteindre grâce à l’analogie de forme entre le schéma (8) bis et le schéma général (8). Ne s'agit-il pas, dans les deux cas, de trouver un exemple pour € ? Seulement, dans le 1er cas, on était certain d’y arriver, la construction progressive des individus À, de type 2, assurant chaque fois une borne supérieure au nombre d'individus de type 1 substituables ; dans le 2€, au contraire, il faudrait avoir recours à un artifice, l'apparition de variables de type 2 rendant impossible toute mise en ordre dans l’édification des individus de types plus élevés ; quant à une borne supérieure pour le nombre d’individus substituables, il n’en saurait être question : il y a déjà 2% individus de type 2. Le formalisme dont les démonstrations ACKERMANN et von NEUMANN établissent la non contradiction ne permet de reconstituer que la partie de l’analyse sans définitions non prédicatives, à peu près «ce qui correspond à la mathématique semi-intuitionniste des critiques de la théorie des ensembles... mathématique de WEyL dans le Continu » (1).

(1) Tbid., p. 46.

130 DÉSINTÉGRATION (HERBRAND)

Pour un formalisme sensiblement plus restreint, celui de la théorie des nombres avec, comme seule fonction, la fonction du suivant et des variables liées introduites par l’axiome logique ordinaire (sans «<), HERBRAND (1) et PRES- BURGER (2) ont donné une méthode qui prouve, non seulement, la non contradiction, mais aussi la saturation, et même permet de décider si une proposition est ou non démontrable. C’est encore une réduction mais portant, cette fois, directement sur toute proposition de la théorie (le détour de la valuation est inutile) : une proposition est constituée par la superposition d’un certain nombre de

quantificateurs II, ..., leur domaine étant des équations z y

de forme x = y +£ ({ étant un nombre; il n’y a jamais que 2 variables, puisque l'addition n’est pas introduite comme fonction), liées par les constantes logiques. On élimine progressivement les quantificateurs en partant de l’intérieur : comme toute proposition peut être mise sous une forme canonique où n'apparaissent que des signes > et V comme constante logique, la réduction reviendra à sañsfaire intuitivement les relations qu’ils expriment : sous le signe > situé le plus à l’intérieur, on remplace la variable qu’il lie par sa valeur calculée dans une des équations du domaine (que l’on supprime). En procédant ainsi de proche en proche, on arrive, avec l'élimination du dernier signe 5, à une disjonction d'équations numériques (si toutes les variables sont liées, ce qu'on peut toujours supposer d’après la règle de généralisation). L’arithmétique intuitive décide alors immédiatement de la vérité ou de la fausseté de la proposition. Des considérations simples de combinatoire montrent que le procédé de réduction est univoque, d’autre part l’adjonction de l’axiome

x —OUE X—=Y+I de

(1) HERBRAND (II), ch. IV.

(2) PRESBURGER (Ï).

DÉSINTÉGRATION (PRESBURGER) ep

(ayant pour conséquence l’axiome élémentaire d’induction complète) permet de démontrer que toute proposition est équivalente à sa réduite. La vérité intuitive de celle-ci entraîne la démonstrabilité de celle-là. La théorie est à la fois saturée et résoluble. PRESBURGER a étendu l'application de la méthode à une arithmétique un peu plus large, comprenant, cette fois, les axiomes définissant l’addition (1). Le formalisme est moins simple puisque dans les propositions élémentaires apparaissent des congruences numériques

a= b (mod. k).

( étant un nombre particulier). Le principe est le même : on élimine les variables liées en satisfaisant successivement aux équations.

Mais les relations générales où intervient un produit entre variables ne peuvent être représentées dans ce formalisme, il faut ajouter les axiomes définissant la multiplication : pour ce nouveau système la méthode est inutilisable. Suivant la remarque de BERNAYS (?), en effet, elle exige que l’on domine les relations formellement exprimées. Sila réduction livre un procédé de décision, c’est qu’elle exige effectivement la résolution de tous les problèmes : or, les problèmes insolubles commencent, en arithmétique, avec la multiplication comme fonction. La proposition (théorème de FER- MAT) :

Il MONA E0 > EE pre)

xy 2 (où k doit être un nombre, puisque l’exponentiation n'est pas ici une fonction) ne peut être réduite si R> 2. D'où les limites d'intérêt de la méthode : c’est bien, suivant le mot de BERNAYS, une désintégration, elle ne fait que détruire, de proche en proche, le processus de formalisation, en rétablissant les rapports intuitifs initiaux, le gain est nul.

(1) Cf. le résumé de sa méthode in HILBERT-BERNAYS (I), p. 359-368. (2)P1014-p2571

192 THÉORÈME DE LŒWENHEIM

De réflexions critiques sur un théorème de LŒWENHEIM, HERBRAND a tiré un procédé entièrement nouveau pour démontrer la non contradiction de formalismes bornés au type 1 (sans axiome :). Le théorème de LŒWENKHEIM (1) est énoncé dans le calcul relatif de SCHRÔDER, système seulement à demi formalisé. Le couple variable individu est défini par le rapport intuitif ensemble élément. Une proposition à variable est une proposition valable pour tout individu du domaine base ou champ (DENKBEREICH) ; les quantificateurs représentent les conjonctions ou les disjonctions de propositions individualisées étendues à la totalité du champ (la règle de généralisation et l’axiome (I) sont évidemment satisfaits) : la vérité d’une proposition dépend donc de celui-ci, qui sera défini si on connaît à la fois ses individus et les valeurs logiques attribuées à toutes les individualisations qu’il détermine des prédicats élémentaires. Reconnaître la validité de la proposition n’est plus ensuite qu’un problème de calcul des propositions. On voit que le nombre des individus dans le champ joue un rôle : la proposition (?) :

2(AxyAAY2NAzx) An 3 Axx