DÉFINITION DE TYPES

utilisés universellement, même s’il n’y a pas de moyens de définition univoque (rôle du choix) (1).

Le resserrement corrélatif du formalisme est obtenu d’abord par la définition expresse des types employés ; pour chaque catégorie de variables on a un moyen récurrent d’engendrer les définitions. Ainsi pour les variables-fonctions dont la valeur est du type des nombres entiers, si Pr (£,) caractérise le type », le type n + 1 sera défini par

Das (En) LU (D (Es) + Pi (Ente (E))]

(æ, caractérisant la variable numérique). On voit alors que

(1) Dans (IX) (p. 176) HILBERT fait déjà allusion à cet axiome « transfini » qui lui permet de dominer de façon finie le formalisme de la théorie des nombres. Il l’énonce explicitement pour la 1re fois en 1923 (HILBERT (X), p. 183) : au lieu de la fonction exA{(x) apparaît la fonction +:A(x), appelée familièrement l’Ayistide : elle désigne l'individu duquel, avant tout autre individu, serait vrai le prédicat À (s’il convenait à un individu). L’axiome (8) a donc la forme (nous laissons de côté l'indice du type) :

A(txA(x)) > U(x) (8) bis

« si (x) signifie être corruptible, alors t:N(x) désignerait un certain homme d’une telle inébranlable intégrité que si on pouvait prouver sa corruptibilité, tous les hommes seraient alors corruptibles » (Z. c., p.183): :

» X(x) ne A(tz — A(x) )

Dès le mémoire Sur l’Infini (1925) l'application du formalisme à la théorie des ensembles amène HILBERT à faire coïncider cet axiome avec l’axiome de choix ; rx%{x) devra alors être remplacé par ex{x) : élément distingué de la classe des individus possédant le prédicat A. Le véritable axiome de choix de la théorie des ensembles n’est d’ailleurs pas atteint pour cela : il faut que l’élément distingué soit coordonné de façon biunivoque à sa classe. On doit donc ajouter l’axiome :

N LUxn) D B(rn)] + Lex, Avr) = ex, B(an)] (8) ter

ñn

axiome foyt de choix (HiLBErT (XIII), p. 319).