ChapitreCalculabilité

Substitution et instances dans l'arithmétique de Peano

La troisième condition de dérivabilité demande que l'arithmétique de Peano raisonne sur des formules où l'on a substitué à une variable le chiffre d'un entier quelconque. Elle démontre d'abord qu'un facteur d'un mot a un code plus petit, que la concaténation est associative, et qu'on forme des termes et des formules par les règles de la syntaxe ; le code du chiffre d'un entier variable est celui d'un terme formé des seules lettres $S$ et $0$. Pour une formule fixée, la substitution se déplie en une concaténation de morceaux fixés et du terme substitué, si bien que l'arithmétique de Peano démontre que les instances d'une formule fixée sont des formules, et que les chiffres y sont substituables.

Il en résulte qu'elle reconnaît les axiomes logiques qui instancient une formule fixée par un chiffre variable, et qu'elle démontre l'instanciation formalisée : d'une démonstration d'une formule universelle, on tire une démonstration de chacune de ses instances. Avec la mise bout à bout des démonstrations du chapitre précédent, on obtient une logique à un paramètre sous la formule naturelle de démontrabilité des formules $\mathrm{Prf}_T$ ; avec un paramètre, le code obtenu n'est pas, en général, celui d'un énoncé. Instancier plusieurs variables demande de substituer dans un code qui n'est plus fixé, ce qui exige un argument de plus : le chapitre suivant le trouve dans une restriction aux paramètres qui ne sont quantifiés nulle part.