Wikiversité

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

Navigation interactive dans l’historique
← Modification précédenteModification suivante →
Contenu supprimé Contenu ajouté
VisuelWikicode
m Bot : Remplacement de texte automatisé (-<sub>2</sub> +₂)
m Bot : Remplacement de texte automatisé (-<sub>3</sub> +₃)
Ligne 58 :
On veut déduire une contradiction à partir de ''hyp''. Il suffit de prouver que z’ n’est pas dans ''FAF<sub>4</sub>''.
 
:''FAF<sub>4</sub>'' =def Union(non-F-Prod(''AAF<sub>3</sub>AAF₃'', ''VAF<sub>3</sub>VAF₃'', ''FAF<sub>3</sub>FAF₃''), et-F-Prod(''AAF<sub>3</sub>AAF₃'', ''VAF<sub>3</sub>VAF₃'', ''FAF<sub>3</sub>FAF₃''), ou-F-Prod(''AAF<sub>3</sub>AAF₃'', ''VAF<sub>3</sub>VAF₃'', ''FAF<sub>3</sub>FAF₃''), ex-F-Prod(''AAF<sub>3</sub>AAF₃'', ''VAF<sub>3</sub>VAF₃'', ''FAF<sub>3</sub>FAF₃''), tt-F-Prod(''FAF<sub>3</sub>FAF₃'')
 
Montrons que z’ n’est pas dans tt-F-Prod(''FAF<sub>3</sub>FAF₃'').
 
Le même raisonnement que ci-dessus peut être répété et on est conduit à vouloir prouver que :
 
: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₃''.
 
:''FAF<sub>3</sub>FAF₃'' =def Union(non-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂''), et-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂''), ou-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂''), ex-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂''), tt-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂'')
 
:non-F-Prod(''AAF₂'', ''VAF₂'', ''FAF₂'') =def Ensemble-image par non-P-Prod de ''VAF₂''
Récupérée de « https://fr.wikiversity.org/wiki/Fondements_des_mathématiques/Preuve_formelle_de_la_cohérence_de_l%27arithmétique_formelle »