ChapitreCalculabilité

Suites codées et démonstrations dans l'arithmétique de Peano

Les fonctions primitives récursives n'ont pas de symbole dans le langage de l'arithmétique, mais, comme l'arithmétique de Peano démontre l'existence et l'unicité de leurs valeurs, on raisonne avec elles comme avec des termes, et elle démontre tous les calculs clos. Elle démontre aussi, par des récurrences, les propriétés générales du codage des suites finies de l'arithmétisation de la syntaxe : tout entier non nul s'écrit $2^n(2k + 1)$, un code se décompose en son début et son dernier terme, la longueur et les termes d'une concaténation se calculent, et un code est déterminé par sa longueur et ses termes. La récurrence de valeurs, qui définit les termes et les formules, y devient une équation démontrable.

La formule naturelle de démontrabilité d'une théorie dont les axiomes forment un ensemble récursivement énumérable est alors équivalente dans l'arithmétique de Peano à une formule de démontrabilité $\exists y\, \delta$, et l'arithmétique de Peano démontre que deux démonstrations mises bout à bout et suivies d'un modus ponens en forment une : c'est la deuxième condition de dérivabilité. Il ne reste, pour le second théorème d'incomplétude, que la troisième.