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

Aller à la navigation Aller à la recherche
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

Menu de navigation