« Fondements des mathématiques/Preuve naturelle de la cohérence de l'arithmétique formelle » : différence entre les versions
Contenu supprimé Contenu ajouté
m Robot : Changement de type cosmétique |
m Robot : Remplacement de texte automatisé (-\b([Qq])ue ([AEIOUaeéèêiou]) +\1u'\2) |
||
Ligne 4 :
L’arithmétique formelle AF va être définie par un système d’axiomes. AF est l’ensemble de toutes les formules qui sont ou bien des axiomes, ou bien des conséquences logiques des axiomes.
Pour prouver
Nous allons commencer par rappeler la définition d’un modèle naturel pour AF, l’ensemble VAF0 des vérités atomiques de AF. Nous choisirons alors des axiomes adaptés à la définition de VAF0 et nous prouverons par un raisonnement naturel que ces axiomes sont vrais pour VAF0.
Ligne 89 :
AF15 équivaut à non(il existe x et y tels que (x=y ou x<y)et(non(y<x)) )
Il est vrai dans VAF0 pour la même raison
Supposons que l’un des axiomes qui traduisent le principe d’induction complète soit faux dans VAF0. Cela veut dire qu’il y a un prédicat P(x, y1…., yn) et des nombres c1…., cn , tels qu’on ait à la fois (i), (ii) et (iii) .
| |||