Des axiomes primitifs récursifs pour toute théorie récursivement axiomatisée

Une énumération primitive récursive. Soit $A$ l'ensemble des codes des axiomes de $T$, et $R$ une relation récursive telle que $a \in A \iff \exists y\ R(a, y)$ (Récursif, r.e.). La fonction $f(a) \simeq \mu y\, R(a, y)$ est récursive (Fonctions récursives, (iii)) ; par la définition de la minimisation, elle est définie exactement sur $A$.

Par le point (i) de la forme normale de Kleene, $f$ a un indice $e$. Comme la fonction $U_1$ est totale, $f(a)$ est défini si et seulement s'il existe $t$ tel que $T_1(e, a, t)$. Ainsi $$a \in A \iff \exists t\ \ T_1(e, a, t),$$ où la relation $T_1$ est primitive récursive.

La théorie $T'$. Posons $$T' = \big\{\sigma^{(t)} : \sigma \in T,\ t \in \mathbb N,\ T_1(e, \ulcorner \sigma \urcorner, t)\big\}.$$ Ses éléments sont des énoncés. En effet, $\sigma^{(t)}$ est une formule, et toute occurrence de variable de $\sigma^{(t)}$ se trouve dans l'une des copies de $\sigma$ ; comme $\sigma$ est un énoncé, elle y est dans la portée d'un quantificateur de cette copie, donc liée dans $\sigma^{(t)}$.

Montrons qu'un entier $N$ est le code d'un élément de $T'$ si et seulement si $$\begin{aligned} &\exists a < N + 1\ \ \exists t < N + 1 \\ &\quad \big(N = c(a, t) \wedge T_1(e, a, t)\big), \end{aligned}$$ relation primitive récursive par les points (i) et (iii) de Clôture.

Si $N = c(a, t)$ et $T_1(e, a, t)$, alors $a \in A$ : l'entier $a$ est le code d'un axiome $\sigma$ de $T$, et $N = \ulcorner \sigma^{(t)} \urcorner$, avec $\sigma^{(t)} \in T'$.

Réciproquement, si $N$ est le code d'un élément de $T'$, il existe, par la définition de $T'$, un axiome $\sigma$ de $T$ et un entier $t$ tels que $T_1(e, \ulcorner \sigma \urcorner, t)$ et $N = \ulcorner \sigma^{(t)} \urcorner$ ; un même mot peut s'écrire $\sigma^{(t)}$ de plusieurs façons, par exemple $\sigma^{(1)} = (\sigma \wedge \sigma)^{(0)}$, et l'on prend ces témoins-là. Les témoins $a = \ulcorner \sigma \urcorner$ et $t$ conviennent, et ils sont au plus égaux à $N$. D'une part, $\sigma$ est un facteur de $\sigma^{(t)}$, donc $\ulcorner \sigma \urcorner \leqslant N$ par le point (ii) de Codage des mots. D'autre part, par ce même point, les préfixes du mot de code $N$ ont des codes strictement croissants avec leur longueur, à partir du code $0$ du mot vide ; donc $\mathrm{lg}(N) \leqslant N$, et $t \leqslant (t + 1)\,\mathrm{lg}(\ulcorner \sigma \urcorner) + 3t = \mathrm{lg}(N)$.

Un lemme de remplacement. Soit $\Gamma$ et $\Delta$ deux théories telles que chaque élément de $\Delta$ soit démontrable à partir de $\Gamma$. Alors toute formule démontrable à partir de $\Delta$ l'est à partir de $\Gamma$.

En effet, soit $\gamma_0, \dots, \gamma_{l-1}$ une démonstration formelle à partir de $\Delta$. Remplaçons chaque $\gamma_j$ qui appartient à $\Delta$ par la démonstration formelle de $\gamma_j$ à partir de $\Gamma$ de plus petit code (Démonstrations), qui se termine par $\gamma_j$. Dans la suite obtenue, chaque formule est un axiome logique, un élément de $\Gamma$, ou se déduit par modus ponens de deux formules qui la précèdent : c'est le cas à l'intérieur de chaque bloc inséré, et une formule $\gamma_j$ obtenue par modus ponens à partir de $\gamma_i$ et de $\gamma_{i'}$, avec $i, i' < j$, vient encore après ces deux formules, qui figurent toujours dans la suite. C'est une démonstration formelle à partir de $\Gamma$, terminée par $\gamma_{l-1}$.

Mêmes théorèmes. Soit $P$ une lettre propositionnelle et $P^{(t)}$ défini comme $\sigma^{(t)}$. Par récurrence sur $t$ et par la table de $\wedge$ (Connecteurs), $P^{(t)}$ prend la même valeur que $P$ sous toute valuation : les formules $P \to P^{(t)}$ et $P^{(t)} \to P$ sont des tautologies. Le remplacement se faisant lettre par lettre, on obtient $\sigma \to \sigma^{(t)}$ et $\sigma^{(t)} \to \sigma$ en remplaçant $P$ par $\sigma$ : ce sont des instances de tautologies, donc des axiomes logiques du groupe (1) de Démonstrations formelles.

Tout élément de $T'$ s'écrit $\sigma^{(t)}$ avec $\sigma \in T$, et la suite $\sigma$, $\sigma \to \sigma^{(t)}$, $\sigma^{(t)}$ est alors une démonstration formelle à partir de $T$. Si $\sigma \in T$, alors $\ulcorner \sigma \urcorner \in A$ ; soit $t$ le plus petit entier tel que $T_1(e, \ulcorner \sigma \urcorner, t)$. Alors $\sigma^{(t)} \in T'$, et la suite $\sigma^{(t)}$, $\sigma^{(t)} \to \sigma$, $\sigma$ est une démonstration formelle à partir de $T'$. Le lemme de remplacement, appliqué dans les deux sens, donne (i).

(ii) La première assertion est le point (ii) de Démonstrations, appliqué à $T'$, et l'équivalence en résulte par (i), puisque $T' \vdash \varphi$ signifie qu'une démonstration formelle de $\varphi$ à partir de $T'$ existe. Deux théories qui démontrent les mêmes formules sont cohérentes en même temps, par la définition de la cohérence (Cohérence).