Les fonctions primitives récursives dans l'arithmétique de Peano

(i) L'ensemble des formules $\varphi$ de $\mathcal S$ telles que $\varphi[t/v]$ soit dans $\mathcal S$ pour toute variable $v$ et tout terme $t$ dont aucune variable n'est quantifiée dans $\varphi$ contient les formules Δ₀, par le point (i) de Σ₁-complétude, et il est stable par $\wedge$ et $\vee$, qui commutent à la substitution. Soit $\varphi = \exists x\, \varphi_1$, avec $\varphi_1$ dans cet ensemble : si $v = x$, la variable $v$ n'est pas libre et $\varphi$ ne change pas ; sinon, $\varphi[t/v] = \exists x\, \varphi_1[t/v]$, puisque $x$, quantifiée dans $\varphi$, ne figure pas dans $t$. Soit $\varphi = \forall x \leqslant r\ \varphi_1$, écrite avec la variable liée $z$ : comme au point (i) de Σ₁-complétude, $\varphi$ ne change pas si $v = x$, devient $\forall x \leqslant r\ \varphi_1[t/z]$ si $v = z$, et devient $\forall x \leqslant r[t/v]\ \varphi_1[t/v]$ sinon, où $r[t/v]$ ne contient ni $x$ ni $z$. Dans chaque cas, la formule obtenue est dans $\mathcal S$, et l'ensemble considéré contient $\mathcal S$. Une substitution simultanée s'obtient, comme au point (iv) de Récurrence dans PA, par des substitutions successives de variables nouvelles puis des termes, qui sont chacune de cette forme.

(ii) Par le point (iv) de Récurrence dans PA, appliqué à (b) et aux termes $t_k$, qui ne contiennent aucune variable quantifiée dans $\exists w\, \varphi$, on a $\vdash_{\mathsf{PA}} (\exists w\, \varphi)[t/v]$, qui est $\exists w\, \varphi[t/v]$ puisque $w$ est distincte des $v_k$ : c'est $\exists w\ f(t) = w$. Soit $w'$ une variable qui ne figure ni dans $\varphi$, ni dans les $t_k$, ni dans $s$ et $s'$. Le même point, appliqué à (c) et aux termes $t_1, \dots, t_n, s, s'$ substitués à $v_1, \dots, v_n, w, w'$, donne la seconde formule, puisque $w'$ ne figure pas dans $\varphi$ et que $\varphi[w'/w][t, s, s'/v, w, w'] = \varphi[t, s'/v, w]$.

(iii) Fonctions de base. Les trois formules sont atomiques, donc Δ₀, et elles définissent les graphes annoncés. L'introduction de l'existentiel, avec le terme $0$, $S\,v_1$ ou $v_k$, et la réflexivité de l'égalité donnent (b) ; la symétrie et la transitivité donnent (c), par exemple $(w = S\,v_1 \wedge w' = S\,v_1) \to w = w'$.

Composition. La formule, notée $\varphi_h$, est dans $\mathcal S$, puisque $\mathcal S$ est stable par $\wedge$ et par $\exists$ ; ses variables libres sont parmi les $v_k$ et $w$, et aucune d'elles n'y est quantifiée. Par la définition de la satisfaction et le lemme de coïncidence, $\varphi_h$ est satisfaite sous une valuation $\sigma$ si et seulement s'il existe des entiers $e_1, \dots, e_m$ tels que $g_j(\sigma(v)) = e_j$ pour chaque $j$ et $f(e_1, \dots, e_m) = \sigma(w)$, c'est-à-dire si et seulement si $h(\sigma(v)) = \sigma(w)$ : c'est (a).

Pour (b), le point (ii), appliqué à chaque $g_j$, et l'élimination fournissent des variables nouvelles $e_j$ telles que $g_j(v) = e_j$, puis, appliqué à $f$ avec les termes $e_1, \dots, e_m$, une variable nouvelle $e_0$ telle que $f(e_1, \dots, e_m) = e_0$. Les introductions successives de $\exists z_m$, …, $\exists z_1$, avec les termes $e_m$, …, $e_1$, puis de $\exists w$, avec le terme $e_0$, donnent $\exists w\, \varphi_h$, et l'on élimine les $e_j$.

Pour (c), soit $w'$ une variable qui ne figure pas dans $\varphi_h$ ; comme $w$ n'est libre que dans $\varphi_f$, la formule $\varphi_h[w'/w]$ est $\exists z_1 \cdots \exists z_m\, (\varphi_1 \wedge \cdots \wedge \varphi_m \wedge \varphi_f[w'/w])$. Sous les hypothèses $\varphi_h$ et $\varphi_h[w'/w]$, l'élimination fournit des variables nouvelles $e_j$ et $e'_j$ telles que $g_j(v) = e_j$, $f(e) = w$, $g_j(v) = e'_j$ et $f(e') = w'$. Le point (ii) donne $e_j = e'_j$ pour chaque $j$, le remplacement d'un terme (Calcul à variables libres, (v)), appliqué $m$ fois, donne $f(e) = w'$, et le point (ii) donne $w = w'$. On élimine les variables introduites.

(iv) Notons $A(a, b)$ la formule $\exists s\, (\varphi_f \wedge B(a, b, 0, s))$ et $R(a, b, y)$ la formule $\forall i < y\ X$, de sorte que $H$ est $\exists a\, \exists b\, \big(A(a, b) \wedge R(a, b, y) \wedge B(a, b, y, w)\big)$. Pour des variables $a'$, $b'$ qui n'y sont pas quantifiées, $A(a', b')$ et $R(a', b', y)$ s'obtiennent en les substituant à $a$ et $b$, et $X(t)$ désigne $X[t/i]$, écrite avec $a$, $b$ ou avec d'autres variables selon le contexte. La formule $B$ est dans $\mathcal S$, et, par (i), $B(a, b, 0, s)$, $B(a, b, S\,i, s')$ et $B(a, b, y, w)$ aussi ; comme $i = y$ est atomique, $H$ est dans $\mathcal S$. Ses variables libres sont parmi les $v_k$, $y$ et $w$, et aucune d'elles n'y est quantifiée. La variable $y$ ne figure pas dans $X$ : la formule $h(v, 0) = w$ est donc $\exists a\, \exists b\, (A(a, b) \wedge R(a, b, 0) \wedge B(a, b, 0, w))$, et $h(v, S\,y) = w$ s'obtient de même avec $S\,y$. Par le point (ii) de Graphe de β dans PA, $B(a, b, t, e)$ et $B(a, b, t, e')$ donnent $e = e'$ : c'est l'unicité de $B$. On écrit $f(v) = e$ pour $\varphi_f[e/s]$ et $g(v, t, e) = e'$ pour $\varphi_g[t, e, e'/i, s, s']$, comme en (ii).

Les équations, de droite à gauche. Sous l'hypothèse $f(v) = w$, le prolongement (Prolongement d'une suite, (ii)), écrit avec des variables liées distinctes de $w$ et instancié par les termes $0$, $0$, $0$, $w$ substitués à $a$, $b$, $n$, $x$, et l'élimination fournissent $a_0$ et $b_0$ tels que $B(a_0, b_0, 0, w)$. L'introduction, avec le terme $w$, donne $A(a_0, b_0)$, et le point (i) (a) de Modules de Gödel donne $R(a_0, b_0, 0)$ ; deux introductions donnent $h(v, 0) = w$.

