« 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é (-... +…); changement de type cosmétique
m (typographie (20%) y'a probablement besoin de TeXifier tout ça)
m (Bot : Remplacement de texte automatisé (-... +…); changement de type cosmétique)
:tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') <math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans ''PAF'' Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) Moins tt-F-Prod(''FAF<sub>4</sub>'')
 
:tt-F-Prod(''FAF<sub>4</sub>'') =<math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''FAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub)
 
Montrons d’abord que ''AF<sub>1</sub>'' est dans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans ''PAF'' Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) .
:''VAF<sub>0</sub>'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
:Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union ... Prod13(X) ))
 
Supposons que <code>a(r=)bxy</code> soit dans ''VAF<sub>0</sub>''.
Im par Prod de w est aussi dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo
 
Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union ... Prod13(X) ))
 
Im par Prod1 de w est donc inclus dans Im par Prod de w
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, ...., 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
 
(iii) la formule qui traduit non P(c, 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