« Fondements des mathématiques/Preuve naturelle de la cohérence de l'arithmétique formelle » : différence entre les versions
Contenu supprimé Contenu ajouté
imported>Tavernierbot m Bot: Retouches cosmétiques |
|||
Ligne 1 :
Cette section expose des axiomes pour l’arithmétique formelle et une preuve naturelle de leur cohérence.
=== Les axiomes de l’arithmétique formelle ===
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 que AF est cohérente, il suffira de prouver que tous ses axiomes sont vrais pour un même modèle.
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.
VAF0 est défini avec un objet de base, 0, un opérateur unaire s, la fonction de succession, deux opérateurs binaires, + et . , l’addition et la multiplication, et deux prédicats binaires fondamentaux, = et <. L’unique formule initiale de VAF0 est 0=0. Ses règles de production sont les suivantes.
Ligne 63 :
Les propriétés P des nombres peuvent être identifiées aux prédicats de AF, c’est à dire aux formules arithmétiques qui contiennent des variables libres. Ces prédicats peuvent être considérés comme les ensembles de l’arithmétique formelle. (il existe un y tel que x=2.y) est par exemple un nom pour l’ensemble des nombres pairs.
On ne peut pas traduire le principe d’induction complète par une seule formule de l’arithmétique formelle parce que l’univers arithmétique est réduit aux nombres. Quand on dit, pour tout x, dans l’arithmétique formelle, cela veut dire, pour tout nombre x. On ne peut donc pas dire, pour toute propriété P des nombres. Pour résoudre ce problème,
Soit P(x, y1, ..., yn) un prédicat qui contient x, y1, ...., yn comme variables libres, et elles seulement. La formule suivante est un axiome.
Ligne 70 :
*si P(0, y1, ..., yn),
*et si pour tout x, si P(x, y1, ..., yn), alors P(sx, y1, ..., yn)
alors pour tout z, P(z, y1, ..., yn)
AF est l’ensemble de tous les axiomes cités jusqu’ici et de toutes leurs conséquences logiques par les règles du calcul des prédicats du premier ordre, que l’on peut exposer par la méthode de la déduction naturelle. Ces axiomes sont identiques ou équivalents à ceux de Peano.
=== La vérité des axiomes ===
Tous les axiomes de AF qui traduisent des règles de production de VAF0 sont évidemment vrais pour VAF0, puisque du fait même de sa définition, ses règles de production sont toujours vraies.
Ligne 85 :
AF14 équivaut à non(il existe x et y tels que x<y et x=y)
Quand on connait la signification arithmétique des symboles, toutes les règles de production de VAF0 sont des vérités arithmétiques, au sens où elles ne produisent que des conclusions vraies si les prémisses sont vraies. Elles ne peuvent donc jamais produire à la fois x<y et x=y.
AF15 équivaut à non(il existe x et y tels que (x=y ou x<y)et(non(y<x)) )
| |||