‹ Recherches sur la théorie de la démonstrationChapitre 42 sur 101 · Chapitre · texte numérisé non relu

Chapitre

nombre indéfini de types. Il faudra changer légèrement (et c’est la modification aux règles de raisonnements énoncées plus haut, qu’il faut effectuer pour toute théorie mathématique comportent des fonctions descriptives) l'énoncé de la deuxième règle de généralisation, qui devient le suivant:

Si P(f,x x» .., x.) est vrai, f étant une variable réelle une fonction descriptive dont les arguments sont des variables réelles ou une constante, alors (4 y) .Dyxixs...x, est vrai.

Par extension, nous disons encore qu’une proposition vraie dans la théorie considérée est une identité propositionnelle.

Cette extension de la théorie du Chapitre 2, est celle qui nous servira désormais; ce qu’elle contient d’essentiellement nouveau, ce n’est pas. l'introduction des types différents, mais bien celle des fonctions descriptives. Désormais les propositions éléments seront de forme Df,f,...f,, fi,f»,...,f, étant des individus, et non plus forcément des variables. Nous verrons d’ailleurs au dernier Chapitre que ,l’Entscheidungsproblem” dans cette nouvelle théorie, se ramène au même problème dans la théorie du Chapitre 2, ce qui fait que l’on peut, si l’on veut, éviter l'emploi des fonctions descriptives; mais elles nous seront nécessaires pour traduire en signes lesthéories mathématiques ordinaires.

1.41. Il est aisé de voir que, outre l’ancienne règle de substitution (Ch. 2, 5.1), nous en avons maintenant une autre:

On peut dans une identité propositionnelle, remplacer une fonction descriptive élémentaire par une fonction descriptive de même type et de mêmes arguments que la première.

Tous les autres résultats des 6 premiers paragraphes du Chapitre 2 subsistent; il faut, bien entendu, faire subir dans la deuxième méthode indiquée au paragraphe 6, la modification déjà indiquée à la deuxième règle de généralisation.

1.42. Quant à la théorie des champs, développée au paragraphe 8, elle s'applique presque sans changement dans ce nouveau cas. Il suffit de procéder comme suit:

1°. À chaque type, nous attachons un certain nombre de variables de ce type, que nous appellerons éléments du champ de ce type.

2% Nous faisons correspondre, comme nous voudrons, à chaque individu qui est une fonction descriptive élémentaire

Fa, &,,-.., a; ) dont les arguments sont des éléments des champs,

un élément du champ du même type que f.

— 59 — Chapitre 3. 1.42.

3°. Puis nous modifions ainsi la règle donnant la réduite de (4x).® x à partir de celle de ® x que nous nommerons # x: cette réduite sera: Pavpav...vpa, Si Œiy Are. A, SONt les éléments du champ du type de x.

4. Quand on a ainsi obtenu la réduite d’une proposition sans variables réelles, on utilise la correspondance décrite dans le 2°, pour, en remplaçant les f(as yes) Qi) par les éléments correspondants des champs, arriver à une proposition sans fonctions descriptives; c’est la proposition ainsi obtenue qui sera la réduite définitive.

Avec cette modification, tous les résultats de la théorie restent vrais (on en déduit en particulier la non-contradiction de la théorie considérée en 1.4).

Les critères de champ permettent évidemment de démontrer la non-contradiction de toutes les théories dont les axiomes sont vrais dans un champ fini (par exemple, la théorie des corps).

Page 1