La preuve de cohérence de Gentzen - Gentzen's consistency proof

La preuve de cohérence de Gentzen est le résultat de la théorie de la preuve en logique mathématique , publiée par Gerhard Gentzen en 1936. Elle montre que les axiomes de Peano de l' arithmétique du premier ordre ne contiennent pas de contradiction (c'est-à-dire sont « cohérents »), tant qu'un certain autre Le système utilisé dans la preuve ne contient pas non plus de contradictions. Cet autre système, appelé aujourd'hui « arithmétique récursive primitive avec le principe additionnel de l'induction transfinie sans quantificateur jusqu'à l' ordinal ε 0 », n'est ni plus faible ni plus fort que le système des axiomes de Peano. Gentzen a fait valoir qu'il évite les modes d'inférence discutables contenus dans l'arithmétique Peano et que sa cohérence est donc moins controversée.

Théorème de Gentzen

Le théorème de Gentzen s'intéresse à l'arithmétique du premier ordre: la théorie des nombres naturels , y compris leur addition et leur multiplication, axiomatisée par les axiomes de Peano du premier ordre . C'est une théorie du "premier ordre": les quantificateurs s'étendent sur des nombres naturels, mais pas sur des ensembles ou des fonctions d'entiers naturels. La théorie est suffisamment forte pour décrire des fonctions entières définies récursivement telles que l'exponentiation, les factorielles ou la séquence de Fibonacci .

Gentzen a montré que la cohérence des axiomes de Peano du premier ordre est prouvable sur la théorie de base de l'arithmétique récursive primitive avec le principe supplémentaire de l'induction transfinie sans quantificateur jusqu'à l' ordinal ε 0 . L'arithmétique récursive primitive est une forme d'arithmétique très simplifiée qui ne prête pas à controverse. Le principe supplémentaire signifie, de manière informelle, qu'il y a un bon ordre sur l'ensemble des arbres à racines finies . Formellement, ε 0 est le premier ordinal tel que et est un ordinal dénombrable beaucoup plus petit que les grands ordinaux dénombrables . C'est la limite de la séquence:

Pour exprimer des ordinaux dans le langage de l'arithmétique, une notation ordinale est nécessaire, c'est-à-dire un moyen d'assigner des nombres naturels aux ordinaux inférieurs à ε 0 . Cela peut être fait de différentes manières, un exemple fourni par le théorème de forme normale de Cantor . Nous demandons pour toute formule sans quantificateur A (x): s'il existe un ordinal a <ε 0 pour lequel A (a) est faux, alors il existe un ordinal au moins.

Gentzen définit une notion de "procédure de réduction" pour les preuves en arithmétique Peano. Pour une preuve donnée, une telle procédure produit un arbre de preuves, celle donnée servant de racine de l'arbre, et les autres preuves étant, en un sens, "plus simples" que celle donnée. Cette simplicité croissante est formalisée en attachant un ordinal <ε 0 à chaque preuve, et en montrant qu'au fur et à mesure que l'on descend dans l'arbre, ces ordinaux deviennent plus petits à chaque pas. Il montre alors que s'il y avait preuve d'une contradiction, la procédure de réduction aboutirait à une suite infinie descendante d'ordinaux inférieurs à ε 0 produite par une opération récursive primitive sur des preuves correspondant à une formule sans quantificateur.

Il est possible d'interpréter la preuve de Gentzen en termes de théorie des jeux ( Tait 2005 ).

Relation avec le programme de Hilbert et le théorème de Gödel

La preuve de Gentzen met en évidence un aspect souvent oublié du deuxième théorème d'incomplétude de Gödel . On prétend parfois que la cohérence d'une théorie ne peut être prouvée que dans une théorie plus solide. La théorie de Gentzen obtenue en ajoutant une induction transfinie sans quantificateur à l'arithmétique récursive primitive prouve la cohérence de l'arithmétique Peano du premier ordre (PA) mais ne contient pas de PA. Par exemple, il ne prouve pas l'induction mathématique ordinaire pour toutes les formules, contrairement à PA (puisque toutes les instances d'induction sont des axiomes de PA). Cependant, la théorie de Gentzen n'est pas non plus contenue dans PA, car elle peut prouver un fait théorique des nombres - la cohérence de PA - que PA ne peut pas. Par conséquent, les deux théories sont, en un sens, incomparables .

Cela dit, il existe d'autres moyens plus puissants de comparer la force des théories, dont la plus importante est définie en termes de notion d' interprétabilité . On peut montrer que, si une théorie T est interprétable dans un autre B, alors T est cohérente si B l'est. (En effet, c'est un gros point de la notion d'interprétabilité.) Et, en supposant que T n'est pas extrêmement faible, T lui-même pourra prouver ce conditionnel: si B est cohérent, alors T. prouver que B est cohérent, par le deuxième théorème d'incomplétude, alors que B pourrait bien être capable de prouver que T est cohérent. C'est ce qui motive l'idée d'utiliser l'interprétabilité pour comparer les théories, c'est-à-dire la pensée que, si B interprète T, alors B est au moins aussi fort (au sens de «force de cohérence») que T l'est.

