« 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 cat |
m Bot : Remplacement de texte automatisé (-oe +œ) |
||
Ligne 159 :
La preuve de cette contradiction est rendu aisée par le fait que VAF est clos par l’opération de conséquence logique, autrement dit, si une formule est la conséquence logique de formules qui sont dans VAF alors elle est aussi dans VAF.
Toutes ses preuves sont longues à écrire mais elles ne posent pas de véritables difficultés autres que la précision des définitions. Le raisonnement est une simple traduction formalisée du raisonnement mis en
Cela termine cette preuve abrégée que Finitaire1 permet de prouver la cohérence de AF.
| |||