143 371
modifications
« Fondements des mathématiques/Preuve formelle de la cohérence de l'arithmétique formelle » : différence entre les versions
Fondements des mathématiques/Preuve formelle de la cohérence de l'arithmétique formelle (modifier)
Version du 5 février 2012 à 20:35
, il y a 10 ansRobot : Remplacement de texte automatisé (-\b([Qq])ue ([AEIOUaeéèêiou]) +\1u'\2)
m (Bot : Remplacement de texte automatisé (-<sub>0</sub> +₀)) |
m (Robot : Remplacement de texte automatisé (-\b([Qq])ue ([AEIOUaeéèêiou]) +\1u'\2)) |
||
|
La définition de ''VAF₂'' 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₁''.
La définition de ''VAF₁'' conduit à vouloir montrer
:''VAF₀'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
a(rttx)asss(rttx)a(rnon)a(ret)b(a(r<)b(rx)sss(rx))a(r=)b(rx)sss(rx)
Le même raisonnement que pour AF1 conduit à vouloir montrer
On va prouver que VAF0 est inclus dans VAF0 Moins Absurd1
Absurd2 =def Im par <-P-Prod de Extension de Z Dans N et Z’ Dans N et Z Egale Z’.
Supposons alors
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.
| |||