ChapitreCalculabilité

Σ₁-complétude formalisée et troisième condition de dérivabilité

Quand les variables auxquelles on substitue des chiffres ne sont quantifiées nulle part, la substitution n'a plus besoin de savoir quels facteurs d'un mot sont des formules : elle remplace chaque lettre de la variable par le chiffre, et laisse les autres. L'arithmétique de Peano démontre alors, pour des codes qui dépendent de variables, que les lettres $\forall$ restent suivies de variables liées, que la substitution agit lettre à lettre, et qu'elle se compose ; elle reconnaît les axiomes qui instancient une formule à plusieurs paramètres, et l'on obtient une logique à plusieurs paramètres sous la formule naturelle de démontrabilité des formules.

Elle démontre ensuite, par des récurrences menées à l'intérieur de l'arithmétique de Peano et poussées sous la démontrabilité, les tables d'addition et de multiplication des chiffres, la valeur de tout terme, puis, pour toute formule Δ₀ dont les variables liées ont été renommées, qu'elle entraîne sa propre démontrabilité ; c'est la Σ₁-complétude formalisée. Appliquée à l'énoncé $\mathrm{Pr}_T\,\ulcorner \varphi \urcorner$, elle donne la troisième condition de dérivabilité, et, avec le chapitre Lemme diagonal et démontrabilité, le théorème de Löb et le second théorème d'incomplétude pour la formule naturelle de démontrabilité, désormais entièrement démontrés.