« 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é (-, *(…|\.\.\.) +…) |
m Bot : Remplacement de texte automatisé (-<sub>1</sub> +₁) |
||
Ligne 7 :
Les 13 axiomes de ''AF'' qui traduisent les 13 règles de production de ''VAF<sub>0</sub>'' sont évidemment vrais de ''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 ''
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle ''
:''
''
:<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 ''
:''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 ''
: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>'')
Ligne 26 :
: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 ''
:''
Il suffit de choisir :
Ligne 40 :
:Z’’’’ = <code>o</code>
Il reste à montrer que ''
Prouvons (''i'') :
:(''i'') Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans ''FAF<sub>4</sub>'', z’’’ est dans ''PAF'', z’’’’ est dans ''N'' et Cz’’Cz’’’’Cz’z’’’ est dans Sub, alors ''
On peut prouver facilement si z ≠ rx alors ''
Supposons ''
Alors
Ligne 74 :
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 ''VAF<sub>2</sub>''.
La définition de ''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 ''
La définition de ''
:''VAF<sub>0</sub>'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
Ligne 102 :
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 ''VAF<sub>0</sub>''.
Cela termine cette preuve de la vérité de ''
== La vérité de AF14 ==
| |||