Itérés, longueur, termes et extensionnalité des codes dans l'arithmétique de Peano

Comme aux nœuds précédents, il suffit de traiter des variables, et l'on raisonne par chaînes d'égalités entre termes fonctionnels.

(i) Première égalité. Récurrence sur $i$, avec le paramètre $N$. Pour $0$, $D(N, S\,0) = \mathrm{dbt}(D(N, 0)) = \mathrm{dbt}(N) = D(\mathrm{dbt}(N), 0)$. Pour le pas, sous l'hypothèse de récurrence, $D(N, S\,S\,i) = \mathrm{dbt}(D(N, S\,i)) = \mathrm{dbt}(D(\mathrm{dbt}(N), i)) = D(\mathrm{dbt}(N), S\,i)$.

Itérés de $0$ et de l'ajout. Par récurrence sur $i$, $D(0, 0) = 0$ et $D(0, S\,i) = \mathrm{dbt}(D(0, i)) = \mathrm{dbt}(0) = 0$ par le point (ii) de Ajout dans PA. Ensuite $D(\mathrm{aj}(h, v), S\,i) = D(\mathrm{dbt}(\mathrm{aj}(h, v)), i) = D(h, i)$, par la première égalité et le point (iii) du même nœud.

Décroissance. Récurrence sur $i$, avec le paramètre $N$. Pour $0$, $D(N, 0) + 0 = N$ et $N \leqslant N$. Pour le pas, écrivons avec la valeur $M$ de $D(N, i)$. Si $M = 0$, alors $D(N, S\,i) = \mathrm{dbt}(0) = 0$. Si $\neg(M = 0)$ et $M + i \leqslant N$, le point (iii) de Ajout dans PA donne $\mathrm{dbt}(M) < M$, c'est-à-dire $S\,\mathrm{dbt}(M) \leqslant M$ ; la compatibilité (Ordre dans PA, (vi)) et la transitivité donnent $S\,\mathrm{dbt}(M) + i \leqslant N$, et $\mathrm{dbt}(M) + S\,i = S(\mathrm{dbt}(M) + i) = S\,\mathrm{dbt}(M) + i$ par $\mathrm Q_5$ et le point (i) de Lois de + et × : c'est $D(N, S\,i) + S\,i \leqslant N$. Dans les deux cas, la disjonction vaut pour $S\,i$.

Annulation. Le point (ii) (b) de Termes fonctionnels, avec le terme $N$ substitué à $i$, donne $D(N, N) = 0 \vee D(N, N) + N \leqslant N$. Dans le second cas, $D(N, N) + N \leqslant 0 + N$, et la compatibilité donne $D(N, N) \leqslant 0$, puis $D(N, N) = 0$ par le point (ii) de Ordre dans PA.

(ii) Caractérisation. La relation minimisée a pour formule naturelle $D(N, i) = 0$, par les points (ii) et (iii) de Relations p.r. dans PA et le point (ii) (d) de Termes fonctionnels, puisque $Z \circ P^2_1$ prend la valeur $0$. Par le point (vi) de Relations p.r. dans PA, avec la borne $S\,N$, la formule $\mathrm{lg}(N) = w$ équivaut à la disjonction de $w < S\,N \wedge D(N, w) = 0 \wedge \forall z < w\ \neg(D(N, z) = 0)$ et de $w = S\,N \wedge \forall z < S\,N\ \neg(D(N, z) = 0)$. Le second cas est exclu : $N < S\,N$, et le point (i) (b) de Modules de Gödel, avec le terme $N$, donnerait $\neg(D(N, N) = 0)$, contraire à (i). Dans le premier cas, la condition $w < S\,N$ découle des deux autres : si l'on avait $N < w$, le même point, avec le terme $N$, donnerait $\neg(D(N, N) = 0)$ ; donc $\neg(N < w)$, et la trichotomie (Ordre dans PA, (v)) donne $w \leqslant N$, c'est-à-dire $w < S\,N$. On obtient l'équivalence annoncée, et, en passant, $\mathrm{lg}(N) \leqslant N$.

