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

Aller à la navigation Aller à la recherche
m
Bot : Remplacement de texte automatisé (-oe +œ)
m (cat)
m (Bot : Remplacement de texte automatisé (-oe +œ))
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 oeuvreœuvre dans la preuve naturelle.
 
Cela termine cette preuve abrégée que Finitaire1 permet de prouver la cohérence de AF.
143 371

modifications

Menu de navigation