Théorème d'accélération de Gödel

Kurt Gödel, en adaptant sa démonstration du premier théorème d'incomplétude, a construit des exemples explicites d'assertions relativement courtes, démontrables dans un système formel donné, mais dont la plus courte démonstration dans ce système est absurdement longue. Ainsi, l'affirmation :

« Cette affirmation ne peut pas être prouvée à l'aide des axiomes de Peano (seuls) en moins d'un gogolplex de symboles »

(ou plus précisément, comme exposé dans la prochaine section, l'affirmation G qui code, au moyen d'un code de Gödel convenable, que G n'est pas démontrable en moins d'un gogoplex de symboles) est effectivement vraie, et même démontrable dans PA (l'arithmétique de Peano) ; de plus, si PA est non contradictoire, la démonstration possède nécessairement plus d'un gogolplex de symboles.

En revanche, il suffit d'adjoindre aux axiomes de Peano l'affirmation que ceux-ci sont non contradictoires (plus techniquement, l'axiome coh_PA, lequel, d'après le second théorème d'incomplétude, ne peut pas être démontré dans PA), pour pouvoir démontrer G en peu de symboles.

Cet argument se généralise à n'importe quel système cohérent plus puissant que PA, par exemple ZFC ; le gogolplex peut être remplacé par n'importe quel nombre que le système permet de décrire en (relativement) peu de symboles, par exemple le nombre de Graham.

Le cadre de ce résultat est le même que celui des théorèmes d'incomplétude (on emploie dans ce qui suit les notations de cet article) : on se place dans une théorie T récursivement axiomatisable, permettant de formaliser l'arithmétique (essentiellement une théorie pour laquelle les axiomes de Peano sont des théorèmes) et supposée cohérente. Il existe alors deux constantes c et d (ne dépendant que de T) telles que pour tout entier N exprimable dans le langage de T en k symboles, il existe une proposition G(N) ayant les propriétés suivantes :

1. G(N) est un théorème de T.
2. La plus courte démonstration de G(N) dans T comporte au moins N symboles.
3. G(N) possède une démonstration dans T + coh_T comportant moins de c+dk symboles.

En pratique, c et d sont assez petits. Par exemple, si T est l'arithmétique de Peano et N un gogolplex, il serait possible d'écrire explicitement (à l'aide d'ordinateurs, tout de même) une proposition équivalente à G(N) en quelques dizaines de milliers de symboles[1].

La construction de G(N) utilise un codage de Gödel associant à toute proposition P un entier noté ⌈P⌉, et suit celle de la proposition indécidable donnée par le premier théorème d'incomplétude. On construit des fonctions arithmétiques codant des propriétés de P par l'intermédiaire de calculs sur ⌈P⌉ (par exemple, une fonction Dem(⌈P⌉) qui détermine si P possède ou non une démonstration dans T. On code alors l'affirmation A(P) : « P n'a pas de démonstration de moins de N symboles » par une formule F(x) telle que F(⌈P⌉)=⌈A(P)⌉. Puis, par une diagonalisation analogue à celle du premier théorème d'incomplétude, on construit G(N) telle que F(⌈G(N)⌉)=⌈G(N)⌉. Le décodage montre alors que G(N) a les propriétés 1) et 2) ; et cette dernière démonstration, utilisant le décodage, peut être faite entièrement dans T (en peu de symboles), si on adjoint à T l'hypothèse que T est non contradictoire, c'est-à-dire coh_T.

Ce théorème de Gödel semble être passé relativement inaperçu ; Jean-Paul Delahaye signale[2] la démonstration, en 1971, d'un résultat plus puissant, montrant que ce phénomène se produit dans toute théorie où l'on peut rajouter une proposition indécidable[3].

Harvey Friedman a obtenu des exemples explicites plus naturels du même phénomène, utilisant des résultats de théorie des graphes tels que le théorème de Kruskal ou le théorème de Robertson-Seymour. Il construit des énoncés affirmant l'existence de suites de N graphes ayant certaines propriétés, dont la preuve dans PA, ou d'ailleurs dans des théories beaucoup plus fortes, demande essentiellement d'exhiber une telle suite, alors que la démonstration est courte si l'on admet l'existence de certains grands ordinaux dénombrables[4]. Des résultats analogues découlent également du théorème de Goodstein[5].

• (en) Samuel R. Buss, « On Gödel's theorems on lengths of proofs. I. Number of lines and speedup for arithmetics », The Journal of Symbolic Logic, vol. 59, n^o 3,‎ 1994, p. 737–756 (ISSN 0022-4812, DOI 10.2307/2275906, lire en ligne)
• (en) Samuel R. Buss, « On Gödel's theorems on lengths of proofs. II. Lower bounds for recognizing k symbol provability », dans Peter Clote, Jeffrey Remmel, Feasible mathematics, II (Ithaca, NY, 1992), vol. 13, Boston, MA, Birkhäuser Boston, coll. « Progr. Comput. Sci. Appl. Logic », 1995, 57–90 p. (ISBN 978-0-8176-3675-3)
• (de) Kurt Gödel, « Über die Länge von Beweisen », Ergebinisse eines mathematischen Kolloquiums, vol. 7,‎ 1936, p. 23–24 (lire en ligne)
• (en) C. Smoryński, « The varieties of arboreal experience », Math. Intelligencer, vol. 4, n^o 4,‎ 1982, p. 182–189 (MR 0685558, lire en ligne)

• Théorème d'accélération de Blum (en)
• Longueur d'une démonstration

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Gödel's speed-up theorem » (voir la liste des auteurs).