Théorème d'incomplétude de Gödel

Les théorèmes d'incomplétude de Gödel sont deux théorèmes célèbres de logique mathématique, démontrés par Kurt Gödel en 1931 dans son article Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (Sur l'indécidabilité formelle des Principia Mathematica et des systèmes apparentés).

Introduction

Grossièrement, le premier 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 à...) énonce qu'une théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur...) suffisante pour faire de l'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 l'appelle plus...) est nécessairement incomplète, 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...) où il existe forcément des énoncés qui ne sont pas démontrables et dont la négation n'est pas non plus démontrable : c'est-à-dire qu'il existe des énoncés sur lesquels on sait qu'on ne pourra jamais rien dire dans le cadre de cette théorie. Sous le même genre d'hypothèses sur les théories considérées, le second théorème affirme qu'il existe un énoncé exprimant la cohérence de la théorie - le fait qu'elle ne permette pas de démontrer tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) et donc n'importe quoi - et que cet énoncé ne peut pas être démontré dans la théorie elle-même. À cause des hypothèses des théorèmes, toute théorie qui prétend formaliser l'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 tout », comme...) des mathématiques, comme la théorie des ensembles, est concernée. Faut-il pour autant renoncer à ce qu'un discours mathématique (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels...) ait une valeur de vérité (La notion de valeur de vérité consiste à attribuer aux énoncés des valeurs numériques au travers de fonctions dont il faudra définir les règles de...) universelle ? Sur quoi se fonder pour savoir s'il est cohérent, puisqu'il semble que l'on ne puisse y arriver par des moyens purement internes aux mathématiques ? Les théorèmes de Gödel ne donnent pas de réponse mais permettent d'écarter celles qui sont trop simples. Il faut déjà noter que ces deux limitations (énoncés dont la vérité est inaccessible, cohérence du discours) sont seulement relatives, comme la suite de l'article l'indiquera.

