« 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 typographie (20%) y'a probablement besoin de TeXifier tout ça |
m Bot : Remplacement de texte automatisé (-... +…); changement de type cosmétique |
||
Ligne 24 :
: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>
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) .
Ligne 80 :
:''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
Supposons que <code>a(r=)bxy</code> soit dans ''VAF<sub>0</sub>''.
Ligne 88 :
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
Im par Prod1 de w est donc inclus dans Im par Prod de w
Ligne 146 :
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,
(i) la formule qui traduit P(0, c1,
(ii) la formule qui traduit (pour tout x, si P(x, c1,
(iii) la formule qui traduit non P(c, c1,
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.
| |||