ANALYSE CLASSIQUE III

l'artifice russellien du terme « celui qui »1 % (x), mais le nouvel axiome est une simple conséquence des axiomes obtenus à partir des schémas (2) et (3), ses « formules. d'unité » (1).

L'analyse classique étudie les procédés de définitions progressives d'individus — ou de catégories de variables — à partir d’une seule espèce d'individus de type x, les nombres entiers. On prend pour cela deux signes fondamentaux, o et s, caractérisés par trois axiomes : les deux axiomes de PEANO et l’axiome d’induction complète (6) :

— Sj —10 (4) sj = sk > ÿ = À (5) Ds CESR Tes () (6)

(7 et À sont des individus de type 1, £& la variable correspondante (2?) — seule catégorie de variables dans ce type —, x une variable propositionnelle de type 2). Tous les individus de type 1 sont obtenus par itération du signe s devant o, $ë exprime donc qu’il faut itérer une fois de plus s devant l’individu substitué à &.— Dans les types supérieurs on introduit une espèce particulière de variables — et d'individus correspondants — les fonctions mathématiques, qui résultent d’une dissociation des prédicats où intervient l’indi-

(x) La définition générale du terme « celui qui » s'effectue au moyen de déux propositions :

Z A(x) et II [A(x) À A(y) > x = y]

57 ZX, y

On en tire A(wA(x)). Dans le cas particulier d’une définition d’individu par les schémas (2) et (3), À (xn) est représenté par IL [## (#n—1) ss JA Dre BERNAYS a montré (HILBERT-BERNAYS (I), Pp. 433-457) qu'il était toujours possible d'éliminer le terme & d’une démonstration : son introduction ne représente pas d'extension véritable du formalisme. (2) est dite la variable portante de l'induction dans la formule x, (£) qui peut comporter dans son argument d’autres variables.