Proposition 9Arithmétisation de la syntaxe

Démonstrations formelles codées

Une démonstration formelle $\gamma_0, \dots, \gamma_{l-1}$ se code par l'entier $\langle \ulcorner \gamma_0 \urcorner, \dots, \ulcorner \gamma_{l-1} \urcorner \rangle$ , code de la suite des codes de ses formules (Codages). Tout entier $p$ code ainsi une unique suite de $\mathrm{lg}(p)$ mots, de codes $(p)^0, \dots, (p)^{\mathrm{lg}(p) - 1}$ .

Énoncé

(i) La relation $\mathrm{MP}(a, b, c)$ : « $b$ est le code du mot ${\to}\, \alpha\, \gamma$ , où $\alpha$ et $\gamma$ sont les mots de codes $a$ et $c$ », qui dit que $\gamma$ se déduit de $\alpha$ et de $\alpha \to \gamma$ par modus ponens, est primitive récursive.

(ii) Soit $T$ une théorie sur la signature de l'arithmétique dont l'ensemble $\mathrm{Ax}_T$ des codes des éléments est primitif récursif. La relation $\mathrm{Dem}_T(p, c)$ : « $p$ code une démonstration formelle à partir de $T$ de la formule de code $c$ » est primitive récursive.

Démonstration

(i) En notation préfixée, $\alpha \to \gamma$ est le mot ${\to}\, \alpha\, \gamma$ . Ainsi $\mathrm{MP}(a, b, c) \iff b = \mathrm{cc}(\langle 2 \rangle, a, c)$ , relation primitive récursive par Codage des mots.

(ii) La définition de Démonstrations formelles se traduit, avec $l = \mathrm{lg}(p)$ , par $\begin{aligned} \mathrm{Dem}_T(p, c) \iff{} &l \geqslant 1 \wedge (p)^{l \mathbin{\dot{-}} 1} = c \\ &\wedge \forall j < l\ \big(\mathrm{Fm}((p)^j) \\ &\qquad \wedge D(p, j)\big), \end{aligned}$ où $D(p, j)$ est la disjonction de $\mathrm{Ax}((p)^j)$ , de $\mathrm{Ax}_T((p)^j)$ et de $\exists i < j\ \exists i' < j\ \ \mathrm{MP}\big((p)^i, (p)^{i'}, (p)^j\big).$ Elle dit que la suite codée par $p$ est une suite finie de formules, terminée par la formule de code $c$ , dont chacune est un axiome logique, un élément de $T$ , ou se déduit de deux formules précédentes par modus ponens. Elle est primitive récursive par (i), par Axiomes logiques et par Clôture.

□

Remarque

Pour $T = \varnothing$ , la suite réduite à la formule $x_0 = x_0$ , axiome du groupe (5), est une démonstration formelle. Son code est $\langle 2^{34} \cdot 17 \rangle = 2^{35} \cdot 17 + 1 = 584\,115\,552\,257$ , et $\mathrm{Dem}_\varnothing(584\,115\,552\,257,\ 2^{34} \cdot 17)$ est vraie.

Remarque

La relation « $c$ est le code d'une formule démontrable à partir de $T$ » s'écrit $\exists p\ \mathrm{Dem}_T(p, c)$ : la quantification sur $p$ n'est pas bornée, et rien ne garantit que cette relation soit primitive récursive, ni même récursive. Le nœud Théorèmes r.e. en tire seulement qu'elle est récursivement énumérable.

Remarque

Gödel a mené cette arithmétisation dans son article « Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I » (Monatshefte für Mathematik und Physik 38, 1931, p. 173-198). Il y définit successivement quarante-cinq fonctions et relations, qu'il appelle « rekursiv », jusqu'à la relation « $x$ est une démonstration de la formule $y$ » ; la quarante-sixième, « $x$ est démontrable », obtenue par une quantification non bornée comme ci-dessus, est la seule dont il ne puisse affirmer qu'elle le soit. Il codait les suites par les exposants des nombres premiers, et non par le code des mots employé ici.

Le nom actuel est postérieur : selon Kleene (« Origins of recursive function theory », Annals of the History of Computing 3, 1981), la récurrence primitive porte ce nom depuis Rózsa Péter (1934), et les fonctions « récursives » de Gödel sont appelées primitives récursives depuis l'article de Kleene de 1936 sur les fonctions récursives générales.

Repose sur

Les axiomes logiques forment un ensemble primitif récursif

Sert à

Aucune fiche de ce graphe ne l'utilise encore.