« Fondements des mathématiques/Preuve formelle de la cohérence de l'arithmétique formelle » : différence entre les versions

m
Robot : 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 que qu'ou <code>a(r=)bxy</code> n’est pas dans ''VAF₀'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans ''VAF₀'', pour tous x et y dans N.
 
:''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 que qu'a(r<)bxy n’est pas dans VAF0 ou a(r=)bxy n’est pas dans VAF0, pour tous x et y dans N.
 
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 que qu'a(r=)bxy soit dans VAF0 et que x et y sont dans N.
 
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.
143 371

modifications