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

Aller à la navigation Aller à la recherche
m
Bot : Remplacement de texte automatisé (-, *(…|\.\.\.) +…)
m (Bot : Remplacement de texte automatisé (-... +…); changement de type cosmétique)
m (Bot : Remplacement de texte automatisé (-, *(…|\.\.\.) +…))
AxIC= Ensemble-somme de Image par IC-Prod de PAF
 
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, …c1…., cn de N,
(i) la formule qui traduit P(0, c1, …c1…., cn) , c’est-à-dire la substitution de 0 à l’une des variables x de P et de c1, …c1…., cn aux autres variables, est un élément de VAF.
 
(ii) la formule qui traduit (pour tout x, si P(x, c1, …c1…., cn) alors P(sx, c1, …c1…., cn) ) est dans VAF
 
(iii) la formule qui traduit non P(c, c1, …c1…., cn) est dans VAF
 
La preuve de cette contradiction est rendu aisée par le fait que VAF est clos par l’opération de conséquence logique, autrement dit, si une formule est la conséquence logique de formules qui sont dans VAF alors elle est aussi dans VAF.
143 371

modifications

Menu de navigation