« 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>5</sub> +₅) |
m Bot : Remplacement de texte automatisé (-<sub>0</sub> +₀) |
||
Ligne 1 :
La théorie ''Finitaire 1'' permet de formaliser la preuve naturelle de la cohérence de l’arithmétique formelle ''AF''.
Il faut montrer que l’ensemble des axiomes de ''AF'' est inclus dans l’ensemble ''VAF'' des vérités du modèle ''
== Pourquoi prouver des évidences ? ==
Les 13 axiomes de ''AF'' qui traduisent les 13 règles de production de ''
== La vérité de ''AF₁'' ==
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle ''R₁'' de ''
:''AF₁'' (pour tout ''x'')(pour tout ''y'')(si ''x = y'' alors ''sx = sy'')
Ligne 76 :
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 ou <code>a(r=)bxy</code> n’est pas dans ''
:''
:Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union … Prod13(X) ))
Supposons que <code>a(r=)bxy</code> soit dans ''
Il y a un w tel que <code>a(r=)bxy</code> est dans w et w est dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo
Ligne 100 :
<code>C(a(r=)bxy)a(r=)b(a(rs)x)a(rs)y</code> est dans Inst-R1 puisque x et y sont dans N et que N est inclus dans Tconst.
On en conclut que <code>a(r=)b(a(rs)x)a(rs)y</code> est dans Im par Prod1 de w et donc dans ''
Cela termine cette preuve de la vérité de ''AF₁'' dans ''
== La vérité de AF14 ==
|