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

m
Bot : Remplacement de texte automatisé (-<sub>2</sub> +₂)
m (Bot : Remplacement de texte automatisé (-<sub>1</sub> +₁))
m (Bot : Remplacement de texte automatisé (-<sub>2</sub> +₂))
:Si x et y sont dans ''N'' alors <code>a(rnon)a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans ''FAF<sub>3</sub>''.
 
:''FAF<sub>3</sub>'' =def Union(non-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂''), et-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂''), ou-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂''), ex-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂''), tt-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂'')
 
:non-F-Prod(''AAF<sub>2</sub>AAF₂'', ''VAF<sub>2</sub>VAF₂'', ''FAF<sub>2</sub>FAF₂'') =def Ensemble-image par non-P-Prod de ''VAF<sub>2</sub>VAF₂''
 
:non-P-Prod =def Fonction a(rnon)X
 
On veut alors montrer que <code>a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans ''VAF<sub>2</sub>VAF₂''.
 
La définition de ''VAF<sub>2</sub>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 ou <code>a(r=)bxy</code> n’est pas dans ''VAF<sub>0</sub>'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans ''VAF<sub>0</sub>'', pour tous x et y dans N.
143 371

modifications