Les ensembles récursivement énumérables sont définis par des formules Σ₁

(i) Renommage. Si $\varphi$ est équivalente à $\exists y\, \delta$ et si $y'$ est une variable qui ne figure pas dans $\delta$, elle l'est à $\exists y'\, \delta[y'/y]$, qui est Σ₁ par le point (i) de Σ₁-complétude. En effet, par le lemme de substitution et le lemme de coïncidence, $\delta[y'/y]$ est satisfaite sous $s(y' \mid m)$ si et seulement si $\delta$ l'est sous $s(y \mid m)$. On peut donc toujours prendre la variable $y$ hors d'un ensemble fini de variables donné. Les variables liées des bornes introduites ci-dessous sont, elles aussi, prises nouvelles.

On raisonne par récurrence sur la construction de $\mathcal S$. Une formule Δ₀ $\delta$ est équivalente à $\exists y\, \delta$ pour une variable $y$ qui n'y figure pas, par le lemme de coïncidence. Soit $\varphi_1$ et $\varphi_2$ équivalentes à $\exists y_1\, \delta_1$ et $\exists y_2\, \delta_2$, et $w$ une variable nouvelle ; par le renommage, on suppose $y_1$, $y_2$ et $w$ distinctes, $y_1$ absente de $\delta_2$ et $y_2$ absente de $\delta_1$, et aucune de ces trois variables libre dans $\varphi_1$ ou $\varphi_2$. Alors :

$\varphi_1 \wedge \varphi_2$ est équivalente à $\exists w\ \exists y_1 \leqslant w\ \exists y_2 \leqslant w\ (\delta_1 \wedge \delta_2)$ : si $m_1$ et $m_2$ sont des témoins, $w = \max(m_1, m_2)$ en est un, et la réciproque est immédiate ;

$\varphi_1 \vee \varphi_2$ est équivalente à $\exists w\, (\delta_1[w/y_1] \vee \delta_2[w/y_2])$ ;

$\exists x\, \varphi_1$, pour $x \neq y_1$, est équivalente à $\exists w\ \exists x \leqslant w\ \exists y_1 \leqslant w\ \delta_1$, avec le maximum des deux témoins.

Soit enfin $\varphi = \forall x \leqslant t\ \varphi_1$, où $t$ ne contient ni $x$ ni la variable liée $z$ de la borne, et $y_1$, $w$ absentes de $t$ et distinctes de $x$ et $z$. Elle est équivalente à $\exists w\ \forall x \leqslant t\ \exists y_1 \leqslant w\ \delta_1$. Soit $s$ une valuation et $m$ la valeur de $t$ sous $s$, qui ne dépend ni de $x$ ni de $w$. Si $\varphi$ est satisfaite sous $s$, pour chaque $k \leqslant m$ il existe un entier $j$ tel que $\delta_1$ soit satisfaite sous $s(x \mid k)(y_1 \mid j)$ ; soit $j_k$ le plus petit. L'entier $\max(j_0, \dots, j_m)$ est un témoin pour $w$. La réciproque est immédiate.

Dans chaque cas, la formule obtenue est Σ₁ à un quantificateur, par la définition des formules Δ₀, et ses variables libres sont parmi celles de $\varphi$ et la variable quantifiée en tête, puisque seules des variables liées ont été ajoutées.

(ii) Les graphes des fonctions récursives. Montrons que le graphe de toute fonction récursive est défini par une formule de $\mathcal S$. Les changements de variables du point (i) de Définissabilité se font par une formule $\exists v_1 \cdots \exists v_n\, (v_1 = w_{\alpha(1)} \wedge \cdots \wedge \varphi)$, qui reste dans $\mathcal S$ si $\varphi$ y est ; on peut donc choisir librement les variables, et l'on note $F(x, y)$ une formule de $\mathcal S$ qui définit le graphe de $f$, lu « $f(x) = y$ ». Dans ces notations, $x$ abrège une suite de variables distinctes, et non la variable $x_0$ du langage. Les fonctions de base sont définies, avec des variables distinctes $v_1, \dots, v_n$ et $v$, par les formules atomiques $v = 0$, $v = S\,v_1$ et $v = v_i$. Pour la composition, $h(x) = y$ est défini par $\exists z_1 \cdots \exists z_m\, (G_1(x, z_1) \wedge \cdots \wedge G_m(x, z_m) \wedge F(z, y))$. Pour la minimisation, $\mu y\, [f(x, y) = 0] = y$ est défini par $$\begin{aligned} &\exists w'\, \big(F(x, y, w') \wedge w' = 0\big) \\ &\wedge \forall z \leqslant y\ \big(z = y \vee {} \\ &\qquad \exists w\, (F(x, z, w) \wedge \neg(w = 0))\big), \end{aligned}$$ où $F(x, y, w')$ et $F(x, z, w)$ désignent des formules de $\mathcal S$ qui définissent le graphe de $f$ avec les variables indiquées, obtenues par le changement de variables ci-dessus, sans substitution d'un terme.

Pour la récurrence primitive, soit $B(a, b, i, u)$ la formule $$\begin{aligned} &\exists q\ \exists r\ \big(a = q \times S(S\,i \times b) + u \\ &\qquad \wedge r + u = S\,i \times b\big), \end{aligned}$$ qui est dans $\mathcal S$. Dans $\mathcal N$, elle dit que $a = qm + u$ avec $u \leqslant m - 1$, où $m = 1 + (i + 1)b$, c'est-à-dire que $u$ est le reste de la division de $a$ par $m$ : elle définit le graphe de la fonction β. Alors $h(x, y) = v$ est défini par l'existence de $a$ et $b$ tels que $$\begin{aligned} &\exists u\, \big(F(x, u) \wedge B(a, b, 0, u)\big) \\ &\wedge \forall i \leqslant y\ \big(i = y \vee \exists u\, \exists u' \\ &\qquad (B(a, b, i, u) \wedge B(a, b, S\,i, u') \\ &\qquad \wedge G(x, i, u, u'))\big) \\ &\wedge B(a, b, y, v), \end{aligned}$$ et, sans paramètre, la première ligne est remplacée par $B(a, b, 0, \underline c)$. Dans chacune des formules $B(a, b, \dots)$ ainsi écrites, les termes indiqués sont substitués à $i$ et à $u$, et les variables liées $q$ et $r$ de $B$ sont prises distinctes de toutes les autres.

Dans $\mathcal N$, la formule $\forall z \leqslant y\ (z = y \vee \chi)$ dit que $\chi$ est satisfaite pour tout $z < y$. Chacune de ces formules a donc, dans $\mathcal N$, le sens de la formule correspondante de la preuve du point (ii) de Définissabilité, et la vérification qui y est faite s'applique sans changement.

Les ensembles récursivement énumérables. Soit $A \subset \mathbb N^n$, avec $x \in A \iff \exists y\ R(x, y)$ pour une relation récursive $R$, et $\Gamma(v_1, \dots, v_n, y, u)$ une formule de $\mathcal S$ qui définit le graphe de sa fonction caractéristique. La formule $\exists y\, \exists u\, (\Gamma \wedge u = S\,0)$ est dans $\mathcal S$ et définit $A$ avec les variables $v_1, \dots, v_n$. Par (i) et le renommage, elle est équivalente à une formule $\exists y\, \delta$ de la forme annoncée, et la définition de la satisfaction de $\exists$ donne la dernière assertion.