Cohérence des axiomes de l'arithmétique formelle
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article 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 (Une définition est un discours qui dit ce qu'est une chose ou ce que signifie un nom. D'où la division entre les définitions réelles et les définitions...) 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 manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise,...) de base, 0, un opérateur (Le mot opérateur est employé dans les domaines :) unaire s, la fonction de succession, deux opérateurs binaires, + et . , l’addition et la multiplication (La multiplication est l'une des quatre opérations de l'arithmétique élémentaire avec l'addition, la soustraction et la division .), 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 (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) 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 (La généralisation est un procédé qui consiste à abstraire un ensemble de concepts ou d'objets en négligeant les détails de façon à...), et closes, c’est-à-dire sans variables libres.

Par exemple, la première règle est traduite par la formule suivante.

AF1 (pour tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) 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 (Les besoins se situent au niveau de l'interaction entre l'individu et l'environnement. Il est souvent fait un classement des besoins humains en trois grandes catégories : les besoins primaires, les besoins...) 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 (L'arithmétique est une branche des mathématiques qui comprend la partie de la théorie des nombres qui utilise des méthodes de la géométrie algébrique et de la théorie des groupes. On...) 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 (Le mot « infini » (-e, -s ; du latin finitus, « limité »), est un adjectif servant à qualifier quelque chose...) 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 (Les prédicats d’une théorie sont les formules qui contiennent des variables libres.) qui contient x, y1, ...., yn comme variables libres, et elles seulement. La formule suivante est un axiome (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en soi ») désigne une...).

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 (Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation...) du premier ordre, que l’on peut exposer par la méthode de la déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner). 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 (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution progressive allant du...) 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é (Un système est fiable lorsque la probabilité de remplir sa mission sur une durée donnée correspond à celle spécifiée dans le cahier des charges.) 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 (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un...) 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 (Le mot puissance est employé dans plusieurs domaines avec une signification particulière :) de la formalisation que pour montrer la justesse des preuves elles-mêmes.

Le second théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir d'axiomes. Un théorème est à...) d'incomplétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être...) 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 (Dans les technologies de l'information (TI), une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction d'affaire, d'un...) 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.091 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique