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

Contenu supprimé Contenu ajouté
m Bot : Remplacement de texte automatisé (-oe +œ)
m Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire)
Ligne 151 :
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