Sous les hypothèses $h(v, y) = u$ et $g(v, y, u) = w$, l'élimination fournit $a_0$ et $b_0$ tels que $A(a_0, b_0)$, $R(a_0, b_0, y)$ et $B(a_0, b_0, y, u)$. Le prolongement, instancié par $a_0$, $b_0$, $S\,y$, $w$ et écrit avec des variables liées nouvelles, et l'élimination fournissent $a_1$ et $b_1$ tels que $B(a_1, b_1, S\,y, w)$ et tels que, par le point (i) (b) de Modules de Gödel et l'axiome (2), $B(a_0, b_0, t, e) \to B(a_1, b_1, t, e)$ pour tout terme $t$ tel que $t < S\,y$ et tout terme $e$ qui est une variable ou un terme clos, et qui est donc substituable. L'élimination de $A(a_0, b_0)$ fournit $e_0$ tel que $f(v) = e_0$ et $B(a_0, b_0, 0, e_0)$ ; comme $0 \leqslant y$, on a $0 < S\,y$, donc $B(a_1, b_1, 0, e_0)$, l'introduction donne $A(a_1, b_1)$, et l'on élimine $e_0$, qui ne figure pas dans $A(a_1, b_1)$. Pour $R(a_1, b_1, S\,y)$, le point (i) (c) de Modules de Gödel demande $X(y)$ et $R(a_1, b_1, y)$, avec $a_1$ et $b_1$. D'une part, $y < S\,y$ donne $B(a_1, b_1, y, u)$, et, avec $B(a_1, b_1, S\,y, w)$ et $g(v, y, u) = w$, deux introductions, avec les termes $w$ et $u$, donnent $X(y)$. D'autre part, sous l'hypothèse $i < y$, la formule $R(a_0, b_0, y)$ et le point (i) (b) du même nœud donnent $X(i)$, avec $a_0$ et $b_0$, et l'élimination fournit $e$ et $e'$ tels que $B(a_0, b_0, i, e)$, $B(a_0, b_0, S\,i, e')$ et $g(v, i, e) = e'$. Le point (v) de Ordre dans PA donne $i < S\,y$ et, puisque $i < y$ est $S\,i \leqslant y$, $S\,i < S\,y$ ; les deux formules $B$ passent à $a_1$, $b_1$, et deux introductions donnent $X(i)$ ; le point (i) (a) donne $R(a_1, b_1, y)$. Deux introductions, avec $a_1$ et $b_1$, donnent $h(v, S\,y) = w$, et l'on élimine les variables introduites.

Existence. Montrons $\vdash_{\mathsf{PA}} \exists w\ h(v, y) = w$ par récurrence sur $y$. Le point (b) pour $\varphi_f$ et le renommage donnent $\exists w\ f(v) = w$, et la première équation, de droite à gauche, et la monotonie de Récurrence dans PA, (ii), donnent le cas $0$. Sous l'hypothèse $\exists w\ h(v, y) = w$, l'élimination avec la variable $u$ donne $h(v, y) = u$ ; le point (ii), appliqué à $g$ avec les termes $v, y, u$, et l'élimination donnent $g(v, y, u) = e$, puis $h(v, S\,y) = e$ par la seconde équation, de droite à gauche, et l'introduction conclut.

Unicité. Soit $a'$, $b'$ et $j$ des variables nouvelles. Sous les hypothèses $A(a, b)$, $R(a, b, y)$, $A(a', b')$ et $R(a', b', y)$, montrons par récurrence sur $j$ la formule $j \leqslant y \to \exists s\, \big(B(a, b, j, s) \wedge B(a', b', j, s)\big)$. Pour $0$ : l'élimination dans $A(a, b)$ et dans $A(a', b')$ fournit $e$ et $e'$ tels que $f(v) = e$, $B(a, b, 0, e)$, $f(v) = e'$ et $B(a', b', 0, e')$ ; le point (ii) donne $e = e'$, d'où $B(a', b', 0, e)$, et l'introduction conclut. Pour le pas, sous l'hypothèse de récurrence et sous $S\,j \leqslant y$, c'est-à-dire $j < y$, on a $j \leqslant y$, et l'élimination fournit $k$ tel que $B(a, b, j, k)$ et $B(a', b', j, k)$. Le point (i) (b) de Modules de Gödel, appliqué à $R(a, b, y)$ et à $R(a', b', y)$ avec le terme $j$, et l'élimination fournissent $e$, $e'$, $d$, $d'$ tels que $B(a, b, j, e)$, $B(a, b, S\,j, e')$, $g(v, j, e) = e'$, $B(a', b', j, d)$, $B(a', b', S\,j, d')$ et $g(v, j, d) = d'$. L'unicité de $B$ donne $e = k = d$, le remplacement donne $g(v, j, e) = d'$, et le point (ii), appliqué à $g$, donne $e' = d'$ ; d'où $B(a', b', S\,j, e')$, et l'introduction donne la formule pour $S\,j$. La variable $j$ n'est libre dans aucune des quatre hypothèses, et le point (iii) de Récurrence dans PA conclut.

Soit alors $w'$ une variable qui ne figure pas dans $H$. Sous les hypothèses $h(v, y) = w$ et $h(v, y) = w'$, l'élimination fournit $a$, $b$, $a'$, $b'$ tels que les quatre hypothèses précédentes, $B(a, b, y, w)$ et $B(a', b', y, w')$. Ce qui précède, avec $y \leqslant y$, et l'élimination fournissent $k$ tel que $B(a, b, y, k)$ et $B(a', b', y, k)$ ; l'unicité de $B$ donne $w = k = w'$.

