II M ER RE A

Xp, dn

Si au.contraire elle est démontrable pour certaines individualisations seulement des mêmes variables on écrit (?) :

— Il M (Tee)

XnVn ou par abréviation (#] :

DNS LA QE 2h \

Les propositions sont dites quantifiées par Î ou par à, et les variables correspondantes (ici x,, y,) liées par Il ou S : il n'y a plus pour ces variables possibilité de substitution d'individus. Un quantificateur peut figurer à l’intérieur

(1) Le cas peut se présenter s’il n’y a qu’un nombre fini d'individus substituables à la variable.

(2) Les majuscules gothiques A, B représentent des propositions complexes ayant pour éléments des prédicats de type # + 1 (les variables sont de type »).

(3) Ce qui ne pourrait être exprimé sans quantificateur.

(4) Le symbole E n’est pas comme Il un nouveau signe, mais abréviation pour 1 II =.

d’une proposition complexe (par application de la règle de substitution) : il a pour éendue — fixée par des parenthèses — la proposition élémentaire ou complexe dont il lie une ou plusieurs variables. L'introduction formelle des quantificateurs s'effectue au moyen d’une règle et d’un axiome :

a) règle de généralisation : on a le droit de quantifier par Il toute proposition à variables valable, I liant toutes ou certaines seulement des variables de la proposition. L’étendue de I peut être d’ailleurs arbitrairement augmentée ou diminuée (lorsque par exemple la proposition quantifiée figure dans une proposition complexe) sous la double réserve : 1° que les variables liées par Il, ou d’autres variables représentées par le même symbole, n'apparaissent pas dans les propositions partielles admises ou exclues par ces extensions ou ces diminutions ; 2° que le quantificateur ne soit pas amené à enjamber des négations lorsque la proposition complète est mise sous forme normale conjonctive ou disjonctive. Autrement dit, que ces variations ne changent rien aux opérations de démonstration de la proposition-(1) ; on peut écrire indifféremment :

I [A(x) VB] ou NHYX(x)vB

La justification intuitive de la règle est immédiate : si une proposition à variables est démontrable il résulte de la règle de substitution que toutes ses individualisations sont démontrables, donc aussi la proposition quantifiée qui résume leur ensemble.

(1) Cette règle, incorporée à la règle de généralisation, remplace ce qu’on distingue habituellement sous le nom de règle de passage: passage des signes v et À dans l’étendue de II (Cf. en particulier HERBRAND (II), p. 32). GÔDEL introduit un axiome spécial :

D(A(x) VB) > DA(x)vB LA

(GôneL (1), p. 350) qui nous semble superflu. L'énoncé de la règle du texte montre assez qu'il s’agit d’un seul acte de l'esprit opérant sur le formalisme.

b) Axiome du calcul des prédirats :

(x) IL x (tu, Vns Znscee) > À (Ans Vns Aie) | Xp Yn I] garantit le passage, dans une démonstration, de propositions individualisées à propositions quantifiées : si on substitue les individus 2,, 7, à ‘x,, y, dans (1) on voit que la substitution ne peut s'effectuer qu’à droite. On obtient, en contraposant :

— U (1, 1u Zn.) + — Il AL V2 Xn Ÿn

ou en remplaçant At) Par (0

NEA PER 0) Re DE: (LS 200) XnŸn

Si les individus ?,, 3, permettent de démontrer le re" membre de l'implication il en résulte donc une démonstration pour la quantification par > de la proposition. Il n’y a pas ici de justification intuitive mais plutôt définition du quantificateur, ou — si l’on donne à celui-ci son sens intuitif — du rapport variable individu : la substituabilité non réciproque se transforme en relation de représentation : la variable n’est plus, d’après la formule (1), que le représentant de la collectivité des individus qui lui sont substituables.

Pas plus pour le calcul des prédicats que pour le calcul des propositions une démonstration de non contradiction des règles et des axiomes n’a de sens : on a vu que pour le calcul des propositions tel qu’ii s’introduit naturellement il n’y a pas d’axiome, mais des règles découlant immédiatement de la notion de non contradiction. Pour le calcul des prédicats la règle est une convention d'écriture et l’axiome est unique. Grâce à la règle on unifie le formalisme en remplaçant partout où cela est commode propositions à variables par propositions quantifiées : l’axiome achève l’unification avec par