II4 LA FONCTION

considérant d’abord que des formalismes partiels où l’on peut donner à l’axiome schéma (2) des substituts plus accessibles : resserrer le tissu du formalisme tout entier en le dotant à la fois de moyens plus puissants de démonstration et de règles plus précises (donc plus faciles à dominer par la pensée finie) pour l'introduction de nouveaux êtres.

L'augmentation de puissance est procurée par l'intervention de la fonction & : elle est définie, dans le cas d’une variable, par l’axiome schéma :

Y (14) gs bA (e, bi (x:)) (8)

(X est une proposition complexe quelconque, 7, la place pour un individu de type », x, une variable de type #). Il y a donc autant de fonctions < que de catégories de variables : le type et la catégorie de la valeur (1) de « (c’est-à-dire du couple :,, À (x,)) sont évidemment ceux de l'individu 7,. Le schéma (8) remplace à la fois les schémas (1) et (2) (ou (2) bis). Le rôle de la fonction e est, en effet, triple : x° elle établit la liaison entre variables et individus : les signes I et > peuvent disparaître (on les réintroduit cependant, pour la commodité, au moyen de définitions explicites (2)) ;

(1) ex, est une fonction d’argument Y(+:) dont la valeur peut être aussi. bien une variable propositionnelle qu’une fonction ou la variable numérique Pratiquement, seul le second cas intervient dans ie système de HILBERT. — Les règles de substitution doivent tenir compte du caractère fonctionnel des variables ou individus substitués : e;, (#7) est une fonction de type # donc, possède à son tour un argument de type n-1. Sur les erreurs commises à ce sujet, cf. von NEUMANN (Il), p. 41. — L'indice #1 dans e;,, indique qu’e lie seulement la variable #2 (si d’autres variables libres figurent dans A). Il peut y avoir plusieurs e superposés, v. plus bas.

(2) On écrit — toujours dans le cas d’une seule variable (les formules pour le cas général s’en déduisent aisément) —

n Aer) Z Ve, = U(xn) ) (0) E A(zn) À Ace, A(tn) ) (ro)

Xn