Les équations, de gauche à droite. Sous l'hypothèse $h(v, 0) = w$, l'élimination fournit $A(a, b)$ et $B(a, b, 0, w)$, puis $e$ tel que $f(v) = e$ et $B(a, b, 0, e)$ ; l'unicité de $B$ donne $e = w$, et le remplacement donne $f(v) = w$. Sous l'hypothèse $h(v, S\,y) = w$, l'élimination fournit $A(a, b)$, $R(a, b, S\,y)$ et $B(a, b, S\,y, w)$. Le point (i) (c) de Modules de Gödel donne $R(a, b, y)$ et $X(y)$, et l'élimination fournit $e$ et $e'$ tels que $B(a, b, y, e)$, $B(a, b, S\,y, e')$ et $g(v, y, e) = e'$. L'unicité de $B$ donne $e' = w$, donc $g(v, y, e) = w$ ; deux introductions donnent $h(v, y) = e$, et l'introduction, avec le terme $e$, donne $\exists u\, (h(v, y) = u \wedge g(v, y, u) = w)$.

Dans $\mathcal N$. La structure $\mathcal N$ est un modèle de $\mathsf{PA}$ (Gödel-Rosser, (iii)), et le théorème de correction y rend vrais les théorèmes précédents. Par l'existence, l'unicité et le lemme de substitution, pour tout $(x, k) \in \mathbb N^{n+1}$, il existe un unique entier $\tilde h(x, k)$ tel que $H$ soit satisfaite sous une valuation qui vaut $x$ en $v$, $k$ en $y$ et $\tilde h(x, k)$ en $w$. La première équation et le fait que $\varphi_f$ définit $f$ donnent $\tilde h(x, 0) = f(x)$ ; la seconde et le fait que $\varphi_g$ définit $g$ donnent $\tilde h(x, k + 1) = g(x, k, \tilde h(x, k))$. Par l'unicité de la récurrence primitive (Primitives récursives), $\tilde h = h$, et $H$ définit le graphe de $h$.

Sans paramètre. On remplace $A(a, b)$ par $B(a, b, 0, \underline c)$ et $f(v) = w$ par $w = \underline c$. Sous l'hypothèse $w = \underline c$, le prolongement donne $B(a_0, b_0, 0, w)$, puis $B(a_0, b_0, 0, \underline c)$ par le remplacement ; dans le second cas de droite à gauche, $B(a_0, b_0, 0, \underline c)$ et $0 < S\,y$ donnent $B(a_1, b_1, 0, \underline c)$ ; le cas $0$ de l'unicité prend le terme $\underline c$ ; et $B(a, b, 0, \underline c)$, $B(a, b, 0, w)$ donnent $w = \underline c$. Le reste ne change pas, et la valeur de $\underline c$ dans $\mathcal N$ est $c$.

(v) Soit $\chi$ la formule $\forall w\, (h(v, y) = w \leftrightarrow \psi)$ ; montrons $\vdash_{\mathsf{PA}} \chi$ par récurrence sur $y$. Le point (iv) et la première hypothèse donnent $h(v, 0) = w \leftrightarrow \psi[0/y]$, et la généralisation en $w$ donne $\chi[0/y]$. Sous l'hypothèse $\chi$, l'axiome (2), avec le terme $u$, donne $h(v, y) = u \leftrightarrow \psi[u/w]$, et la monotonie de Récurrence dans PA, (ii), appliquée dans les deux sens sous cette hypothèse où $u$ n'est pas libre, donne $\exists u\, (h(v, y) = u \wedge g(v, y, u) = w) \leftrightarrow \exists u\, (\psi[u/w] \wedge g(v, y, u) = w)$. Avec la seconde équation de (iv) et la seconde hypothèse, $h(v, S\,y) = w \leftrightarrow \psi[S\,y/y]$, et la généralisation en $w$, qui n'est pas libre dans $\chi$, donne $\chi[S\,y/y]$. Le point (iii) de Récurrence dans PA et l'axiome (2), avec le terme $w$, concluent. Sans paramètre, la preuve est la même.

