« 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é (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire)
Sharayanan (discussion | contributions)
m typographie (20%) y'a probablement besoin de TeXifier tout ça
Ligne 1 :
La théorie Finitaire1''Finitaire 1'' permet de formaliser la preuve naturelle de la cohérence de l’arithmétique formelle ''AF''.
Il faut montrer que l’ensemble des axiomes de ''AF'' est inclus dans l’ensemble ''VAF'' des vérités du modèle VAF0''VAF<sub>0</sub>''. Tous ces ensembles sont constructibles dans Finitaire1''Finitaire 1''.
 
== 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.
 
Les 13 axiomes de ''AF'' qui traduisent les 13 règles de production de VAF0''VAF<sub>0</sub>'' sont évidemment vrais de VAF0''VAF<sub>0</sub>''. 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.
 
== La vérité de AF1''AF<sub>1</sub>'' ==
AF1 (pour tout x)(pour tout y)(si x=y alors sx=sy)
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle R1''R<sub>1</sub>'' de VAF0''VAF<sub>0</sub>'' 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''Finitaire 1''.
 
AF1:''AF<sub>1</sub>'' (pour tout ''x'')(pour tout ''y'')(si ''x = y'' alors ''sx = sy'')
AF1 est représenté par
 
AF1''AF<sub>1</sub>'' est représenté par :
a(rttx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)
 
:<code>a(rttx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
Il faut prouver que AF1 est dans VAF. Montrons qu’il est dans VAF5.
 
Il faut prouver que AF1''AF<sub>1</sub>'' est dans ''VAF''. Montrons qu’il est dans VAF5''VAF<sub>5</sub>''.
VAF5 =def Union(non-V-Prod(AAF4, VAF4, FAF4), et-V-Prod(AAF4, VAF4, FAF4), ou-V-Prod(AAF4, VAF4, FAF4), ex-V-Prod(AAF4, VAF4, FAF4), tt-V-Prod(AAF4, VAF4, FAF4) )
 
:''VAF<sub>5</sub>'' <math>\overset{\overset{def}{=}}{\,}</math> Union(non-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), et-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ou-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ex-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') )
Montrons que AF1 est dans tt-V-Prod(AAF4, VAF4, FAF4)
 
Montrons que ''AF<sub>1</sub>'' est dans tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'')
tt-V-Prod(AAF4, VAF4, FAF4) =def Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans AAF4 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(FAF4)
 
:tt-FV-Prod(FAF4''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 FAF4''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>'')
 
Montrons:tt-F-Prod(''FAF<sub>4</sub>'') d’abord que AF1 est=<math>\overset{\overset{def}{=}}{\,}</math> dans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans AAF4''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) .
 
tt-V-Prod(AAF4,Montrons VAF4,d’abord FAF4)que ''AF<sub>1</sub>'' est =defdans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans AAF4''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(FAF4).
AF1 = ass(rx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)
 
