LA FONCTION #€ II

29 lorsqu'un prédicat n’est vrai que d’un individu, elle désigne celui-ci ; elle évite donc l’artifice du terme russellien «celui qui » et permet de transformer immédiatement toutes les définitions d'individus en définitions explicites; — 30 elle détermine le choix d’un individu particulier lorsque le prédicat convient à une collectivité. — C’est donc un moyen universel de passage entre propositions à variables et propositions individualisées ; le passage a même lieu cette fois dans les 2 sens, sans que, du reste, la définition du couple variable-individu soit lésée : ce n’est que pour l'individu xx 1 À (x) qu'il y a réversibilité de substitution avec la variable. On voit le gain de puissance : les procédés applicables seulement aux individus pouvant être maintenant

On vérifie sans peine que les relations entre Im et X, le schéma (1) sont satisfaits.

Pour le schéma (2 bis) — que nous considérerons au lieu de (2) puisqu'il sert seul dans le développement donné par HILBERT, mais la démonstration serait identique, sinon d’écriture plus compliquée — il suffit de substituer dans (8) au signe Y l'expression :

AE (Eux) = A] On à :

IT [fn (Enr) = À] > IT Lez, (II [En (Ën—x) ONU

x Sn—1 Égr

où 7n représente une piace vide pour un individu, fonction de type #). Si l’on remplace dans le terme de gauche 7, par «, on a:

Il DE A] + I Less (ICE (En—1) —= À ]) = A]

(2 Enr n—1

Le premier terme est une identité facile à démontrer dans le formalisme ; le terme de droite est donc également une identité ; elle s'écrit, d’après la définition du signe E :

2 I [En (Enr) = À] (2 Ent

(cf. von NEUMANN (II), p. 43).

Enfin l’axiome d’induction complète (6) s'écrit maintenant :

LA AE) = 57 AG). (6) bis