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

Contenu supprimé Contenu ajouté
imported>Tavernierbot
m Bot: Retouches cosmétiques
Ligne 3 :
Il faut montrer que l’ensemble des axiomes de AF est inclus dans l’ensemble VAF des vérités du modèle VAF0. Tous ces ensembles sont constructibles dans Finitaire1.
 
== Pourquoi prouver des évidences ? ==
Les 13 axiomes de AF qui traduisent les 13 règles de production de VAF0 sont évidemment vrais de VAF0. Les moyens de preuve de Finitaire 1 sont suffisants pour établir cette évidence. Quand on écrit une telle preuve formelle, on ne cherche qu’en apparence à prouver l’évidence. Mais ce qu’on fait en vérité c’est éprouver l’efficacité de la formalisation. Si les règles permettent de prouver des évidences, c’est un bon signe. Si elles ne le pouvaient pas, elles seraient très insuffisantes. En prouvant formellement des évidences on cherche à prouver la qualité de la formalisation mais pas les évidences que l’on prouve cependant.
 
== La vérité de AF1 ==
La preuve suivante de la vérité de l’axiome AF1 qui traduit la règle R1 de VAF0 a une valeur générale. N’importe quel axiome qui traduit une règle de production d’un modèle est vrai pour ce modèle, et la preuve de ceci peut être formalisée dans Finitaire1.
 
Ligne 51 :
On peut prouver facilement si z ≠ rx alors AF1 ≠ assz’z’’’, il reste à montrer que AF1 ≠ ass(rx)z’’’.
 
Supposons AF1 = ass(rx)z’’’ (hyp).
 
Alors
Ligne 75 :
non-P-Prod =def Fonction a(rnon)X
 
On veut alors montrer que a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y n’est pas dans VAF2.
 
La définition de VAF2 conduit à vouloir montrer que a(r=)bxy et a(rnon)a(r=)b(a(rs)x)a(rs)y ne sont pas tous les deux dans VAF1.
 
La définition de VAF1 conduit à vouloir montrer que ou a(r=)bxy n’est pas dans VAF0 ou a(r=)b(a(rs)x)a(rs)y est dans VAF0, pour tous x et y dans N.
 
VAF0 =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 a(r=)bxy soit dans VAF0.
Ligne 91 :
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
Ligne 107 :
Cela termine cette preuve de la vérité de AF1 dans VAF0. Toutes les étapes n’ont pas toujours été explicitées mais il s’agit à chaque fois de la même technique, expliciter les définitions des ensembles étudiés et déduire avec la logique du premier ordre et les axiomes de Finitaire1 les énoncés que l’on veut prouver. Toutes les étapes de ces preuves, longues à écrire mais rapides à trouver, sont également triviales. Elles consistent essentiellement à vérifier qu’on n’a pas oublié de mentionner toutes les règles évidentes dans les axiomes de Finitaire1.
 
== La vérité de AF14 ==
Il reste à prouver que les représentants de AF14, AF15 et des axiomes d’induction complète sont dans VAF.
 
Ligne 144 :
Comme a(r=)bxy n’est pas dans Absurd1, x = y. Comme a(r<)bxx est dans Absurd2, a(r<)bxy n’est pas dans VAF0. Cela termine cette preuve abrégée de la vérité de AF14. La vérité de AF15 peut être prouvée par un raisonnement semblable.
 
== La vérité des axiomes d’induction complète ==
Soit AxIC l’ensemble des (représentants des) axiomes d’induction complète.
 
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