« Fondements des mathématiques/Preuve formelle de la cohérence de l'arithmétique formelle » : différence entre les versions

m
Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire)
m (Bot : Remplacement de texte automatisé (-oe +œ))
m (Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire))
Si P est dans PAF, IC-Prod(P) est l’ensemble fini des axiomes d’induction complète qu’il définit. Ic-Prod(P) contient autant d’éléments que le prédicat P a de variables libres. La construction de AxIC est laborieuse mais elle ne pose pas de difficultés de principes parce qu’il s’agit d’une question décidable. Une démarche semblable aux preuves de vérités des autres axiomes conduit alors à vouloir prouver que les trois hypothèses suivantes sont mutuellement contradictoires pour un élément P de PAF, et n+1 éléments c, c1, ...., cn de N,
(i) la formule qui traduit P(0, c1, ...., cn) , c’est -à -dire la substitution de 0 à l’une des variables x de P et de c1, ...., cn aux autres variables, est un élément de VAF.
 
(ii) la formule qui traduit (pour tout x, si P(x, c1, ...., cn) alors P(sx, c1, ...., cn) ) est dans VAF
143 371

modifications