« 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>4</sub> +₄)
m Bot : Remplacement de texte automatisé (-<sub>5</sub> +₅)
Ligne 16 :
:<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₁'' est dans ''VAF''. Montrons qu’il est dans ''VAF<sub>5</sub>VAF₅''.
 
:''VAF<sub>5</sub>VAF₅'' <math>\overset{\overset{def}{=}}{\,}</math> Union(non-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄''), et-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄''), ou-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄''), ex-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄''), tt-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄'') )
 
Montrons que ''AF₁'' est dans tt-V-Prod(''AAF₄'', ''VAF₄'', ''FAF₄'')