Ces théorèmes, et surtout leurs conséquences sur la conception de leur discipline qu'avaient les mathématiciens de l'époque, en particulier David Hilbert et ses élèves, étaient très inattendus. Peu de mathématiciens comprirent tout d'abord ces théorèmes et ce qu'ils impliquaient. Il faut compter parmi ceux-ci John von Neumann (John von Neumann, mathématicien et physicien américain d'origine hongroise, a apporté d'importantes contributions tant en mécanique quantique, qu'en analyse fonctionnelle, en théorie des ensembles, en informatique, en...), qui après avoir assisté au premier exposé de Gödel en 1930 sur le premier théorème 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...), lui envoya une lettre mentionnant un corollaire (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...) qui était le second théorème (que Gödel connaissait déjà). Paul Bernays également, proche collaborateur de David Hilbert, comprit très vite les conséquences de ces théorèmes sur les conceptions de ce dernier, et donna la première démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en s'appuyant sur un ensemble de...) détaillée du second théorème[1] dans l'ouvrage Grundlagen der Mathematik, (co-signé avec Hilbert). Enfin, Gödel se rendit plusieurs fois aux États-Unis dans les années 1930. Ses travaux eurent une grande audience auprès d'Alonzo Church (Alonzo Church 14 juin 1903 - 11 août 1995 fut un mathématicien (logicien) américain à qui l'on doit certains des fondements de l'informatique théorique.) et de ses élèves, Stephen Cole Kleene (Stephen Cole Kleene (né le 5 janvier 1909 à Hartford, mort le 25 janvier 1994) est un mathématicien et logicien états-unien.) et John Barkley Rosser, et jouèrent un rôle important dans la naissance de la théorie de la calculabilité (La théorie de la calculabilité (appelée aussi parfois théorie de la récursion) est une branche de la logique mathématique et de l'informatique théorique. Alors que la notion intuitive de fonction calculable est aussi vieille que les...).

Le second de la célèbre liste de problèmes que Hilbert présenta en 1900 à Paris (Paris est une ville française, capitale de la France et le chef-lieu de la région d’Île-de-France. Cette ville est construite sur une boucle de la Seine, au centre du bassin parisien, entre les confluents de la Marne et de la Seine en...) était celui de la démonstration de la cohérence de l'arithmétique. Toute la question, qui n'est pas éludée par Hilbert, est de savoir quels moyens on se donne pour une telle preuve. Le second théorème d'incomplétude montre qu'il faut une théorie qui doit être " plus forte " (en un sens qu'il faudrait préciser) que l'arithmétique elle-même. On considère généralement que la réponse apportée au second problème de Hilbert est négative. Gerhard Gentzen donna cependant en 1936 une preuve de cohérence de l'arithmétique, de façon compatible bien-sûr avec le second théorème de Gödel. La preuve est fort intéressante, mais sa signification en tant que preuve de cohérence reste discutable (voir les articles sur Gentzen et sur le programme de Hilbert).

Pour mieux comprendre le contexte historique qui a conduit Gödel à démontrer ses théorèmes et l'impact de ceux-ci à l'époque, consulter l'article sur le programme de Hilbert.

La suite de l'article ne cherche pas à suivre exactement le contenu de l'article de Gödel. Quelques points se sont précisés depuis. On commence par une présentation encore un peu informelle. Des esquisses des preuves des théorèmes, ainsi que des précisions sur leurs énoncés, sont données en fin d'article.

Énoncés des deux théorèmes

Le premier théorème d'incomplétude peut être énoncé de la façon encore un peu approximative suivante (les termes techniques sont expliqués dans le paragraphe suivant).

Dans n'importe quelle théorie récursivement axiomatisable, cohérente et capable de " formaliser l'arithmétique ", on peut construire un énoncé arithmétique qui ne peut être ni prouvé ni réfuté dans cette théorie.

De tels énoncés sont dits indécidables dans cette théorie. On dit également indépendant de la théorie.

Toujours dans l'article de 1931, Gödel en déduit le second théorème d'incomplétude :

Si T est une théorie cohérente qui satisfait des hypothèses analogues, la cohérence de T, qui peut s'exprimer dans la théorie T, n'est pas démontrable dans T.

Ces deux théorèmes ont été prouvés pour l'arithmétique de Peano et donc pour les théories plus fortes que celle-ci, en particulier les théories destinées à fonder les mathématiques, telles que la théorie des ensembles, ou les Principia Mathematica...

Les conditions d'application des théorèmes

Pour fixer les idées, on considère dorénavant que les théories en question sont, comme celles que l'on vient de mentionner (arithmétique de Peano, théorie des ensembles), des théories du premier ordre de la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la...) classique, même si les théorèmes d'incomplétude restent valides, sous les mêmes conditions, par exemple en logique intuitionniste[2] ou en passant à l'ordre supérieur.

  • Par théorie récursivement axiomatisable, on entend que la théorie peut être axiomatisée de façon qu'il soit possible de reconnaître de façon purement mécanique (Dans le langage courant, la mécanique est le domaine des machines, moteurs, véhicules, organes (engrenages, poulies, courroies, vilebrequins, arbres de transmission, pistons,...) les axiomes parmi les énoncés du langage de la théorie. C'est le cas évidemment des théories utilisées pour formaliser tout ou partie des mathématiques usuelles.
  • Une théorie est cohérente si aucune contradiction (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.) ne peut être prouvée à partir de ses axiomes. On dit aussi qu'elle est consistante ou non-contradictoire. Pour le premier théorème d'incomplétude, Gödel faisait une hypothèse de cohérence un peu plus forte. L'hypothèse de cohérence simple suffit de toute façon pour le second théorème, qui n'énonce que la non-démontrabilité de l'énoncé de cohérence. J. B. Rosser a donné en 1936 une démonstration du premier théorème d'incomplétude sous la simple hypothèse de cohérence. À proprement parler, l'énoncé du premier théorème d'incomplétude donné au début de cet article n'est donc pas exactement celui de Gödel. On le nomme souvent théorème de Gödel-Rosser.
  • Une théorie permet de formaliser l'arithmétique si, d'une part il est possible de définir (en un sens qu'il faudrait préciser) les entiers (donnés par zéro (Le chiffre zéro (de l’italien zero, dérivé de l’arabe sifr, d’abord transcrit zefiro en italien) est un symbole marquant une position vide dans l’écriture des...) et la fonction successeur), avec les opérations usuelles, au moins l'addition (L'addition est une opération élémentaire, permettant notamment de décrire la réunion de quantités ou l'adjonction de...) 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 si d'autre part un certain nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) d'énoncés sur les entiers sont prouvables dans la théorie. L'arithmétique de Peano est une telle théorie, et satisfait les hypothèses des deux théorèmes d'incomplétude. En fait une théorie arithmétique beaucoup plus faible suffit pour le premier (la récurrence n'est essentiellement pas utile). Pour le second, il faut un minimum de récurrence.
    Il est remarquable que pour formaliser l'arithmétique, l'addition et la multiplication suffisent (en plus de zéro et du successeur). C'est le tout premier pas vers la solution du dixième problème de Hilbert (voir théorème de Matiyasevich). L'addition seule ne suffit pas : l'arithmétique de Presburger (L'arithmétique de Presburger est une théorie du premier ordre, dans le langage de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition...), qui est la théorie obtenue en restreignant l'arithmétique de Peano au langage de l'addition (en plus de zéro et du successeur), est complète.

Conséquences immédiates du premier théorème d'incomplétude

On peut reformuler le premier théorème d'incomplétude en disant que si une théorie T satisfait les hypothèses utiles, il existe un énoncé tel que chacune des deux théories obtenues l'une en ajoutant à T cet énoncé comme axiome (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en soi ») désigne une...), l'autre en ajoutant la négation de cet énoncé, sont cohérentes. Donnons en la démonstration.

Étant donné un énoncé G, notons non G sa négation. On montre facilement qu'un énoncé G n'est pas démontrable dans T si et seulement si la théorie T + non G (la théorie T à laquelle on ajoute l'axiome non G) est cohérente. En effet, si G est démontrable dans T, T + non G est évidemment contradictoire. Réciproquement, supposons T + non G contradictoire. Cela signifie que, dans la théorie T, on peut déduire de non G une contradiction. On en déduit que G est conséquence de T (c'est un raisonnement par l'absurde).

Il est donc équivalent de dire qu'un énoncé G est indécidable dans une théorie cohérente T, et de dire que les deux théories T + non G et T + G sont cohérentes. L'énoncé G n'étant évidemment pas indécidable dans chacune de ces deux théories, on voit que la notion d'énoncé indécidable est par nature relative à une théorie 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 événement, etc.).

Ainsi, si G est l'énoncé indécidable donné pour T par le premier théorème d'incomplétude, on aura, en appliquant à nouveau ce théorème, un nouvel énoncé indécidable dans la théorie T + G (et donc d'ailleurs indécidable aussi dans la théorie T).

De fait, quand le théorème d'incomplétude s'applique à une théorie T, il s'applique à toutes les extensions cohérentes de cette théorie, tant qu'elles restent récursivement axiomatisables : il n'y a aucun moyen effectif de compléter une telle théorie.

Il faut également noter que, quelle que soit la théorie en jeu, Gödel a montré que l'énoncé obtenu est arithmétique, c’est-à-dire qu'on peut l'exprimer dans le langage de l'arithmétique. Il s'agit même d'un énoncé de l'arithmétique qui, bien que fastidieux à écrire explicitement, est logiquement assez simple (en un sens qui sera précisé en fin d'article). Par exemple, on obtiendra par le théorème de Gödel appliqué à la théorie des ensembles de Zermelo-Fraenkel un énoncé arithmétique mais qui sera indécidable dans celle-ci.

Conséquences immédiates du second théorème d'incomplétude

Il peut être utile pour comprendre l'énoncé du second théorème d'incomplétude, de le reformuler par contraposée :

Si T est une théorie récursivement axiomatisable qui permet de formaliser " suffisamment d'arithmétique ", et si T prouve un énoncé exprimant qu'elle est cohérente, alors T est contradictoire.

En revanche, une théorie qui démontre un énoncé exprimant qu'elle n'est pas cohérente, peut très bien ne pas être contradictoire, comme on le déduit du second théorème d'incomplétude lui-même !

Donnons en une preuve. Appelons cohT un énoncé qui exprime la cohérence de T dans la théorie T. De la même façon qu'au paragraphe précédent pour le premier théorème, on reformule le second théorème d'incomplétude en disant que, sous les hypothèses utiles sur T, si la théorie T est cohérente, la théorie T'=T + non cohT est encore cohérente. Rappelons que " T n'est pas cohérente ", signifie qu'il existe une preuve d'une contradiction dans T. Une preuve dans T est aussi une preuve dans T' , qui a juste un axiome supplémentaire. Il est donc simple de montrer dans une théorie telle que T, qui satisfait les hypothèses du théorème de Gödel, que non cohT a pour conséquence non cohT' (n'oublions pas cependant que cohT et cohT sont des énoncés exprimés dans le langage de ces théories, il faudrait, pour que la preuve soit vraiment complète, rentrer dans le détail de cette représentation pour montrer cette implication). On a donc déduit du second théorème de complé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 ajouté, en un sens qu'il faut préciser...), et de l'existence d'une théorie cohérente T qui satisfait les hypothèses de ce théorème -- prenons par exemple l'arithmétique de Peano -- l'existence d'une théorie T' cohérente qui démontre non cohT', à savoir un énoncé exprimant qu'elle n'est pas cohérente. De telles théories sont fort heureusement pathologiques : on n'en a jamais rencontré parmi les théories mathématiques usuelles. Ce résultat peut choquer l'intuition, mais il faut bien voir que l'on peut reformuler le second théorème d'incomplétude en disant que toute théorie cohérente qui satisfait les hypothèses utiles a une extension qui démontre la négation de sa cohérence.

A contrario une théorie incohérente, dans laquelle tous les énoncés sont prouvables, démontrera évidemment un énoncé exprimant qu'elle est cohérente.

On voit par ces diverses remarques que le second théorème d'incomplétude ne dit rien en défaveur de la cohérence d'une théorie à laquelle il s'applique, par exemple la cohérence de l'arithmétique de Peano. Tout ce qu'il dit de cette dernière, c'est qu'elle ne peut se prouver que dans une théorie logiquement plus forte.

Un autre exemple d'application simple, mais assez surprenante, du second théorème d'incomplétude est le théorème de Löb, qui affirme que, dans une théorie T qui satisfait les hypothèses utiles, prouver dans T un énoncé sous l'hypothèse que cet énoncé est prouvable dans la théorie, revient à prouver l'énoncé. Autrement dit cette hypothèse est inutile.

Vérité et démontrabilité

On va introduire la notion de vérité, parfois méconnue en dehors de la logique mathématique (La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme. Ses débuts furent marqués par la rencontre entre deux idées nouvelles :), mais utile pour comprendre les théorèmes de Gödel. On va voir que la vérité est une notion mathématique, assez intuitive, mais qui ne se formalise pas dans des théories aussi simples que celles dans lesquelles se formalise la démontrabilité : il faut un minimum de théorie des ensembles, alors que la démontrabilité se contente de l'arithmétique. La notion de vérité que l'on va utiliser se définit mathématiquement (mais dans une théorie plus forte que celle étudiée). Le vocabulaire utilisé correspond à l'intuition, la notion est très commode. Mais il n'est pas 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 :...) d'attribuer une valeur excessive à cette notion pour l'utiliser. Par exemple, Gödel construit effectivement un énoncé dont on montre qu'il est vrai dans N, ce que l'on peut interpréter par " on sait le prouver dans une théorie plus forte que celle de départ ".

Les théorèmes de Gödel portent sur des théories pouvant formaliser suffisamment d'arithmétique ; pour simplifier, on se limite de surcroît dans ce paragraphe aux théories arithmétiques, c'est-à-dire aux théories qui ne parlent que des entiers.

Vérité dans le modèle standard de l'arithmétique

Alors que la démontrabilité est définie par rapport à une théorie, un système d'axiomes, la vérité est définie relativement à un modèle, une structure mathématique : un ensemble muni de lois et relations. Si dans une théorie un énoncé peut être indécidable, dans un modèle un énoncé est vrai ou faux, pas d'autre alternative. Nous allons dans la suite nous intéresser à la vérité dans le modèle standard de l'arithmétique, les entiers que "tout le monde (Le mot monde peut désigner :) connaît", que l'on note N[3]. C'est une structure tellement intuitive que ces précisions peuvent paraître superflues. Mais justement le théorème d'incomplétude de Gödel montre l'existence de structures mathématiques qui ressemblent étrangement aux entiers, par exemple elles vérifient tous les axiomes de l'arithmétique de Peano y compris la récurrence, mais qui ne sont pas les entiers usuels, puisqu'elles vérifient un énoncé faux dans N. En effet, si G est une formule indécidable dans T, prenons l'arithmétique de Peano pour T, nous avons vu à la section précédente que les théories T + G et T + non G sont cohérentes. Cela signifie, d'après le théorème de complétude du même Gödel, que ces théories ont chacune un modèle. Ces deux modèles ne satisfont pas les mêmes énoncés : ils ne peuvent être identiques. L'un d'entre eux au moins n'est donc pas le modèle standard. Quand on démontre le théorème de Gödel, on sait d'ailleurs quel est des deux l'énoncé vrai dans le modèle standard (sachant que la théorie T est cohérente). Le fait que l'on sache qu'un énoncé est vrai dans le modèle N, sans savoir le démontrer dans la théorie arithmétique de Peano, signifie simplement qu'on sait le démontrer dans une théorie arithmétique plus forte, que l'on n'a pas forcément cherché à expliciter.

À l'époque où Gödel démontre son théorème, la notion de vérité n'est pas vraiment formalisée, même si elle est connue de ce dernier, puiqu'il a démontré en 1929 le théorème de complétude. 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...) utilisée actuellement est due à Alfred Tarski, on la trouve dans un article publié en 1956.

Définissons la vérité dans N. Le langage a pour seul symbole de constante 0, pour seuls symboles de fonction s (la fonction successeur, qui ajoute 1), + et ×, pour seul symbole de relation en plus de l'égalité, le symbole d'inégalité ≤.

Le modèle standard se définit simplement : les seuls éléments de l'ensemble de base du modèle sont les entiers usuels, tous décrits par les termes du langage de la forme s ... s 0 (où s est le signe pour la fonction successeur, "ajouter 1"), c’est-à-dire la notation unaire bien connue qui correspond à l'idée primitive d'entier. Les termes du langage sont essentiellement des polynômes à plusieurs variables et à coefficients entiers positifs, les formules atomiques, qui sont les énoncés élémentaires, sans symbole logique, des égalités ou inégalités polynômiales. Pour définir le modèle il reste à décrire les formules atomiques closes, c’est-à-dire sans variable, vraies et fausses.

On définit facilement la vérité dans N des égalités et inégalités polynômiales sur les entiers (pas de variable !) notés de cette façon, et on peut même le faire mécaniquement, c’est-à-dire que la vérité des énoncés atomiques (égalités et inégalités polynômiales closes) est décidable (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.) au sens algorithmique (L'algorithmique est l’ensemble des règles et des techniques qui sont impliquées dans la définition et la conception d'algorithmes, c'est à dire de processus...). Les algorithmes en jeu sont essentiellement ceux de l'addition et de la multiplication en base 1, conceptuellement plus simples que ceux que l'on enseigne à l'école primaire pour la base 10 (bien que probablement plus fastidieux à utiliser).

A partir de là, on a défini le modèle, et donc on a la définition par induction de la vérité d'une formule quelconque dans ce modèle. Sans rentrer dans la définition formelle, observons quelques cas particuliers. Tout d'abord la vérité des formules closes sans quantificateurs reste décidable : on peut se ramener à des conjonctions et disjonctions d'égalités et d'inégalités (≠ et ≤) polynômiales. Passons aux quantificateurs, un énoncé du genre ∃x(P(x)=Q(x))P et Q sont des polynômes à une seule variable, est vrai quand on peut trouver un entier n tel que P(n)=Q(n). Remarquez que s'il existe un tel entier, une machine pourra le trouver, en essayant les entiers les uns après les autres par ordre croissant. Mais la machine ne s'arrêtera pas s'il n'existe pas de tel entier. Il n'y a pas d'évidence que la vérification de telles formules est algorithmiquement décidable (et elle ne l'est pas).

La situation (En géographie, la situation est un concept spatial permettant la localisation relative d'un espace par rapport à son environnement proche ou non. Il inscrit un lieu dans un cadre plus général afin de le...) est "pire" pour le quantificateur universel : un énoncé du genre ∀ x(P(x)=Q(x)) est vrai si pour chaque entier n, l'égalité P(n)=Q(n) est vraie : c'est bien défini, mais, si l'on suit la définition, cela demande une infinité de vérifications ! On voit bien la différence entre vérité et démontrabilité. Une preuve est nécessairement finie, et de plus on doit pouvoir reconnaître mécaniquement une preuve formelle. Pour démontrer un énoncé universel tel que celui-ci, habituellement on fait une récurrence. Sommairement, une preuve par récurrence est une façon finie de représenter une infinité de vérifications. La récurrence peut se "déplier" de façon à construire une infinité de preuves, une pour chaque entier. Cependant la récurrence introduit une certaine uniformité dans ces preuves[4]. Il n'y a aucune évidence qu'ainsi l'on puisse capturer la vérité dans N de tous les énoncés universels, et le théorème de Gödel montre justement que ce n'est pas le cas. L'énoncé de Gödel, qui est vrai dans N et non démontrable est justement un énoncé universel, appelons le ∀ x H(x). Prenons le cas de l'arithmétique de Peano. Quand on définit précisément l'énoncé, on montre que pour chaque entier n, H(n) est prouvable dans l'arithmétique de Peano. Mais on ne peut pas démontrer ∀ x H(x)[5].

Remarquons que, quand on a un moyen mécanique de décider la vérité dans N de certaines classes d'énoncés, par exemple les énoncés sans quantificateurs, on a en particulier une preuve de ces énoncés, ou de leurs négations, au sens non formel de cette notion, sans faire forcément attention à la théorie dans laquelle se dérive cette preuve. Dans les cas abordés ci-dessus, ces preuves se dérivent effectivement dans les théories pour lesquelles on peut démontrer les théorèmes de Gödel.

Vérité et incomplétude

Rappelons que si l'on démontre un énoncé à partir d'énoncés vrais dans un modèle, l'énoncé obtenu est vrai dans ce modèle, et que, dans un modèle, un énoncé (une formule close) est soit vrai soit faux. Par conséquent la théorie des énoncés vrais dans N est close par déduction et complète. On déduit immédiatement du premier théorème d'incomplétude que

La théorie des énoncés vrais dans N n'est pas récursivement axiomatisable.

et donc, la vérité étant close par déduction

Si T est une théorie récursivement axiomatisable qui permet de formaliser "suffisamment d'arithmétique", et dont tous les axiomes sont vrais dans N, il existe un énoncé G vrai dans N qui n'est pas démontrable dans T.

C'est un théorème d'incomplétude, plus faible cependant que le premier théorème d'incomplétude de Gödel, car il s'applique à moins de théories, les hypothèses étant nettement plus fortes. Par ailleurs on ne peut le formaliser directement dans l'arithmétique, pour en déduire le second théorème d'incomplétude[6]. Tel quel il se déduit d'ailleurs du Théorème de Tarski (Le théorème de Tarski, ou théorème de non définissabilité de Tarski, peut s'énoncer informellement ainsi : on ne peut définir dans le langage...) (1933), qui est plus facile à démontrer que celui de Gödel. Comme l'énoncé G non démontrable est vrai dans N et que la théorie ne démontre que des énoncés vrais dans N, la négation de cet énoncé n'est pas non plus démontrable. Par ailleurs comme la théorie T a un modèle, elle est cohérente.

Il est possible cependant de donner une assertion (Dans la langue française, le mot assertion (n,f) représente une vérité absolue : il définit une proposition reconnue comme vraie. -> voir Wiktionary) sous cette forme qui soit vraiment équivalente à celle démontrée par Gödel. On peut en effet préciser dans l'énoncé du théorème la complexité (La complexité est une notion utilisée en philosophie, épistémologie (par exemple par Anthony Wilden ou Edgar Morin), en physique, en biologie (par exemple...) logique de l'énoncé G ci-dessus. Alors, plutôt que de supposer que tous les axiomes de la théorie, et donc finalement tous ses théorèmes, sont vrais dans N, on peut se contenter d'une hypothèse sur les axiomes de la théorie qui a pour conséquence que tous les théorèmes de la complexité logique de la négation de G sont vrais dans N. C'est le cas justement de l'hypothèse de cohérence que faisait Gödel (explicitée dans une note en bas de page ultérieure). Une telle assertion est donnée (Dans les technologies de l'information, une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction, d'un événement, etc.) à la fin du paragraphe diagonalisation (La diagonalisation est un procédé d'algèbre linéaire. Il s'applique à des endomorphismes d'un espace vectoriel. Il consiste à rechercher une base de l'espace...) dans la suite de l'article.

Des exemples de systèmes incomplets et d'énoncés indécidables

L'existence de théories incomplètes est banale. Beaucoup de théories, comme la théorie des groupes, des anneaux, des corps, ne sont pas complètes : par exemple on peut dire au premier ordre qu'un groupe ou un corps a 2 éléments, ou 3 éléments. C'est différent pour l'arithmétique, on aurait souhaité capturer par une axiomatique toutes les propriétés des entiers naturels. Pour les théories destinées à fonder les mathématiques, Principia Mathematica ou théorie axiomatique des ensembles (Il existe plusieurs versions formelles de la théorie des ensembles, mais quand on parle de « la » théorie axiomatique des ensembles, on désigne habituellement sous ce nom la théorie ZFC. Au...), on peut s'attendre à ne pas avoir encore découvert tous les axiomes. Mais le théorème de Gödel affirme qu'il restera toujours des énoncés indécidables (tant que la théorie reste récursivement axiomatisable).

Il existe également des théories complètes intéressantes, comme l'arithmétique de Presburger déjà évoquée, la théorie des corps algébriquement clos d'une caractéristique donnée, la théorie des corps réels clos, et la géométrie (La géométrie est la partie des mathématiques qui étudie les figures de l'espace de dimension 3 (géométrie euclidienne) et, depuis le...) élémentaire qui lui est associée.

Énoncés indécidables dans l'arithmétique de Peano

Appliqués à l'arithmétique, les théorèmes de Gödel fournissent des énoncés dont la signification est tout à fait intéressante, puisqu'il s'agit de la cohérence de la théorie. Cependant ces énoncés dépendent du codage (De façon générale un codage permet de passer d'une représentation des données vers une autre.) choisi. Ils sont pénibles à écrire explicitement.

Paris et Harrington ont montré en 1977 qu'un renforcement du théorème de Ramsey fini, vrai dans N, n'est pas démontrable dans l'arithmétique de Peano. Il s'agit du premier exemple d'énoncé indécidable dans l'arithmétique qui n'utilise pas de codage du langage. Depuis, on en a découvert d'autres. Le théorème de Goodstein (En logique mathématique, le théorème de Goodstein est un énoncé arithmétique qui est indécidable dans l'axiomatique des entiers naturels de Peano, mais peut être prouvé en...) est un tel énoncé ; sa preuve est particulièrement simple (quand on connaît les ordinaux), mais utilise une induction jusqu’à l'ordinal dénombrable ε0. Kirby et Paris ont démontré en 1982 que l'on ne peut pas prouver ce théorème dans l'arithmétique de Peano.

Les énoncés de ce genre qui ont été découverts sont des résultats de combinatoire (En mathématiques, la combinatoire, appelée aussi analyse combinatoire, étudie les configurations de collections finies d'objets ou les combinaisons d'ensembles...). Leur preuve n'est pas nécessairement très compliquée, et en fait il n'y a aucune raison de penser qu'il y a un lien entre complexité technique d'une preuve et possibilité de formaliser celle-ci dans l'arithmétique de Peano.

Énoncés indécidables en théorie des ensembles

En théorie des ensembles, on a d'autres énoncés indécidables que ceux fournis par le théorème de Gödel qui peuvent être de nature différente (En mathématiques, la différente est définie en théorie algébrique des nombres pour mesurer l'éventuel défaut de dualité d'une application définie à l'aide de la trace, dans l'anneau des entiers...). Ainsi, d'après des travaux de Gödel, puis de Paul Cohen, l'axiome du choix et l'hypothèse du continu sont des énoncés indécidables dans ZF la théorie des ensemble (La théorie des ensembles est une branche des mathématiques créée initialement par le mathématicien allemand Georg Cantor à la fin du XIXe siècle.) de Zermelo et Fraenkel, le second étant d'ailleurs indécidable dans ZFC (En mathématiques, l'abréviation ZF désigne la théorie de Zermelo-Fraenkel, ZFC quand elle comprend l'axiome du choix, théorie axiomatique des ensembles la plus couramment...) (ZF plus l'axiome du choix). Mais d'une part, ce ne sont pas des énoncés arithmétiques. D'autre part, la théorie obtenue en ajoutant à ZF l'axiome du choix ou sa négation est équi-cohérente à ZF : la cohérence de l'une entraîne la cohérence de l'autre et réciproquement. De même pour l'hypothèse du continu. Ce n'est pas le cas pour un énoncé exprimant la cohérence de ZF, d'après justement le second théorème d'incomplétude. De même pour l'un des deux énoncés obtenus par les preuves usuelles du premier théorème d'incomplétude (il est équivalent à un énoncé de cohérence).

Dès que l'on peut montrer dans une théorie des ensembles T+A, qu'un ensemble (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, et qui peut être désigné par une étiquette verbale. Il est...) de la théorie) est modèle de la théorie des ensembles T, c’est-à-dire la cohérence de T, on déduit par le second théorème d'incomplétude que, si T est cohérente, A n'est pas démontrable dans T. On montre ainsi que certains axiomes qui affirment l'existence de "grands" cardinaux, ne sont pas démontrables dans ZFC.

Théorèmes d'incomplétude et calculabilité

La notion de calculabilité intervient à divers titres à propos des théorèmes d'incomplétude. On l'a utilisée pour en définir les hypothèses. Elle intervient dans la preuve du premier théorème d'incomplétude (Gödel utilise les fonctions récursives primitives). Enfin incomplétude et indécidabilité de l'arithmétique sont liées.

Indécidabilité algorithmique

Il y a un lien étroit entre décidabilité algorithmique d'une théorie, l'existence d'une méthode mécanique pour tester si un énoncé est ou non un théorème, et complétude de cette théorie. Une théorie récursivement axiomatisable et complète est décidable. On peut donc prouver le premier théorème d'incomplétude en montrant qu'une théorie qui satisfait les hypothèses utiles est indécidable. Ce résultat, l'indécidabilité algorithmique des théories qui satisfont les hypothèses du premier théorème d'incomplétude, a été démontré indépendamment par Turing et Church en 1936 (voir problème de la décision), en utilisant les méthodes développées par Gödel pour son premier théorème d'incomplétude. Pour un résultat d'indécidabilité, qui est un résultat négatif, il faut avoir formalisé la calculabilité, et être convaincu que cette formalisation est correcte, conviction qui ne peut reposer seulement sur des bases mathématiques. En 1931, Gödel connaît un modèle de calcul que l'on dirait maintenant Turing-complet (Le terme Turing-complet[1] désigne en informatique un système formel ayant au moins le pouvoir des machines de Turing.), les fonctions récursives générales, décrit dans une lettre que Jacques Herbrand lui a adressée, et qu'il a lui-même précisé et exposé en 1934. Cependant il n'est pas convaincu à l'époque d'avoir décrit ainsi toutes les fonctions calculables. À la suite de travaux de Kleene, Church, et Turing, ces deux derniers ont énoncé indépendamment en 1936 la thèse (Une thèse (du nom grec thesis, se traduisant par « action de poser ») est l'affirmation ou la prise de position d'un locuteur, à...) de Church : les fonctions calculables sont les fonctions récursives générales.

On peut être plus précis en donnant une classe restreinte d'énoncés pour laquelle la prouvabilité est indécidable. Si on reprend les arguments développés dans le paragraphe Vérité et démontrabilité ci-dessus, on voit par exemple que la classe des énoncés sans quantificateurs (et sans variables) est, elle, décidable.

En utilisant les arguments développés par Gödel, on montre que la prouvabilité des énoncés Σ1 est indécidable. Sans entrer dans le détail de la définition des formules Σ1 (faite ci-dessous), cela ne semble pas si loin d'une solution négative au dixième problème de Hilbert : l'existence d'un algorithme de décision pour la résolution des équations diophantiennes. Mais il fallu plusieurs dizaines d'années et les efforts successifs de plusieurs mathématiciens dont Martin Davis, Hilary Putnam, Julia Robinson et finalement Youri Matiiassevitch pour y arriver en 1970 (voir théorème de Matiiassevitch).

On peut tout à fait déduire le premier théorème de Gödel du théorème de Matiiassevitch. Cela peut paraître artificiel, puiqu'un résultat d'indécidabilité beaucoup plus facile à démontrer suffit. Mais on peut en déduire des énoncés indécidables d'une forme particulièrement simple. En effet, le théorème de Matiiassevitch équivaut à dire que la vérité des énoncés (formules closes) qui s'écrivent comme des égalités polynomiales quantifiées existentiellement, n'est pas décidable. Or :

  • on peut reconnaître mécaniquement de tels énoncés, et donc leurs négations ;
  • l'ensemble des tels énoncés vrais est récursivement énumérable (Intuitivement un ensemble est récursivement énumérable s'il existe un procédé mécanique (en gros qui peut être réalisé par un ordinateur)...), et donc, d'après le théorème de Matiiassevitch, l'ensemble des tels énoncés faux n'est pas récursivement énumérable ;
  • l'ensemble des théorèmes d'une théorie récursivement axiomatisable est récursivement énumérable (voir Théorie récursivement axiomatisable), et donc l'ensemble des théorèmes qui s'écrivent comme la négation d'une égalité polynômiale quantifiée existentiellement également ;
  • l'hypothèse de cohérence que fait Gödel pour son premier théorème d'incomplétude a pour conséquence directe que des égalités quantifiées existentiellement et fausses ne peuvent être démontrables.

On en déduit qu'il existe des énoncés vrais non démontrables, qui s'écrivent comme la négation d'une égalité polynômiale quantifiée existentiellement, ou plus simplement comme une inégalité polynômiale quantifiée universellement.

Une preuve partielle du premier théorème d'incomplétude

La preuve par Gödel de son premier théorème d'incomplétude utilise essentiellement deux ingrédients :

  • le codage par des nombres entiers du langage et des fonctions qui permettent de le manipuler, ce que l'on appelle l'arithmétisation de la syntaxe ;
  • un argument diagonal (Dans les preuves mathématiques, notamment celles de logique mathématique, l'argument diagonal est un mécanisme de construction réflexive menant le plus souvent à une impossibilité. Une telle construction est donc basée...) qui, en utilisant l'arithmétisation de la syntaxe, fait apparaître un énoncé similaire au paradoxe (Un paradoxe est une proposition qui contient ou semble contenir une contradiction logique, ou un raisonnement qui, bien que sans faille apparente,...) du menteur : l'énoncé de Gödel est équivalent, via codage, à un énoncé affirmant sa propre non prouvabilité dans la théorie considérée.

Mais l'énoncé de Gödel n'est pas paradoxal. Il est vrai dans N, car s'il était faux, il serait prouvable. Or cet énoncé est de complexité logique suffisamment simple pour que sa prouvabilité dans une théorie cohérente capable de coder l'arithmétique entraîne sa vérité dans N (on n'a pas besoin de supposer que N est modèle de la théorie). Il est donc vrai dans N. Il n'est donc pas prouvable, par définition de l'énoncé.

Pour montrer que la négation de l'énoncé de Gödel n'est pas non plus prouvable, il faut une hypothèse de cohérence plus forte, comme celle qu'a faite Gödel. Rosser a modifié astucieusement l'énoncé pour pouvoir utiliser simplement la cohérence. En ce qui concerne la preuve de Gödel l'argument est le suivant : l'énoncé étant vrai, sa négation est fausse. Si on supposait que N est modèle de la théorie, cela suffirait pour qu'elle ne soit pas démontrable. Mais Gödel a construit un énoncé d'une complexité logique suffisamment faible pour qu'une hypothèse beaucoup moins forte suffise : il s'agit essentiellement de dire que de tels énoncés faux ne peuvent être démontrables, et il peut l'exprimer de façon syntaxique.

La preuve esquissée ci-dessus est reprise de façon plus précise dans le paragraphe "diagonalisation".

Arithmétisation de la syntaxe

À l'époque actuelle, quiconque connait un peu d'informatique (L´informatique - contraction d´information et automatique - est le domaine d'activité scientifique, technique et industriel en rapport avec le...) n'a aucun mal à imaginer que l'on puisse représenter les énoncés d'une théorie par des nombres. Cependant il faut également manipuler ces codages dans la théorie. La difficulté réside dans les restrictions du langage : une théorie du premier ordre avec essentiellement l'addition et la multiplication comme symboles de fonction. C'est la difficulté que Gödel résout pour montrer que la prouvabilité peut être représentée par une formule dans la théorie.

La suite est un peu technique. En première lecture, on peut simplifier l'argumentation en supposant que N est modèle de T, auquel cas on n'a pas besoin d'être attentif à la complexité logique de l'énoncé. La partie sur la fonction β et la représentation de la récurrence reste utile. On précise également des notions, et des résultats qui ont été évoqués ou rédigés de façon approximative ci-dessus.

Codes

Il peut être amusant d'écrire soi même les codages, il l'est certainement beaucoup moins de lire ceux des autres. On trouve donc beaucoup de variété dans la littérature. Le choix du codage n'a pas grande importance, en soi. Éventuellement certains se "manieront" plus facilement dans la théorie. Comme les formules et les démonstrations peuvent être vues comme des suites finies de caractères, lettres, espace, ponctuation, et ceux-ci en nombre fini, on peut les coder par un nombre, celui étant écrit dans une base de taille le nombre de caractères nécessaire, ou par tout autre moyen qui permet de coder des suites finies d'entiers (Gödel utilise les exposants de la décompostion d'un nombre en facteurs premiers). On peut également utiliser un codage des couples (voir ci-dessous) pour représenter, suites finies, arbres, et donc les structures syntaxiques utiles ...

Formules Σ0

Un problème plus important est d'avoir des fonctions pour manipuler ces structures, l'équivalent des programmes en informatique : il est à peu près clair que l'on ne peut se contenter de compositions de fonctions constantes, d'additions et de multiplications, c’est-à-dire de polynômes à coefficients entiers positifs. On va représenter les fonctions utiles par des formules. Voyons un exemple, par ailleurs fort utile pour les codages. La bijection (Une fonction f: X → Y est dite bijective ou est une bijection si pour tout y dans l’ensemble d'arrivée Y il existe un et un seul x dans l’ensemble de définition X tel que f(x) = y. On dit encore dans...) de Cantor entre N×N et N est bien connue et tout à fait calculable : on énumére les couples d'entiers diagonale (On appelle diagonale d'un polygone tout segment reliant deux sommets non consécutifs (non reliés par un côté). Un polygone à n côtés possède diagonales.) par diagonale (somme constante), par exemple en faisant croître la seconde ( Seconde est le féminin de l'adjectif second, qui vient immédiatement après le premier ou qui s'ajoute à quelque chose de nature identique. La seconde est une unité de mesure du temps. La seconde d'arc est...) composante :

=[1+2+ … +(x+y)]+y=½(x+y)(x+y+1)+y

Cette fonction n'est déjà plus représentée par un terme du langage, à cause de la division (La division est une loi de composition qui à deux nombres associe le produit du premier par l'inverse du second. Si un nombre est non nul, la fonction "division par ce nombre" est la réciproque de la...) par 2, mais elle est représentée par la formule (on utilise "≡" pour la relation d'équivalence) :

z= ≡ 2z=(x+y)(x+y+1)+2y

Passons maintenant aux fonctions de décodage, c’est-à-dire à un couple de fonctions inverses. On aura besoin de quantificateurs :

x=π1(z) ≡ ∃y≤z 2z=(x+y)(x+y+1)+2y  ;         y=π2(z) ≡ ∃x≤z 2z=(x+y)(x+y+1)+2y

On a donc représenté une fonction, plus exactement son graphe (Le mot graphe possède plusieurs significations. Il est notamment employé :) (la formule soulignée) par une formule du langage de l'arithmétique. Les formules ci-dessus sont bien particulières : la première est une égalité polynômiale, si on remplace les trois variables libres par des termes clos du langage, représentant des entiers (s…s0), elle devient décidable. Les deux suivantes utilisent un quantificateur borné : "∃x≤z A" signifie "il existe un x plus petit ou égal à z tel que A". Là encore si on remplace les deux variables libres par des entiers cette formule devient décidable : pour vérifier une quantification existentielle bornée, il suffit de chercher jusqu’à la borne, soit on a trouvé, et l'énoncé est vérifié, soit on n'a pas trouvé et il ne l'est pas. Ce n'est plus le cas (pour la seconde partie de l'assertion) si la quantification existentielle n'est pas bornée. On pourra conserver cette propriété de décidabilité en ajoutant des quantifications universelles bornées, notée "∀ x≤ p A" ("pour tout x plus petit ou égal à p, A"). Les formules construites à partir des égalités polynômiales en utilisant les connecteurs booléens usuels, et des quantifications uniquement bornées sont appelées formules Σ0. Remarquez que la négation d'une formule Σ0 est Σ0.

On se convainc facilement, des arguments sont donnés juste ci-dessus et au paragraphe vérité et démontrabilité, que la vérité dans N des formules closes Σ0 est décidable : on a un moyen mécanique de savoir si elles sont vraies ou fausses. Pour démontrer le premier théorème d'incomplétude de Gödel (il faut un peu plus pour Gödel-Rosser, de la récurrence pour le second), la condition minimale sur la théorie, en plus d'être récursivement axiomatisable et d'une hypothèse de cohérence, est de démontrer toutes les formules Σ0 vraies dans N, et donc, par stabilité par négation des Σ0 et cohérence, de n'en démontrer aucune fausse. C'est ce que l'on a entendu par "formaliser suffisamment d'arithmétique". Remarquez que c'est une hypothèse sur les axiomes de la théorie. Par exemple l'ensemble des formules Σ0 vraies dans N étant décidable, on peut le choisir comme système d'axiomes pour une théorie qui sera bien récursivement axiomatisable (on peut évidemment le simplifier). En particulier on peut démontrer :

Dans l'arithmétique de Peano, les formules closes Σ0 sont vraies dans N si et seulement si elles sont démontrables.

Résultat qui se démontre d'ailleurs sans véritablement utiliser les axiomes de récurrence de l'arithmétique de Peano (ce qui est naturel puisqu'il n'y a pas véritablement de quantification universelle dans ces énoncés).

Formules Σ1

Il serait bien commode de se contenter de manipuler des fonctions représentables par des formules Σ0 : vérité et démontrabilité sont confondues, ces formules sont décidables, donc les fonctions représentées par des formules Σ0 sont calculables. Mais le "langage de programmation (Un langage de programmation est un langage informatique, permettant à un être humain d'écrire un code source qui sera analysé par une machine,...)" induit (L'induit est un organe généralement électromagnétique utilisé en électrotechnique chargé de recevoir l'induction de l'inducteur et de la transformer en...) n'est pas assez riche. On doit introduire les formules Σ1, qui sont les formules obtenues en plaçant un quantificateur existentiel en tête d'une formule Σ0. En général la négation d'une formule Σ1 n'est pas équivalente à une formule Σ1. On a la propriété suivante :

Dans une théorie qui prouve toutes les formules Σ0 vraies dans N, les formules Σ1 vraies dans N sont prouvables.

En effet une formule Σ1 "∃ x A x" est vraie dans N signifie que pour un certain entier, que l'on peut écrire "s…s0", la formule "A s…s0" est vraie, or cette formule est Σ0.

Il existe des théories arithmétiques cohérentes, qui démontrent des formules closes Σ1 fausses, contrairement à ce qui se passe pour les Σ0. Il faut préciser que de telles théories arithmétiques sont assez pathologiques, comme celles qui démontrent un énoncé exprimant leur propre contradiction (voir début de l'article). L'hypothèse de cohérence supplémentaire utile pour le premier théorème d'incomplétude, que l'on va appeler Σ-cohérence, c'est justement de supposer que la théorie ne démontre aucune formule close Σ1 fausse. On suppose que certaines formules ne sont pas démontrables, donc la contradiction ne l'est pas : c'est bien une hypothèse de cohérence au moins aussi forte que la cohérence simple. Elle est vraiment plus forte : on peut exprimer la négation de la cohérence d'une théorie par une formule Σ1[7].

Fonctions définissables, fonctions représentables

Un sous-ensemble (En mathématiques, un ensemble A est un sous-ensemble ou une partie d’un ensemble B, ou encore B est sur-ensemble de A, si tout élément du...) E de N, ou plus généralement de Np est définissable dans l'arithmétique s'il existe une formule F de l'arithmétique avec p variables libres telle que :

(n1,…, np) ∈ E si et seulement si F(n1,…, np) est vraie dans N

Un sous-ensemble E de Np est représentable dans une théorie T s'il existe une formule s'il existe une formule F de l'arithmétique avec p variables libres telle que :

(n1,…, np) ∈ E si et seulement si F(n1,…, np) est démontrable dans T.

Une fonction f à plusieurs variables sur N est définissable dans N si son graphe est défini dans N, représentable dans une théorie T' si son graphe est représentable dans T. Un ensemble, ou une fonction est définissable par une formule Σ1 si et seulement si il, ou elle, est représentable par cette formule dans une théorie Σ-cohérente où tous les énoncés Σ0 sont démontrables.

Il existe d'autres notions de représentabilité plus fortes, pour les ensembles comme pour les fonctions. Pour celle introduite ici on dit souvent faiblement représentable.

On notera y=f(x) une formule Σ1 définissant ou représentant f. Pour le théorème de Gödel c'est la notion de fonction ou d'ensemble représentable qui est utile, mais la notion de fonction ou d'ensemble définissable est plus simple à manipuler, et comme on s'intéresse aux cas où elles sont équivalentes, on va dans la suite parler de définissabilité par une formule Σ1.

On peut remarquer que la conjonction, la disjonction de deux formules Σ1, la quantification existentielle d'une formule Σ1, la quantification universelle bornée d'une formule Σ1, sont équivalentes dans N (on note ≡N) à une formule Σ1 :

∃x A ∨ ∃x B ≡ ∃x (A ∨ B)  ;   ∃x ∃y A(x, y) ≡N ∃z ∃x≤z ∃y≤z A(x, y)  ;   ∃x A ∧ ∃y B ≡ ∃x ∃y (A ∧ B) ;  ∀x≤z ∃y A(x, y) ≡N∃ u ∀x≤z ∃y≤u A(x, y).

L'ensemble de fonctions à notre disposition est donc stable par composition (on donne l'exemple pour une variable, on généralise sans peine à des fonctions de plusieurs variables) :

z=f o g (x) ≡ ∃ y [z=f(y)y = g (x)]

On définit également de façon naturelle :

f(x)=g(y) ≡ ∃ z [z=f(x)z = g (y)]

Cependant, pour pouvoir avoir un langage suffisamment expressif pour définir les fonctions utiles sur la syntaxe, il manque une notion très utile : la définition par récurrence. L'idée pour l'obtenir est d'utiliser un codage des suites finies (les listes de l'informatique). Supposons que nous ayons un tel codage, notons l=[n0;…;np] l'entier qui code la suite finie n0,…, np. Il faut pouvoir décoder : notons β(l, i)=ni l'élément en place i de la suite codée par l (la valeur n'a pas d'importance si i est trop grand). Supposons que nous ayons une fonction g de N dans N (une suite infinie d'entiers) définie par :

g(0)=a ;  g(n+1)=f(g(n))

et que f soit définissable dans N. Alors on pourra définir la fonction g par :

y=g(x) ≡ ∃ l [β(l,0)=a ∧ ∀ i < x β(l, i+1)=f(β(l, i))y = β(l, x)]

formule qui est équivalente dans N à une formule Σ1 dès que le graphe de β est Σ1. Ceci se généralise au schéma de récurrence utilisé pour les fonctions récursives primitives. Il suffit donc trouver une formule Σ1 qui définit une fonction β : c'est la principale difficulté à résoudre pour le codage de la syntaxe.

La fonction β

Le nom de fonction β est repris de l'article original de Gödel. Pour la définir, il a eu l'idée d'utiliser le théorème des restes chinois : pour coder n1,…, np on va donner p entiers premiers entre eux deux à deux, engendrés à partir d'un seul entier d, et un entier a dont les restes des divisions par chacun de ces entiers sont n1,…, np. La suite n1,…, np sera donc codée par les deux entiers a et d, l'entier si on en veut un seul. Plusieurs (une infinité !) entiers coderont la même suite, ce qui n'est pas gênant si on pense à l'objectif (coder les définitions par récurrence). Le principal est que l'on assure que toute suite finie a au moins un code.

Étant donnés les entiers n1,…, np, on choisi un entier s, tel que s ≥ p et pour tout ni, s≥ni. Les entiers

d0=1+s!, d1=1+2s!, …, dn=1+(n+1)s!

sont alors premiers entre eux deux à deux. De plus ni < di. Par le théorème chinois on déduit l'existence d'un entier a tel que pour chaque entier ni de la suite finie, le reste de la division de a par di soit ni. On a donc, en posant d = s! :

β(d, a,i)=r(a,1+(i+1)d) ;  z=r(a, b) ≡ z

On a bien une fonction β définie par une formule Σ0.

On en déduit que :

si une fonction se définit par récurrence primitive à partir de fonctions définissables par des formules Σ1, elle est définissable par une formule Σ1.

On peut faire beaucoup de choses avec les fonctions récursives primitives. Une fois ce résultat obtenu, le reste n'est plus qu'affaire de soin. On peut utiliser des méthodes plus ou moins astucieuses pour gérer les problèmes de liaison de variables. On montre que la fonction qui code la substitution d'un terme à une variable dans une formule est récursive primitive, que l'ensemble des (codes de) preuves d'une théorie T récursivement axiomatisable est récursif primitif, et enfin que la fonction qui extrait d'une preuve la conclusion de celle-ci est récursive primitive. Dire qu'une formule est prouvable dans T, c'est dire qu'il existe une preuve de cette formule dans T, ce qui, codé dans la théorie, reste Σ1, bien que le prédicat (Les prédicats d’une théorie sont les formules qui contiennent des variables libres.) "être démontrable" ne soit pas lui récursif primitif, ni même récursif[8].

En conclusion, pour une théorie récursivement axiomatisable T, on a deux formules Σ1, DemT(x) et z=sub(x, y), telles que :

  • DemT(⌈F⌉) est vraie dans N si et seulement si F est prouvable dans T ;
  • pour toute formule F(x), ⌈F(n)⌉ = sub(⌈F⌉, n), et la fonction sub est définie par la formule z=sub(x, y).

On a noté ⌈F⌉ l'entier qui code la formule F.

Du fait que les formules sont Σ1, on peut remplacer "vrai" par "démontrable dans T" sous les hypothèses suffisantes.

Diagonalisation

La construction de l'énoncé de Gödel repose sur un argument diagonal. On construit tout d'abord la formule à une variable libre Δ(x) :

Δ(x) ≡ ∀z[z=sub(x, x) ⇒ DemT(z)]

qui peut s'interpréter dans N par la formule de code x appliquée à son propre code n'est pas démontrable dans T, et on applique cette formule à l'entier ⌈Δ⌉. On obtient G=Δ(⌈Δ⌉), une formule qui dit bien d'elle même qu'elle n'est pas démontrable dans T. On reprend en la précisant l'argumentation déjà donnée au dessus. On suppose que T est récursivement axiomatisable, démontre toutes les formules Σ0 vraies dans N, donc toutes les formules Σ1 vraies dans N, et qu'elle est Σ-cohérente.

  • G=Δ(⌈Δ⌉) est une formule close, équivalente à la négation d'une formule Σ1 ;
  • si la formule G était démontrable, la négation de G étant Σ1 ne pourrait être vraie car alors elle serait démontrable, et donc cela contredirait la cohérence de T. La formule G serait donc vraie dans N, ce qui voudrait dire, par construction de G, que la formule G ne serait pas démontrable, contradiction. Donc G n'est pas démontrable.
  • si la négation de la formule G était démontrable dans T, par Σ-cohérence elle serait vraie, or elle est fausse d'après ce qui précède. Donc la négation de G n'est pas démontrable.

On voit donc bien, le dernier argument étant assez tautologique, que le véritable contenu du théorème est dans la non-démontrabilité de G. Le premier théorème d'incomplétude de Gödel s'énonce donc aussi bien par :

Si T est une théorie récursivement axiomatisable, cohérente, et qui démontre toutes les formules Σ0 vraies dans N, alors il existe une formule G, négation d'une formule Σ1, qui est vraie dans N, mais non démontrable dans T.

Remarquez que la formule G en question est équivalente à une formule universelle ∀x H(x), où H est Σ0. Cette formule étant vraie, pour chaque entier n (représenté par s...s 0) H(n) est vraie, donc démontrable étant Σ0. On a donc bien, comme annoncé dans le paragraphe " vérité et démontrabilité ", un énoncé universel ∀x H(x) qui n'est pas démontrable dans T, alors que pour chaque entier n, H(n) est démontrable dans T.

Argument de la preuve du second théorème d'incomplétude

Le second théorème d'incomplétude se prouve essentiellement en formalisant la preuve du premier théorème d'incomplétude pour une théorie T dans cette même théorie T. En effet, on a montré ci-dessus que, si la théorie était cohérente la formule G de Gödel (qui dépend de T), n'est pas prouvable. Mais la formule de Gödel est équivalente à sa non prouvabilité. On a donc montré que la cohérence de la théorie T entraîne G : si T est suffisante pour formaliser cette preuve, on a alors montré dans la théorie T que la cohérence de la théorie T entraîne G, formule qui n'est pas prouvable dans T, donc n'est pas prouvable dans T.

On utilise simplement la non-démontrabilité de G, donc l'hypothèse de cohérence simple suffit. Par contre la théorie T doit forcément être plus expressive que pour le premier théorème d'incomplétude. En particulier on a besoin de récurrence.

Les conditions que doivent vérifier la théorie T pour démontrer le second théorème d'incomplétude ont été précisées tout d'abord par Paul Bernays dans les Grundlagen der Mathematik (1939) co-écrit avec David Hilbert, puis par Martin Löb, pour la démonstration de son théorème, une variante du second théorème d'incomplétude. Les conditions de démontrabilité de Löb portent sur le prédicat de prouvabilité dans la théorie T, que l'on nomme comme ci-dessus DemT :

  • D1. Si F est démontrable dans T, alors DemT(⌈F⌉) est démontrable dans T.
  • D2. DemT(⌈F⌉) ⇒ DemT(DemT(⌈F⌉)) est démontrable dans T.
  • D3. DemT(⌈F ⇒ G⌉) ⇒ (DemT(⌈F⌉) ⇒ DemT(⌈G⌉)) est démontrable dans T.

La condition D1 est apparue implicitement pour démontrer le premier théorème d'incomplétude. La seconde condition D2 est une formalisation dans la théorie de D1. Enfin la dernière, D3, est une formalisation de la règle logique primitive dite de Modus Ponens. Notons cohT la formule qui exprime la cohérence de T, c’est-à-dire que l'absurde, que l'on note ⊥, n'est pas démontrable (la négation est notée maintenant ¬) :

cohT ≡ ¬DemT(⌈⊥⌉)

Comme la négation d'une formule F, ¬F, équivaut à F entraîne l'absurde, F⇒⊥, on déduit de la condition D3 que

  • D'3 DemT(⌈¬F⌉) ⇒ (DemT(⌈F⌉) ⇒ ¬cohT.

Pour déduire le second théorème d'incomplétude des trois conditions de Löb, il suffit de reprendre le raisonnement déjà fait ci-dessus. Soit G la formule de Gödel, qui, sous hypothèse de cohérence simple, entraîne ¬DemT(⌈G⌉). D'après D1 et la cohérence de la théorie T, G n'est pas démontrable dans T (premier théorème). On formalise maintenant ce raisonnement dans T. Supposons que dans T, DemT(⌈G⌉). Comme d'autre part on démontre dans T que DemT(⌈G ⇒ ¬DemT(⌈G⌉)⌉), on déduit par D3 dans T, DemT(⌈¬DemT(⌈G⌉)⌉). Finalement par D'3 on a montré ¬cohT dans T. Récapitulons : on a montré dans T que DemT(⌈G⌉) ⇒ ¬cohT, c’est-à-dire par définition de G, ¬G ⇒ ¬cohT, et par contraposée cohTG. Or on a vu que G n'est pas démontrable dans T, donc cohT n'est pas démontrable dans T.

La preuve de D1 a été déjà été esquissée à propos du premier théorème d'incomplétude : il s'agit de formaliser proprement la démontrabilité, et on utilise que les formules closes Σ1 vraies sont démontrables.

La condition D3 formalise la règle de modus ponens, une règle que l'on a tout intérêt à avoir dans les systèmes formels pour les démonstrations que l'on a choisi. Il faudrait rentrer dans le détail du codage pour donner la preuve de D3, mais elle ne sera pas bien difficile. Il faut faire attention à bien formaliser le résultat indiqué dans la théorie choisie : les variables en jeu (par exemple il existe un x qui est le code d'une preuve de F) sont les variables de la théorie. Il faudra quelques résultats sur l'ordre, savoir démontrer quelques résultats élémentaires sur les preuves dans la théorie.

C'est la condition D2 qui s'avère la plus délicate a démontrer. C'est un cas particulier de la propriété

  • Pour toute formule close F Σ1, FDemT(⌈F⌉) est démontrable dans T

qui formalise (dans T) que toute formule close Σ1 vraie est démontrable dans T. On n'a donné ci-dessus aucun détail sur la preuve de ce dernier résultat, T étant par exemple l'arithmétique de Peano. Si on en donnait, on se rendrait compte que l'on n'a pas besoin de l'axiome de récurrence de la théorie, mais que, par contre, l'on raisonne par récurrence sur la longueur (La longueur d’un objet est la distance entre ses deux extrémités les plus éloignées. Lorsque l’objet est filiforme ou en forme de lacet, sa longueur est celle de l’objet complètement...) des termes, la complexité des formules ... Comme il faut maintenant formaliser cette preuve dans la théorie, il faut de la récurrence. Pour résumer la situation : quand on a démontré sérieusement le premier théorème d'incomplétude pour l'arithmétique de Peano, on a fait cette preuve, qui est un peu longue, mais ne présente pas de difficulté. Pour le second théorème, la seule chose à faire consiste maintenant à montrer que cette preuve se formalise dans l'arithmétique de Peano elle-même, ce qui est intuitivement relativement clair (quand on a fait la preuve), mais très pénible à expliciter complètement (Le complètement ou complètement automatique, ou encore par anglicisme complétion ou autocomplétion, est une fonctionnalité informatique permettant...).

On peut en fait démontrer le second théorème d'incomplétude pour une théorie plus faible que l'arithmétique de Peano, l'arithmétique primitive récursive. On étend le langage de façon à avoir des symboles de fonction pour toutes les fonctions primitives récursives, et on ajoute à la théorie les axiomes qui définissent ces fonctions. On restreint la récurrence aux formules sans quantificateurs, ce qui fait que celles-ci sont "immédiates". L'arithmétique primitive récursive est souvent considérée comme la formalisation des mathématiques finitaires, avec lesquelles Hilbert espérait pouvoir prouver la cohérence des théories mathématiques.

Notes

  1. Gödel n'en donnait qu'une esquisse (Une esquisse est un dessin tracé rapidement soit comme ébauche pour une œuvre plus élaborée, soit pour prendre des notes dans des...), très satisfaisante cependant, dans l'article original, et ne publia jamais la démonstration détaillée qu'il avait pourtant annoncée.
  2. La prouvabilité intuitionniste étant plus faible que la prouvabilité classique, l'énoncé que Gödel fournit pour le premier théorème d'incomplétude, indécidable en logique classique, le reste en logique intuitionniste. Par ailleurs, la preuve de Gödel est constructive : l'énoncé indécidable peut être donné explicitement pour une théorie donnée. Elle peut se formaliser en logique intuitionniste, même si le présent article ne s'en soucie pas.
  3. parfois, dans les ouvrages sur le théorème de Gödel, on parle simplement d'énoncé vrai, pour vrai dans le modèle standard de l'arithmétique
  4. encore que les choses puissent être bien compliquées, dès que les formules ont une certaine complexité logique, et que les récurrences sont imbriquées
  5. du point (Graphie) de vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) de la vérité, on a bien que ∀ x H(x) est vraie dans N, le modèle standard, Mais il existe un modèle non standard de l'arithmétique de Peano, dans lequel il y a au delà des entiers usuels dits standards, des entiers dits non standards, dont l'un au moins ne satisfait pas la propriété H
  6. D'après le théorème de Tarski, la vérité dans N pour les énoncés d'une théorie arithmétique ne peut se formaliser dans le langage de cette théorie.
  7. En fait Gödel fait une hypothèse plus forte, la ω-cohérence : une théorie arithmétique ω-cohérente ne peut démontrer A0, A1, A2, ... (A n pour chaque entier n) et "¬∀x Ax". On en déduit, dans le cas où "Ax" est Σ0, et "∃ x A x" est démontrable (donc "¬∀x¬Ax"), que l'on ne peut démontrer "¬A n" pour tous les entiers n. Or les "A n" sont closes Σ0, donc démontrables si et seulement si elles sont vraies dans N. Pour un certain entier n0, "¬ A n0" n'est pas démontrable, donc "A n0" est vraie dans N, donc "∃ x A x" est vraie dans N. On a déduit la Σ-cohérence de la ω-cohérence.
  8. En fait, les ensembles définissables par des formules Σ1, et donc les ensembles représentables (au sens faible où on l'a définit) dans une théorie arithmétique Σ-cohérente, sont exactement les ensembles récursivement énumérables. Tous les arguments pour ce résultat sont d'ailleurs dans l'article de Gödel (il ne peut y être énoncé, puisque la notion n'est pas encore connue), et sont ceux résumés dans le présent paragraphe. En effet on montre en théorie de la calculabilité que les projetés des ensembles primitifs récursifs sont les récursivement énumérables. Ce résultat fournit d'ailleurs une autre preuve du théorème de Gödel. Il suffit par exemple de reprendre l'argument donné dans le paragraphe " indécidabilité algorithmique ", en utilisant l'indécidabilité du problème de l'arrêt au lieu du théorème de Matiiassevitch.

Sources

en Français :

  • Raymond Smullyan (Raymond Smullyan est un logicien, mathématicien et magicien américain né en 1919.), Les théorèmes d'incomplétude de Gödel - Dunod, 2000 - ISBN 210005287X

Plusieurs preuves du premier théorème d'incomplétude, y compris la variante de Gödel-Rosser, et dont les premières sont simplifiées en renforçant les hypothèses. Un exposé rapide sur le second.

  • René Cori, Daniel Lascar, Logique mathématique (tome II) - Masson - 1994 - ISBN 2-225-84080-6

Preuve du théorème de Gödel-Rosser par l'indécidabilité de la théorie.

  • Jean-Louis Krivine, Théorie des ensembles, ch. 9, Cassini (La mission Cassini-Huygens est une mission spatiale automatique réalisée en collaboration par le Jet Propulsion Laboratory (JPL), l'Agence spatiale européenne (ESA) et l'Agence spatiale italienne (ASI). Son objectif est l'étude de la planète...) 1998, ISBN 2-84225-014-1

Une preuve du second théorème d'incomplétude en théorie des ensembles utilisant la conséquence sémantique.

en Anglais :

  • Craig Smorynski, Logical Number Theory I -- An Introduction, Springer Verlag, 1991 - ISBN 3-540-52236-0 - ISBN 0-387-52236-0.

Théorèmes d'indécidabilité et d'incomplétude (premier), théorème de Matiiassevitch ...

  • Craig Smorynski, The Incompletness Theorems, in Handbook of Mathematical Logic édité par J. Barwise, North Holland, 1977 - ISBN 0-7204-2285-X

Les deux théorèmes d'incomplétude, contexte, preuves relativement détaillées, prolongements.

  • Jean-Yves Girard (Né à Lyon en 1947, ancien élève de l'École normale d'Instituteurs de Lyon (1962), ancien élève de l'École normale supérieure de Saint-Cloud (1966), Jean-Yves Girard est un logicien et mathématicien contemporain, directeur de...), Proof Theory and Logical Complexity, volume (Le volume, en sciences physiques ou mathématiques, est une grandeur qui mesure l'extension d'un objet ou d'une partie de l'espace.) 1. Bibliopolis, 1987.

En particulier des détails sur la preuve du second théorème d'incomplétude

Articles originaux :

  • K. Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. (" Sur quelques théorèmes formels indécidables des Principia Mathematica et des systèmes qui leur sont reliés ") Monatshefte für Mathematik und Physik, 38 (received 17 Nov 1930, published 1931), pp. 173-198. Traduit en anglais par van Heijenoort in From Frege to Gödel. Harvard University Press, 1971. pp. 596-616.
  • K. Gödel: Some basic theorems on the foundations of mathematics and their implications (1951). Printed in Collected works / Kurt Gödel v.III; edited by Solomon Feferman. Clarendon Press ; New York : Oxford University Press, 1995. pp. 304-323.
  • K. Gödel: On formally undecidable propositions of Principia Mathematica and related systems I (PDF) Translated by Martin Hirzel, Boulder, November 27, 2000.
  • J. B. Rosser: Extensions of some theorems of Gödel and Church. Journal of Symbolic Logic, 1 (1936), N1, pp. 87-91.
  • Martin Davis, (éd) 2004 (1965). The undecidable. Dover Publications. Recueil des principaux articles de Gödel, Church, Turing, Rosser, Kleene, et Post.
  • Jeff Paris, Leo Harrington, A mathematical Incompleteness in Peano Arithmetic, 1977, in Handbook of Mathematical Logic (cité ci-dessus).

Autres:

  • Jean-Paul Delahaye (Jean-Paul Delahaye est un informaticien et mathématicien français.), L'intelligence et le calcul - Belin pour la science (La science (latin scientia, « connaissance ») est, d'après le dictionnaire Le Robert, « Ce que l'on sait pour l'avoir appris,...), 2002 - ISBN 284245040X
  • Douglas Hofstadter, Gödel, Escher, Bach, les brins d'une guirlande éternelle - Dunod, 2000 - ISBN 210005435X
  • Raymond Smullyan, Quel est le titre de ce livre ? - Dunod, 1993 - ISBN 210002003X, Ca y est, je suis fou - Dunod, 1993 - ISBN 2100019635, Les énigmes de Sheherazade - Flammarion, 1998 - ISBN 2080355643.

casse-têtes logico-mathématiques, dont certains sont inspirés par le théorème de Gödel

  • William Poundstone, Les labyrinthes de la raison - Belfond, 1998 - ISBN 2714425666
Page générée en 0.480 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