« 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é (-<sub>0</sub> +₀) |
m Robot : Remplacement de texte automatisé (-\b([Qq])ue ([AEIOUaeéèêiou]) +\1u'\2) |
||
Ligne 76 :
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
Ligne 113 :
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
Ligne 137 :
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.
| |||