Valeurs. Pour $N = 0$, $D(0, 0) = 0$ et la clause $\forall z < 0$ est démontrable (Modules de Gödel, (i) (a)) : $\mathrm{lg}(0) = 0$. Soit $M = \mathrm{aj}(h, v)$, et écrivons avec la valeur $l$ de $\mathrm{lg}(h)$, de sorte que $D(h, l) = 0$ et $\forall z < l\ \neg(D(h, z) = 0)$. Par (i), $D(M, S\,l) = D(h, l) = 0$. Sous l'hypothèse $z < S\,l$, distinguons $z = 0$ et $z = S\,z'$, par l'instance de $\mathrm Q_3$ : dans le premier cas, $D(M, 0) = M$, qui n'est pas nul par le point (iii) de Ajout dans PA ; dans le second, $S\,z' < S\,l$ donne $S\,z' \leqslant l$, c'est-à-dire $z' < l$, et $D(M, S\,z') = D(h, z')$ n'est pas nul. Le point (i) (a) de Modules de Gödel donne $\forall z < S\,l\ \neg(D(M, z) = 0)$, et la caractérisation donne $\mathrm{lg}(M) = S\,l$. Enfin, si $\neg(N = 0)$, le point (iii) de Ajout dans PA donne $N = \mathrm{aj}(\mathrm{dbt}(N), \mathrm{dr}(N))$, donc $\mathrm{lg}(N) = S\,\mathrm{lg}(\mathrm{dbt}(N))$, qui n'est pas nul par $\mathrm Q_1$ ; la contraposition donne la dernière formule.

(iii) Soit $M = \mathrm{aj}(h, v)$, et $l$ la valeur de $\mathrm{lg}(h)$, de sorte que $\mathrm{lg}(M) = S\,l$ par (ii). Pour le rang $l$ : par le point (iii) de Fonctions usuelles dans PA, $S\,l \leqslant S\,l$ donne $S\,l \mathbin{\dot{-}} S\,l = 0$, et $(M)^l = \mathrm{dr}(D(M, 0)) = \mathrm{dr}(M) = v$. Pour un rang $j < l$, c'est-à-dire $S\,j \leqslant l$, l'élimination fournit $a$ tel que $a + S\,j = l$ ; le même point donne $l \mathbin{\dot{-}} S\,j = a$ et, puisque $S\,a + S\,j = S(a + S\,j) = S\,l$ et $S\,j \leqslant S\,l$, $S\,l \mathbin{\dot{-}} S\,j = S\,a$. Alors, par (i), $$\begin{aligned} (M)^j &= \mathrm{dr}(D(M, S\,a)) \\ &= \mathrm{dr}(D(h, a)) \\ &= \mathrm{dr}(D(h, l \mathbin{\dot{-}} S\,j)) = (h)^j. \end{aligned}$$

(iv) Soit $\theta$ la formule $\forall M\, \forall N\, \big((\mathrm{lg}(M) = l \wedge \mathrm{lg}(N) = l \wedge \forall j < l\ (M)^j = (N)^j) \to M = N\big)$, pour une variable $l$ nouvelle ; montrons-la par récurrence sur $l$. Pour $0$, la dernière formule de (ii) donne $M = 0$ et $N = 0$. Pour le pas, sous l'hypothèse $\theta$ et sous $\mathrm{lg}(M) = S\,l$, $\mathrm{lg}(N) = S\,l$ et $\forall j < S\,l\ (M)^j = (N)^j$ : comme $\mathrm{lg}(0) = 0$, ni $M$ ni $N$ n'est nul, et le point (iii) de Ajout dans PA donne $M = \mathrm{aj}(h, v)$ et $N = \mathrm{aj}(h', v')$, avec $h = \mathrm{dbt}(M)$, $v = \mathrm{dr}(M)$, et de même pour $N$, écrits avec leurs valeurs. Par (ii) et $\mathrm Q_2$, $\mathrm{lg}(h) = l = \mathrm{lg}(h')$. Sous l'hypothèse $j < l$, on a $j < S\,l$, et (iii) donne $(h)^j = (M)^j = (N)^j = (h')^j$ ; le point (i) (a) de Modules de Gödel donne $\forall j < l\ (h)^j = (h')^j$, et $\theta$, instanciée par $h$ et $h'$, donne $h = h'$. Comme $l < S\,l$, (iii) donne $v = (M)^l = (N)^l = v'$, et $M = \mathrm{aj}(h, v) = \mathrm{aj}(h', v') = N$. La généralisation en $M$ et $N$ donne $\theta[S\,l/l]$, et le point (iii) de Récurrence dans PA donne $\vdash_{\mathsf{PA}} \theta$. On instancie $\theta$ par $M$ et $N$, par l'axiome (2), puis $l$ par le terme fonctionnel $\mathrm{lg}(N)$, par le point (ii) (b) de Termes fonctionnels.