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

m
Amélioration de la syntaxe de l'article.
m (Robot : Remplacement de texte automatisé (- l'opposition + l’opposition , - d'asile + d’asile , - s'adresser + s’adresser , - l'ensemble + l’ensemble , - d'argent + d’argent , - l'argent + l’argent , - l'augmentation + l’augmentat...)
m (Amélioration de la syntaxe de l'article.)
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. :
 
R1 (Règle 1) : si x=y alors sx=sy ;
 
R2 : si x=y alors x<sy ;
 
R3 : si x<y alors x<sy ;
 
R4 : si x=y alors x+0=y ;
 
R5 : si x+y=z alors y+x=z ;
 
R6 : si x+y=z alors sx+sy=sz ;
 
R7 : si x=x alors x.0=0 ;
 
R8 : si x.y=z alors y.x=z ;
 
R9 : si x.y=z alors x.sy=z+x ;
 
R10 : si x=y alors y=x ;
 
R11 : si x=y et y=z alors x=z ;
 
R12 : si x=y et y<z alors x<z ;
 
R13 : si x=y et z<y alors z<x.
 
Les éléments de VAF0 sont toutes les formules que l’on peut déduire de 0=0 en appliquant un nombre fini de fois les règles précédentes.
Pour obtenir les axiomes de AF, on peut commencer par traduire les règles de production en formules généralisées, c’est-à-dire qu’elles commencent par un opérateur de généralisation, et closes, c’est-à-dire sans variables libres.
 
Par exemple, la première règle est traduite par la formule suivante. :
 
AF1 (pour tout x)(pour tout y)(si x=y alors sx=sy).
 
On obtient ainsi treize axiomes. Il faut leur ajouter les deux suivants si l’on veut prouver des négations de faussetés atomiques. :
 
AF14 (pour tout x)(pour tout y)(si x<y alors non(x=y)) ;
 
AF15 (pour tout x)(pour tout y)(si (x=y ou x<y) alors non(y<x)).
 
< a été choisi comme prédicat fondamental justement pour que les axiomes de la négation des faussetés atomiques puissent être mis sous une forme aussi simple.
 
Pour toute propriété P des nombres,
* si P est vraie de 0,
* et si pour tout nombre x, si P est vraie de x alors P est vraie de sx,
alors pour tout nombre x, P est vraie de x
 
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, il faut alors traduire le principe d’induction complète par un schéma d’axiomes, un cadre formel qui détermine un nombre infini de formules qui sont toutes adoptées comme axiomes. Il y a autant d’axiomes d’induction complète qu’il y a de prédicats arithmétiques.
 
Soit P(x, y1…y<sub>1</sub>…, yny<sub>n</sub>) un prédicat qui contient x, y1…y<sub>1</sub>…., yny<sub>n</sub> comme variables libres, et elles seulement. La formule suivante est un axiome.
 
Pour tous y1…y<sub>1</sub>…., yny<sub>n</sub>,
* si P(0, y1…y<sub>1</sub>…, yny<sub>n</sub>),
* et si pour tout x, si P(x, y1…y<sub>1</sub>…, yny<sub>n</sub>), alors P(sx, y1…y<sub>1</sub>…, yny<sub>n</sub>),
alors pour tout z, P(z, y1…y<sub>1</sub>…, yny<sub>n</sub>).
 
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.
Il reste à prouver que les deux axiomes suivants sont vrais ainsi que tous les axiomes qui traduisent le principe d’induction complète.
 
AF14 Pour tous x et y, si x<y alors non(x=y).
 
AF15 Pour tous x et y, si x=y ou x<y alors non(y<x).
 
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. AF14 est donc vrai dans VAF0.
 
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 qu'AF14.
 
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…y<sub>1</sub>…., yny<sub>n</sub>) et des nombres c1…c<sub>1</sub>…., cnc<sub>n</sub> , tels qu’on ait à la fois (i), (ii) et (iii) .
 
(i) P(0, c1…c<sub>1</sub>…., cnc<sub>n</sub>).
 
(ii) Pour tout x, si P(x, c1…c<sub>1</sub>…., cnc<sub>n</sub>) alors P(sx, c1…c<sub>1</sub>…., cnc<sub>n</sub>).
 
(iii) non (pour tout z, P(z, c1…c<sub>1</sub>…., cnc<sub>n</sub>)).
 
(iii) équivaut à il existe un z tel que non P(z, c1…c<sub>1</sub>…., cnc<sub>n</sub>). Soit c ce nombre. P(c, c1…c<sub>1</sub>…., cnc<sub>n</sub>) serait donc faux dans VAF0 mais une suite de c déductions à partir de P(0, c1…c<sub>1</sub>…., cnc<sub>n</sub>) avec (ii) suffit pour prouver que P(c, c1…c<sub>1</sub>…., cnc<sub>n</sub>) est vrai. Il faut donc rejeter l’hypothèse que l’un des axiomes qui traduisent le principe d’induction complète est faux.
 
Cela termine cette preuve de la cohérence de AF. Elle revient principalement à dire que tous les axiomes de l’arithmétique sont évidemment vrais pour les nombres entiers, ce qui n’est pas vraiment une nouvelle extraordinaire. Mais cette preuve est importante parce qu’elle prouve qu’on peut prouver la cohérence des axiomes, et donc plus généralement, la fiabilité des principes.
96

modifications