Coherence des axiomes de l'arithmetique formelle

Cette page expose des axiomes pour l'arithmétique formelle et une preuve naturelle, connue des logiciens, de la cohérence de ces axiomes.

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.

R1 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 x+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.

Ces quinze axiomes ne suffisent pas parce qu’aucun d’entre eux ne dit que tous les nombres entiers sont obtenus à partir de 0 et d’un nombre fini d’applications de l’opérateur de succession.

Pour exprimer cette propriété essentielle de tous les nombres, on a besoin du principe d’induction complète. On peut l’énoncer de la façon suivante.

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

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, 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, ..., yn) un prédicat qui contient x, y1, ...., yn comme variables libres, et elles seulement. La formule suivante est un axiome.

Pour tous y1, ...., yn,

• 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.

Une preuve sémantique de la cohérence des axiomes de l’arithmétique formelle

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.

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 que 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, ...., yn) et des nombres c1, ...., cn, tels qu’on ait à la fois (i), (ii) et (iii) .

(i) P(0, c1, ...., cn)

(ii) Pour tout x, si P(x, c1, ...., cn) alors P(sx, c1, ...., cn)

(iii) non (pour tout z, P(z, c1, ...., cn))

(iii) équivaut à il existe un z tel que non P(z, c1, ...., cn). Soit c ce nombre. P(c, c1, ...., cn) serait donc faux dans VAF0 mais une suite de c déductions à partir de P(0, c1, ...., cn) avec (ii) suffit pour prouver que P(c, c1, ...., cn) 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. Le second théorème d'incomplétude de Gödel ne prouve pas qu’une preuve de la cohérence des axiomes de l’arithmétique formelle ne peut pas être donnée mais seulement qu’elle ne peut pas être formalisée à l’intérieur de l’arithmétique formelle.