« 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é (-<sub>1</sub> +₁)
m (Bot : Remplacement de texte automatisé (-, *(…|\.\.\.) +…))
m (Bot : Remplacement de texte automatisé (-<sub>1</sub> +₁))
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 ''AF<sub>1</sub>AF₁'' ==
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle ''R<sub>1</sub>R₁'' de ''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 ''Finitaire 1''.
 
:''AF<sub>1</sub>AF₁'' (pour tout ''x'')(pour tout ''y'')(si ''x = y'' alors ''sx = sy'')
 
''AF<sub>1</sub>AF₁'' est représenté par :
 
:<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 ''AF<sub>1</sub>AF₁'' est dans ''VAF''. Montrons qu’il est dans ''VAF<sub>5</sub>''.
 
:''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 ''AF<sub>1</sub>AF₁'' est dans tt-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>'') <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>AF₁'' 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) .
 
:''AF<sub>1</sub>AF₁'' = <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 :
:Z’’’’ = <code>o</code>
 
Il reste à montrer que ''AF<sub>1</sub>AF₁'' n’est pas dans tt-F-Prod(''FAF<sub>4</sub>'').
 
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 ''AF<sub>1</sub>AF₁'' ≠ assz’z’’’.
 
On peut prouver facilement si z ≠ rx alors ''AF<sub>1</sub>AF₁'' ≠ assz’z’’’, il reste à montrer que ''AF<sub>1</sub>AF₁'' ≠ ass(rx)z’’’.
 
Supposons ''AF<sub>1</sub>AF₁'' = ass(rx)z’’’ (''hyp'').
 
Alors
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 ''VAF<sub>1</sub>VAF₁''.
 
La définition de ''VAF<sub>1</sub>VAF₁'' conduit à vouloir montrer que ou <code>a(r=)bxy</code> n’est pas dans ''VAF<sub>0</sub>'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans ''VAF<sub>0</sub>'', pour tous x et y dans N.
 
:''VAF<sub>0</sub>'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
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 ''AF<sub>1</sub>AF₁'' dans ''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 ''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 ''Finitaire 1''.
 
== La vérité de AF14 ==
143 371

modifications