Cohérence des axiomes de l'arithmétique formelle - Définition

Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs est disponible ici.

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

R3 si x

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

R13 si x=y et z

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

AF15 (pour tout x)(pour tout y)(si (x=y ou 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 naturelle 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

AF15 Pour tous x et y, si x=y ou x

AF14 équivaut à non(il existe x et y tels que x

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

AF15 équivaut à non(il existe x et y tels que (x=y ou 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. 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.

Le rôle des preuves de cohérence et des méthodes formelles Pour réaliser le programme de Hilbert on peut prouver la cohérence des théories en construisant des modèles, c’est-à-dire des ensembles de formules atomiques. L’ensemble des vérités atomiques de l’arithmétique élémentaire permet par exemple de prouver la cohérence des théories arithmétiques. Il ne suffit pas de définir un ensemble de formules atomiques, il faut prouver que c’est bien un modèle, c’est-à-dire que tous les axiomes sont vrais pour ce modèle. De telles preuves peuvent être données avec un langage et un raisonnement naturels parce qu’elles sont souvent très élémentaires. On peut être aussi sûr de la validité de ces preuves qu’on l’est de la validité de tous les principes élémentaires de raisonnement. Il est cependant souhaitable de formaliser les preuves naturelles. Il ne s’agit pas toujours de les rendre plus sûres, parce que certains raisonnements naturels peuvent être plus fiables que les calculs formalisés, étant plus compréhensibles. On peut se tromper dans les options de formalisation, mais, on ne se trompe pas si on applique avec attention des principes élémentaires et naturels sur des questions simples. Formaliser des preuves naturelles présente un intérêt plus pour montrer la justesse et la relative puissance de la formalisation que pour montrer la justesse des preuves elles-mêmes.

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.

Page générée en 0.035 seconde(s) - site hébergé chez Contabo
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
A propos - Informations légales | Partenaire: HD-Numérique
Version anglaise | Version allemande | Version espagnole | Version portugaise