Les axiomes logiques forment un ensemble primitif récursif

Notons $\langle 2, 3, k \rangle$, etc., les codes de mots fixés suivis d'une lettre $a_k$, primitifs récursifs en $k$ (Codage des mots, (i)). Pour chaque groupe, on borne les composantes par $M$, ce que justifie le point (iii) du codage pour les lettres et le point (ii) pour les facteurs.

Groupe (1). C'est l'ensemble $\mathrm{Inst}$ de Tautologies.

Groupe (2). Soit $A_2(M)$ la relation : $\mathrm{Fm}(M)$, et il existe $k < M$, $a \leqslant M$ et $T \leqslant M$ tels que $k \geqslant 8$, $\mathrm{Fm}(a)$, $\mathrm{Tm}(T)$, $\mathrm{Sbl}(T, k, a)$ et $$M = \mathrm{cc}\big(\langle 2, 3, k \rangle, a, \mathrm{Sb}(a, T, k)\big).$$ Elle est primitive récursive par Substitution.

Si $M$ code un axiome ${\to}\, \forall x\, \alpha\ \alpha[t/x]$, où $x = a_k$ et $t$ est substituable à $x$ dans $\alpha$, alors $k < M$ et $\ulcorner \alpha \urcorner \leqslant M$, puisque $\alpha$ est un facteur. Si $x$ a une occurrence libre dans $\alpha$, $t$ est un facteur de $\alpha[t/x]$ et $\ulcorner t \urcorner \leqslant M$.

Sinon, $\alpha[t/x] = \alpha = \alpha[x/x]$, et le terme $x$, de code $2k + 1 \leqslant M$, est substituable à $x$ dans $\alpha$ : une occurrence libre de $x$ ne peut se trouver dans une sous-formule $\forall x\, \psi$, où elle serait liée. Dans les deux cas, $A_2(M)$. Réciproquement, si $A_2(M)$, le mot de code $M$ est ${\to}\, \forall x\, \alpha\ \alpha[t/x]$, avec $t$ substituable à $x$ dans $\alpha$, par le point (i) de Substitution : $A_2$ est exactement le groupe (2).

La condition $\mathrm{Fm}(M)$ est automatique, puisque $\alpha[t/x]$ est une formule par le point (iii) de Substitution ; l'écrire ne change pas la relation.

Groupe (3). $A_3(M)$ : il existe $k < M$ et $a, b \leqslant M$ tels que $k \geqslant 8$, $\mathrm{Fm}(a)$, $\mathrm{Fm}(b)$ et $$\begin{aligned} M = \mathrm{cc}\big(&\langle 2, 3, k, 2 \rangle, a, b, \\ &\langle 2, 3, k \rangle, a, \langle 3, k \rangle, b\big). \end{aligned}$$

Groupe (4). $A_4(M)$ : il existe $k < M$ et $a \leqslant M$ tels que $k \geqslant 8$, $\mathrm{Fm}(a)$, $\neg\mathrm{VL}(a, k)$ et $M = \mathrm{cc}(\langle 2 \rangle, a, \langle 3, k \rangle, a)$, avec la relation $\mathrm{VL}$ de Variables libres.

Groupe (5). $A_5(M)$ : il existe $k < M$ tel que $k \geqslant 8$ et $M = \langle 0, k, k \rangle$ ; ou bien $\mathrm{Fm}(M)$, et il existe $k, k' < M$ et $a, a' \leqslant M$ tels que $k, k' \geqslant 8$, $\mathrm{At}(a)$, $\mathrm{lg}(a') = \mathrm{lg}(a)$, $$\begin{aligned} &\forall j < \mathrm{lg}(a)\ \big((a')^j = (a)^j \\ &\quad\vee ((a)^j = k \wedge (a')^j = k')\big), \end{aligned}$$ et $M = \mathrm{cc}(\langle 2, 0, k, k', 2 \rangle, a, a')$. Une formule atomique ne contient pas de lettre $\forall$ : ses occurrences de $x$ sont tous les rangs où figure la lettre $x$, et la condition dit que $\alpha'$ s'obtient en remplaçant certaines d'entre elles par $y$. Ici encore, $\mathrm{Fm}(M)$ est automatique, puisque $\alpha'$ est une formule par le point (iii) de Substitution, appliqué au terme $y$.

Généralisations. Enfin, $M$ code un axiome logique si et seulement s'il existe $g < \mathrm{lg}(M) + 1$ tel que $2g \leqslant \mathrm{lg}(M)$, $$\forall m < g\ \big((M)^{2m} = 3 \wedge (M)^{2m+1} \geqslant 8\big),$$ et que $\mathrm{sm}(M, 2g, \mathrm{lg}(M))$ appartienne à $\mathrm{Inst}$ ou vérifie l'une des relations $A_2$ à $A_5$. Cette relation est primitive récursive par Clôture.