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

En logique mathématique, le théorème d'accélération de Gödel (ou théorème de speed-up), démontré par Kurt Gödel en 1936, montre l'existence de théorèmes ayant des démonstrations très longues, mais qui peuvent être considérablement raccourcies en utilisant un système d'axiomes légèrement plus puissant.

## Description informelle

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.

## Énoncé rigoureux du théorème

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 :
* G(N) est un théorème de T.
* La plus courte démonstration de G(N) dans T comporte au moins N symboles.
* 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.
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$.

## Autres exemples et conséquences

Ce théorème de Gödel semble être passé relativement inaperçu ; Jean-Paul Delahaye signale 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.
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. Des résultats analogues découlent également du théorème de Goodstein.
Une conséquence de ces résultats est la construction de théories non cohérentes, mais où la plus courte contradiction n’apparaît qu’après un nombre d’étapes physiquement inaccessibles (par exemple la théorie « T et non G(N) ») ; le fait qu’une théorie de ce genre apparaisse cohérente en pratique affaiblit un peu les arguments usuels sur la validité des systèmes formels.