Une forme forte du deuxième théorème d'incomplétude, prouvé par Pavel Pudlák, qui s'appuyait sur des travaux antérieurs de Solomon Feferman , déclare qu'aucune théorie cohérente T qui contient l' arithmétique de Robinson , Q, ne peut interpréter Q plus Con (T), l'affirmation que T est consistent. En revanche, Q + Con (T) n'interpréter T, par une forme solide du arithmetized théorème de complétude . Donc Q + Con (T) est toujours plus fort (dans un bon sens) que T ne l'est. Mais la théorie de Gentzen interprète trivialement Q + Con (PA), car elle contient Q et prouve Con (PA), et donc la théorie de Gentzen interprète PA. Mais, d'après le résultat de Pudlák, PA ne peut pas interpréter la théorie de Gentzen, puisque la théorie de Gentzen (comme je viens de le dire) interprète Q + Con (PA), et l'interprétabilité est transitive. Autrement dit: si PA interprétait la théorie de Gentzen, alors il interpréterait également Q + Con (PA) et serait donc incohérent, d'après le résultat de Pudlák. Ainsi, dans le sens de la force de cohérence, caractérisée par l'interprétabilité, la théorie de Gentzen est plus forte que l'arithmétique de Peano.

Hermann Weyl a fait le commentaire suivant en 1946 concernant la signification du résultat de cohérence de Gentzen suite à l'impact dévastateur du résultat d'incomplétude de Gödel en 1931 sur le plan de Hilbert pour prouver la cohérence des mathématiques.

Il est probable que tous les mathématiciens auraient finalement accepté l'approche de Hilbert s'il avait pu la mener à bien. Les premiers pas étaient inspirants et prometteurs. Mais ensuite Gödel lui a porté un coup terrible (1931), dont il ne s'est pas encore remis. Gödel a énuméré les symboles, formules et séquences de formules dans le formalisme de Hilbert d'une certaine manière, et a ainsi transformé l'assertion de cohérence en proposition arithmétique. Il pourrait montrer que cette proposition ne peut être ni prouvée ni réfutée dans le cadre du formalisme. Cela ne peut signifier que deux choses: soit le raisonnement par lequel une preuve de cohérence est donnée doit contenir un argument qui n'a pas de contrepartie formelle au sein du système, c'est-à-dire que nous n'avons pas réussi à formaliser complètement la procédure d'induction mathématique; ou l'espoir d'une preuve de cohérence strictement «finitiste» doit être abandonné. Lorsque G. Gentzen a finalement réussi à prouver la cohérence de l'arithmétique, il a franchi ces limites en affirmant comme évidente un type de raisonnement qui pénètre dans la «deuxième classe de nombres ordinaux» de Cantor.

Kleene (2009 , p. 479) a fait le commentaire suivant en 1952 sur la signification du résultat de Gentzen, en particulier dans le contexte du programme formaliste initié par Hilbert.

Les propositions originales des formalistes de sécuriser les mathématiques classiques par une preuve de cohérence ne prévoyaient pas qu'une méthode telle que l'induction transfinie jusqu'à ε 0 devrait être utilisée. Dans quelle mesure la preuve de Gentzen peut être acceptée comme garantissant la théorie classique des nombres dans le sens de cette formulation du problème est dans l'état actuel des choses une question de jugement individuel, en fonction de la mesure dans laquelle on est prêt à accepter l'induction jusqu'à ε 0 en tant que finitaire. méthode.

Autres preuves de cohérence de l'arithmétique

La première version de Gentzen de sa preuve de cohérence n'a pas été publiée de son vivant parce que Paul Bernays s'était opposé à une méthode implicitement utilisée dans la preuve. La preuve modifiée, décrite ci-dessus, a été publiée en 1936 dans les Annales . Gentzen a continué à publier deux autres preuves de cohérence, une en 1938 et une en 1943. Toutes ces preuves sont contenues dans ( Gentzen & Szabo 1969 ).

En 1940, Wilhelm Ackermann a publié une autre preuve de cohérence pour l'arithmétique Peano, en utilisant également l'ordinal ε 0 .

Travail initié par la preuve de Gentzen

La preuve de Gentzen est le premier exemple de ce que l'on appelle l' analyse ordinale théorique de la preuve . Dans l'analyse ordinale, on évalue la force des théories en mesurant la taille des ordinaux (constructifs) dont on peut prouver qu'ils sont bien ordonnés, ou de manière équivalente la taille d'un ordinal (constructif) qui peut être prouvée par induction transfinie. Un ordinal constructif est le type d'ordre d'un bon ordre récursif des nombres naturels.

Laurence Kirby et Jeff Paris ont prouvé en 1982 que le théorème de Goodstein ne peut pas être prouvé en arithmétique Peano. Leur preuve était basée sur le théorème de Gentzen.

Remarques

Les références