Les théorèmes d'une théorie récursivement axiomatisée

(i) Les formules, les énoncés et les axiomes logiques sont traités au chapitre Arithmétisation de la syntaxe : Formules, (ii), Variables libres, (iv), et Axiomes logiques. Une relation primitive récursive est récursive (Fonctions récursives, (i)).

Restent les axiomes de $\mathsf{PA}$. Les six premiers sont des énoncés fixés, de codes $c_1, \dots, c_6$ : l'ensemble de leurs codes a pour fonction caractéristique $\mathrm{sg}\big(\chi_=(N, c_1) + \cdots + \chi_=(N, c_6)\big)$, primitive récursive.

Pour le schéma de récurrence, $P \wedge Q$ abrège $\neg(P \to \neg Q)$ (Connecteurs), et la formule dont on prend la clôture s'écrit en notation préfixée $$\begin{aligned} &{\to}\, \neg\, {\to}\, \varphi[0/x]\ \neg\, \forall x\, {\to}\, \varphi\ \varphi[S\,x/x] \\ &\quad \forall x\, \varphi. \end{aligned}$$ Pour $x = a_k$ et $\varphi$ de code $a$, son code est donc, avec les fonctions de Codage des mots et de Substitution, $$\begin{aligned} I(a, k) = \mathrm{cc}\big(&\langle 2, 1, 2 \rangle, \mathrm{Sb}(a, \langle 4 \rangle, k), \\ &\langle 1, 3, k, 2 \rangle, a, \\ &\mathrm{Sb}(a, \langle 5, k \rangle, k), \langle 3, k \rangle, a\big), \end{aligned}$$ fonction primitive récursive de $(a, k)$, puisque $\langle 4 \rangle$ et $\langle 5, k \rangle$ sont les codes des termes $0$ et $S\,x$ ; c'est le code d'une formule par le point (iii) de Substitution.

Un entier $M$ code un axiome de récurrence si et seulement s'il existe $a \leqslant M$, $k < M$ et $g < \mathrm{lg}(M) + 1$ tels que $\mathrm{Fm}(a)$, $k \geqslant 8$, $2g \leqslant \mathrm{lg}(M)$, $\mathrm{sm}(M, 2g, \mathrm{lg}(M)) = I(a, k)$, et que les $g$ blocs du début énumèrent, par indices croissants, les variables libres de la formule de code $I(a, k)$. Les bornes viennent de ce que $\varphi$ est un facteur du mot de code $M$ et $a_k$ une de ses lettres (Codage des mots, (ii) et (iii)).

La dernière condition s'écrit, avec $J = I(a, k)$ et la relation $\mathrm{VL}$ de Variables libres : pour tout $m < g$, $(M)^{2m} = 3$, $\mathrm{VL}(J, (M)^{2m+1})$, et $(M)^{2m+1} < (M)^{2m+3}$ si $m + 1 < g$ ; et, pour tout $j < \mathrm{lg}(J)$ tel que $\mathrm{Lib}(J, j)$, il existe $m < g$ tel que $(M)^{2m+1} = (J)^j$. Toutes ces relations sont primitives récursives, et la réunion de deux ensembles primitifs récursifs l'est aussi (Clôture, (i)).

(ii) C'est le point (i) de Démonstrations : en notation préfixée, $\psi$ est le mot $\to \varphi\, \chi$, et la relation est $\ulcorner \psi \urcorner = \mathrm{conc}\big(\mathrm{conc}(\langle 2 \rangle, \ulcorner \varphi \urcorner), \ulcorner \chi \urcorner\big)$.

(iii) Soit $R$ une relation récursive telle que $a$ soit le code d'un axiome de $T$ si et seulement si $\exists y\, R(a, y)$. Une démonstration formelle $\gamma_0, \dots, \gamma_{l-1}$ se code par la suite $\langle \ulcorner \gamma_0 \urcorner, \dots, \ulcorner \gamma_{l-1} \urcorner \rangle$, comme au nœud Démonstrations, où le cas d'un ensemble d'axiomes primitif récursif est traité ; il faut ici des témoins pour les axiomes de $T$.

Considérons la relation $D(p, w, c)$ : l'entier $c$ code un énoncé, $\mathrm{lg}(p) \geqslant 1$ et $(p)^{\mathrm{lg}(p) - 1} = c$.

De plus, pour tout $j < \mathrm{lg}(p)$, l'une des trois conditions suivantes est remplie : $(p)^j$ code un axiome logique ; $R\big((p)^j, (w)_j\big)$ ; il existe $i, i' < j$ tels que $(p)^j$ se déduise de $(p)^i$ et $(p)^{i'}$ par modus ponens.

Elle est récursive, par (i), (ii) et les quantifications bornées (Fonctions récursives, (ii)).

Si $T \vdash \sigma$, soit $p$ le code d'une démonstration de $\sigma$ ; pour chaque $j$ tel que $(p)^j$ code un axiome de $T$, soit $y_j$ le plus petit $y$ tel que $R((p)^j, y)$, et $y_j = 0$ sinon. Alors $D(p, w, \ulcorner \sigma \urcorner)$ pour $w = \prod_{j} p_j^{y_j}$. Réciproquement, $D(p, w, c)$ dit que $p$ code une démonstration de l'énoncé de code $c$. Ainsi $$T \vdash \sigma \iff \exists p\ \exists w\ D(p, w, \ulcorner \sigma \urcorner),$$ et l'on conclut par le point (iv) de Récursif, r.e.. Pour $\mathsf{PA}$, l'ensemble des codes des axiomes est récursif par (i), donc récursivement énumérable.