La récurrence de valeurs dans l'arithmétique de Peano

(i) Par le point (iv) de Fonctions p.r. dans PA, $F(x, 0) = w$ équivaut à $(Z \circ P^p_1)(x) = w$, ou à $w = 0$ sans paramètre, donc à $w = 0$. Sous l'hypothèse $F(x, n) = u$, la seconde équation du même point et le point (ii) (d) de Termes fonctionnels ramènent $F(x, S\,n) = w$ à $\mathrm{aj}(u, G(x, n, u)) = w$. Le même point (ii) (d), appliqué à la composée $f$, donne $f(x, n) = G(x, n, F(x, n))$, c'est-à-dire $f(x, n) = G(x, n, u)$ sous l'hypothèse, et le remplacement (Termes fonctionnels, (ii) (c)) donne $F(x, S\,n) = \mathrm{aj}(u, f(x, n))$. Écrite avec la valeur $u$, c'est la deuxième équation.

(ii) Soit $\theta$ la conjonction de $\mathrm{lg}(F(x, n)) = n$ et de $\forall m < n\ (F(x, n))^m = f(x, m)$ ; montrons-la par récurrence sur $n$, avec les paramètres $x$. Pour $0$ : $\mathrm{lg}(0) = 0$ par le point (ii) de Longueur dans PA, et la clause $\forall m < 0$ est démontrable (Modules de Gödel, (i) (a)). Pour le pas, écrivons avec la valeur $u$ de $F(x, n)$, de sorte que $F(x, S\,n) = \mathrm{aj}(u, f(x, n))$. Le point (ii) de Longueur dans PA et l'hypothèse de récurrence donnent $\mathrm{lg}(F(x, S\,n)) = S\,\mathrm{lg}(u) = S\,n$. Par le point (i) (c) de Modules de Gödel, la clause pour $S\,n$ équivaut à celle pour $n$, jointe à $(F(x, S\,n))^n = f(x, n)$. Pour $m < n$, c'est-à-dire $m < \mathrm{lg}(u)$, le point (iii) de Longueur dans PA donne $(\mathrm{aj}(u, f(x, n)))^m = (u)^m$, qui vaut $f(x, m)$ par l'hypothèse de récurrence ; et, comme $n = \mathrm{lg}(u)$, le même point donne $(\mathrm{aj}(u, f(x, n)))^n = f(x, n)$.

(iii) Sous les deux hypothèses, (ii) donne $\mathrm{lg}(F(x, n)) = n = \mathrm{lg}(h)$ et, pour $m < n$, $(F(x, n))^m = f(x, m) = (h)^m$ ; l'extensionnalité (Longueur dans PA, (iv)) donne $h = F(x, n)$, et (i) et le remplacement donnent $f(x, n) = G(x, n, h)$.

(iv) La construction de $\chi_R = f$ est la composée $\chi_Q \circ (P^{p+1}_1, \dots, P^{p+1}_{p+1}, F)$ : c'est celle de la relation $Q(x, n, F(x, n))$, obtenue par substitution. Le point (ii) (d) de Termes fonctionnels donne donc $\hat R(x, n) \leftrightarrow \hat Q(x, n, F(x, n))$, les projections étant données par les termes $x_k$ et $n$. Pour $m < n$, (ii) donne $(F(x, n))^m = f(x, m)$, et le point (i) de Relations p.r. dans PA, appliqué à $R$ avec les termes $x$ et $m$, donne $\neg(f(x, m) = 0) \leftrightarrow \hat R(x, m)$ ; le remplacement conclut. Enfin, si $\chi_Q$ est booléenne, la valeur $f(x, n) = \chi_Q(x, n, F(x, n))$ est $0$ ou $S\,0$, par l'instance de $\chi_Q(x, n, z) = w \to (w = 0 \vee w = S\,0)$ obtenue avec la valeur $z$ de $F(x, n)$.