ChapitreCalculabilité

La fonction β et les fonctions primitives récursives dans l'arithmétique de Peano

Une suite finie n'est pas un objet du langage de l'arithmétique, mais un couple d'entiers la code par la fonction $\beta$ de Gödel. L'arithmétique de Peano démontre que la formule qui définit le graphe de $\beta$ définit une fonction, et qu'une suite codée se prolonge d'un terme quelconque, par un lemme chinois pour une famille bornée de modules, sans factorielle ni nombres premiers.

Il en résulte que les formules qui transcrivent les définitions des fonctions primitives récursives, par composition et par récurrence primitive, définissent des fonctions aux yeux de l'arithmétique de Peano, et qu'elle en démontre les équations de définition. Les fonctions usuelles s'y reconnaissent, et les relations primitives récursives y reçoivent une formule naturelle, pour laquelle elle démontre les règles de calcul des connecteurs, des quantifications bornées, de la définition par cas et de la minimisation bornée. C'est la deuxième étape de la démonstration des conditions de dérivabilité du second théorème d'incomplétude.