‹ Recherches sur la théorie de la démonstrationChapitre 67 sur 101 · Nous voyons donc que la Théorie 3 peut être fondée · texte numérisé non relu

Nous voyons donc que la Théorie 3 peut être fondée

car

sur les axiomes suivants:

et les axiomes déduits de:

Do:(x).Dx-)Dx +1: ). dy (1)

en remplaçant ® x par des fonctions propositionnelles quelconques.

Ce sont à peu près les axiomes de Peano pour l’Arithmétique.

Remarquons que nous aurions pu fonder la Théorie 1 sur les axiomes déduits des 5 premiers (de 1.2) par substitution, et sur la règle:

Si E PO ef si -.(x).Px DDxt1, on déduit: - dy les démonstrations restaient les mêmes, mais nous n’aurions pas mis en évidence ce fait remarquable que, dans la Théorie 3, (et, on le voit aisément, la Théorie 1), ,l’axiome d’induction totale”, est une conséquence d’un certain nombre de ses cas particuliers.

84. Neumann, dans le mémoire cité plus haut ($ 5), a démontré que, quand on avait démontré la non-contradiction des cinq premiers des axiomes ci-dessus, on en déduisait immédiatement la non-contradiction de ceux déduits de la proposition (1). La méthode employée est, au fond, la suivante:

Dans une démonstration déterminée, on n’emploie jamais la proposition (1) que pour un nombre fini de fonctions ® x, soient D; x, D,,...®,x. On constate immédiatement que le produit logique des propositions (y):.D,0:(x).®;x )®D;,x+1: )%dy satisfait aux conditions du Théorème du Ch. 3, 3.31 vu que:

me 0) ed: 00,0

DO (x) Dem re T2) D y. n".D0:

CCR KO PE ED AU ES D (Ces propositions sont des identités aisées à démontrer).

8.5. Pour aboutir à une théorie équivalente à l’arithmétique classique, il faudrait encore introduire les définitions par récurrence. Pour le faire, nous nous permettrons d’adjoindre un certain nombre de fois à la théorie des fonctions descriptives nouvelles à un ou plusieurs arguments, avec, à chaque fois, des axiomes de forme suivante: Soit Axy:y:...y, la fonction descriptive introduite; supposons que dans la théorie à laquelle on ajoute AxY1ÿ5...y, On ait:

ra) x = = 0 xp y, (12) (zx = Vrzyr. y, avec des fonctions propositionnelles déterminées d et \'; on ajoute alors les axiomes:

H.D[AOpipoe ns Yuyae..y,l NT ee M SN À

Page 1