(vi) Par récurrence sur la longueur de la construction, on montre l'assertion pour toutes les fonctions qui y figurent, tous les choix de variables et toutes les parties finies $V$ à la fois. Pour une fonction de base, les formules de (iii) n'ont pas de variable liée. Pour une composition, on prend des variables $z_1, \dots, z_m$ distinctes, hors de $V$ et différentes des $v_k$ et de $w$, et l'on obtient, par l'hypothèse de récurrence, des définitions $\varphi_j$ et $\varphi_f$ avec les variables indiquées, dont aucune variable liée n'est dans $V$ ni parmi les $v_k$, les $z_j$ et $w$ ; la clause (iii) s'applique. Pour une récurrence primitive, on prend de même $a$, $b$, $i$, $s$, $s'$ et les variables liées de $B$ et des bornes hors de $V$ et des variables libres, puis $\varphi_f$ et $\varphi_g$ dont les variables liées évitent toutes celles-là ; la clause (iv) s'applique. En prenant à chaque étape les premières variables convenables dans l'ordre $x_0, x_1, \dots$ du langage, on obtient une formule déterminée, sans aucun choix : c'est la définition naturelle de $f$ associée à la construction, aux variables et à $V$.

(vii) Observons d'abord que les clauses (iii) et (iv) commutent à la substitution de variables : si $v''$, $w''$ (et $y''$ pour une récurrence) sont des variables distinctes qui ne sont pas quantifiées dans la formule obtenue, la substituer à $v$, $w$ (et $y$) revient à appliquer la même clause aux formules composantes où l'on a substitué $v''$ à $v$, avec les variables $w''$ (et $y''$), puisque ces variables ne rencontrent aucun quantificateur. Une formule ainsi substituée est encore une définition fonctionnelle : elle est dans $\mathcal S$ par (i), (b) et (c) passent par le point (iv) de Récurrence dans PA, et (a) par le lemme de substitution.

On raisonne par récurrence sur la longueur de la construction, l'énoncé portant sur tous les choix de variables à la fois. Pour une fonction de base, les deux formules substituées sont la même formule, par exemple $w'' = v''_k$. Pour une composition, $\varphi[v'', w''/v, w]$ est $\exists z_1 \cdots \exists z_m\, (\varphi_1[v''/v] \wedge \cdots \wedge \varphi_f[w''/w])$, et de même pour $\varphi'$, avec des variables $z'_j$. Soit $\zeta_1, \dots, \zeta_m$ des variables distinctes qui ne figurent dans aucune des deux formules. Le renommage du point (iii) de Calcul à variables libres, appliqué dans les deux sens comme au point (ii) de Collection et forme Σ₁, et la monotonie de Récurrence dans PA, (ii), remplacent les $z_j$ par les $\zeta_j$ ; l'hypothèse de récurrence, appliquée aux $g_j$ avec les variables $v'', \zeta_j$ et à $f$ avec les variables $\zeta, w''$, et la monotonie remplacent chaque $\varphi_j[v'', \zeta_j/v, z_j]$ par $\varphi'_j[v'', \zeta_j/v', z'_j]$ et $\varphi_f[\zeta, w''/z, w]$ par $\varphi'_f[\zeta, w''/z', w']$ ; un dernier renommage ramène les $\zeta_j$ aux $z'_j$. Pour une récurrence primitive, notons $H''$ et $\psi$ les deux formules substituées, écrites avec $v''$, $y''$, $w''$. Par l'observation initiale, $H''$ est la formule de (iv) construite sur $\varphi_f[v''/v]$ et $\varphi_g[v''/v]$, et $\psi$ celle construite sur $\varphi'_f[v''/v']$ et $\varphi'_g[v''/v']$ ; le point (iv), appliqué à $\psi$, donne ses deux équations avec ces dernières formules, et l'hypothèse de récurrence, appliquée à $f$ et à $g$ avec les variables $v'', w''$ et $v'', y'', u, w''$, où $u$ est une variable nouvelle, les transforme en les équations écrites avec $\varphi_f[v''/v]$ et $\varphi_g[v''/v]$. Le point (v), appliqué à $H''$ et à $\psi$, conclut. Le cas sans paramètre est le même.