:''AF<sub>1</sub>'' = <code>ass(rx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
Il suffit de choisir
 
Il suffit de choisir :
Z’ = rx
 
:Z’ = <code>rx </code>
Z’’ = asss(rttx)a(rnon)a(ret)b(a(r=)bosss(rx))a(rnon)a(r=)b(a(rs)oa(rs)sss(rx)
 
Z’’’:Z’’ = <code>asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sssbosss(rx))a(rnon)a(r=)b(a(rs)(rx))aoa(rs)sss(rx)</code>
 
AF1:Z’’’ = ass(rx)<code>asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
Z’’’’ = o
 
:Z’’’’ = <code>o</code>
Il reste à montrer que AF1 n’est pas dans tt-F-Prod(FAF4).
 
Il reste à montrer que AF1''AF<sub>1</sub>'' n’est pas dans tt-F-Prod(FAF4''FAF<sub>4</sub>'').
Prouvons (i)
 
Prouvons (''i'') :
(i) Pour tout z’, z’’, z’’’, z’’’’,
 
:(''i'') Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans FAF4''FAF<sub>4</sub>'', z’’’ est dans ''PAF'', z’’’’ est dans ''N'' et Cz’’Cz’’’’Cz’z’’’ est dans Sub, alors ''AF<sub>1</sub>'' ≠ assz’z’’’.
 
On peut prouver facilement si z ≠ rx alors AF1''AF<sub>1</sub>'' ≠ assz’z’’’, il reste à montrer que AF1''AF<sub>1</sub>'' ≠ ass(rx)z’’’.
Alors AF1 ≠ assz’z’’’
 
Supposons AF1''AF<sub>1</sub>'' = ass(rx)z’’’ (''hyp'').
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
 
:z’’’ = <code>asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
 
:z’’= <code>asss(rttx)a(rnon)a(ret)b(a(r=)bz’’’sss(rx))a(rnon)a(r=)b(a(rs)z’’’a(rs)sss(rx)</code>
 
On veut déduire une contradiction à partir de ''hyp''. Il suffit de prouver que z’ n’est pas dans FAF4''FAF<sub>4</sub>''.
 
FAF4:''FAF<sub>4</sub>'' =def Union(non-F-Prod(AAF3''AAF<sub>3</sub>'', VAF3''VAF<sub>3</sub>'', FAF3''FAF<sub>3</sub>''), et-F-Prod(AAF3''AAF<sub>3</sub>'', VAF3''VAF<sub>3</sub>'', FAF3''FAF<sub>3</sub>''), ou-F-Prod(AAF3''AAF<sub>3</sub>'', VAF3''VAF<sub>3</sub>'', FAF3''FAF<sub>3</sub>''), ex-F-Prod(AAF3''AAF<sub>3</sub>'', VAF3''VAF<sub>3</sub>'', FAF3''FAF<sub>3</sub>''), tt-F-Prod(FAF3''FAF<sub>3</sub>'')
 
Montrons que z’ n’est pas dans tt-F-Prod(FAF3''FAF<sub>3</sub>'').
 
Le même raisonnement que ci-dessus peut être répété et on est conduit à vouloir prouver que :
 
si:Si x et y sont dans ''N'' alors <code>a(rnon)a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans FAF3''FAF<sub>3</sub>''.
 
FAF3:''FAF<sub>3</sub>'' =def Union(non-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>''), et-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>''), ou-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>''), ex-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>''), tt-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>'')
 
:non-F-Prod(AAF2''AAF<sub>2</sub>'', VAF2''VAF<sub>2</sub>'', FAF2''FAF<sub>2</sub>'') =def Ensemble-image par non-P-Prod de VAF2''VAF<sub>2</sub>''
 
:non-P-Prod =def Fonction a(rnon)X
 
On veut alors montrer que <code>a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans VAF2''VAF<sub>2</sub>''.
 
La définition de VAF2''VAF<sub>2</sub>'' conduit à vouloir montrer que <code>a(r=)bxy</code> et <code>a(rnon)a(r=)b(a(rs)x)a(rs)y</code> ne sont pas tous les deux dans VAF1''VAF<sub>1</sub>''.
 
La définition de VAF1''VAF<sub>1</sub>'' conduit à vouloir montrer que ou <code>a(r=)bxy</code> n’est pas dans VAF0''VAF<sub>0</sub>'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans VAF0''VAF<sub>0</sub>'', pour tous x et y dans N.
 
VAF0:''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 VAF0''VAF<sub>0</sub>''.
 
Il y a un w tel que <code>a(r=)bxy</code> est dans w et w est dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo
 
Im par Prod de w est aussi dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo
Ligne 95 ⟶ 92 :
Im par Prod1 de w est donc inclus dans Im par Prod de w
 
:Prod1 =def Fonction Extension de (Il existe un Z’ tel que Z’ Dans X Et CZ’Z Dans Inst-R1)
 
:Inst-R1 =def Ensemble-image par Rep-R1 de Produit cartésien de Tconst et Tconst
 
:Rep-R1 =def Fonction C(a(r=)bXX’)(a(r=)b(a(rs)X)a(rs)X’)
 
<code>C(a(r=)bxy)a(r=)b(a(rs)x)a(rs)y</code> est dans Inst-R1 puisque x et y sont dans N et que N est inclus dans Tconst.
 
On en conclut que <code>a(r=)b(a(rs)x)a(rs)y</code> est dans Im par Prod1 de w et donc dans VAF0''VAF<sub>0</sub>''.
 
Cela termine cette preuve de la vérité de AF1''AF<sub>1</sub>'' dans VAF0''VAF<sub>0</sub>''. 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''Finitaire 1'' 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''Finitaire 1''.
 
== La vérité de AF14 ==