« 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>1</sub> +₁) |
m Bot : Remplacement de texte automatisé (-<sub>2</sub> +₂) |
||
Ligne 66 :
: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(''
:non-F-Prod(''
: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 ''
La définition de ''
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.
| |||