Ajout d'un terme, début et dernier terme d'un code dans l'arithmétique de Peano

Comme au nœud Puissances de 2 dans PA, il suffit de traiter des variables, et l'on raisonne par chaînes d'égalités entre termes fonctionnels. Pour une minimisation bornée, on emploie la caractérisation du point (vi) de Relations p.r. dans PA, avec la borne substituée par le point (ii) (b) de Termes fonctionnels : pour établir $\mu(v, y) = w$, il suffit d'établir son premier cas, $w < y$, $\hat R(v, w)$ et $\forall z < w\ \neg\hat R(v, z)$. Pour la borne stricte $\exists z < t$, on emploie le point (i) de Modules de Gödel : si $u < t$ et $\varphi[u/z]$, alors $\exists z < t\ \varphi$, par (b), appliqué à $\neg\varphi$, et la contraposition.

(i) Divisibilité. Par les points (ii) à (iv) de Relations p.r. dans PA et le point (ii) (d) de Termes fonctionnels, avec $\mathrm{mul}(d, k) = d \times k$, on a $\vdash_{\mathsf{PA}} d \mathrel{\hat|} x \leftrightarrow \exists k < S\,x\ (d \times k = x)$. Si $\exists k < S\,x\ (d \times k = x)$, raisonnons par l'absurde sous l'hypothèse $\forall k\, \neg(k \times d = x)$ : sous $k < S\,x$, l'axiome (2) et la commutativité donnent $\neg(d \times k = x)$, et le point (i) (a) de Modules de Gödel donne $\forall k < S\,x\ \neg(d \times k = x)$, contradiction ; donc $\exists k\, (k \times d = x)$, qui est $d \mid x$. Réciproquement, sous l'hypothèse $c \times d = x$, obtenue par élimination : si $d = 0$, alors $x = c \times 0 = 0$, et le terme $0$ convient, puisque $0 < S\,x$ et $d \times 0 = 0 = x$ ; sinon, le point (vi) de Ordre dans PA donne $c \leqslant c \times d = x$, donc $c < S\,x$, et $d \times c = x$, et le terme $c$ convient.

Quotient. La relation minimisée a pour formule naturelle $x < d \times S\,z$, par les points (ii) et (iii) de Relations p.r. dans PA. Sous les hypothèses $\neg(d = 0)$, $g \times d + r = x$ et $r < d$, établissons le premier cas pour $w = g$ et la borne $S\,x$. D'abord $g \leqslant g \times d \leqslant g \times d + r = x$, donc $g < S\,x$. Ensuite $d \times S\,g = g \times d + d$ par $\mathrm Q_7$ et la commutativité, et $S\,r \leqslant d$ donne $S(g \times d + r) = g \times d + S\,r \leqslant g \times d + d$, par $\mathrm Q_5$ et la compatibilité (Ordre dans PA, (vi)) : c'est $x < d \times S\,g$. Enfin, sous $z < g$, c'est-à-dire $S\,z \leqslant g$, la compatibilité avec la multiplication donne $d \times S\,z \leqslant d \times g \leqslant x$, ce qui exclut $x < d \times S\,z$ par le dernier point de (v) du même nœud ; le point (i) (a) de Modules de Gödel donne $\forall z < g\ \neg(x < d \times S\,z)$. Ainsi $q(x, d) = g$.

(ii) Début. Par le point (iv) de Fonctions p.r. dans PA, sans paramètre, $p_0 = w$ équivaut à $w = S\,S\,0$, donc $\vdash_{\mathsf{PA}} \mathrm{pw}(p_0, S\,z) = 2^{S\,z}$. Par le point (iii) de Relations p.r. dans PA et (i), la relation minimisée dans $\mathrm{dbt}(N) = \mu k < N\ \neg(\cdots)$ a pour formule naturelle, en $(N, 0, z)$, une formule équivalente à $\neg(2^{S\,z} \mid N)$. Soit $N = 2^n \times \mathrm O(k)$ ; établissons le premier cas pour $w = n$ et la borne $N$.

Par le point (ii) de Puissances de 2 dans PA et le point (vi) de Ordre dans PA, avec $\neg(\mathrm O(k) = 0)$ par $\mathrm Q_1$, on a $n < 2^n \leqslant N$, donc $n < N$. Ensuite, sous l'hypothèse $c \times 2^{S\,n} = N$, on a $c \times 2^{S\,n} = c \times (2^n \times S\,S\,0) = (c + c) \times 2^n$ et $N = \mathrm O(k) \times 2^n$ ; comme $2^n$ n'est pas nul, l'instance de $\mathrm Q_3$ l'écrit $S\,s$, et la simplification du point (iv) de Lois de + et × donne $c + c = \mathrm O(k)$, ce qu'exclut la parité (Puissances de 2 dans PA, (iii)) : donc $\neg(2^{S\,n} \mid N)$. Enfin, sous l'hypothèse $z < n$, c'est-à-dire $S\,z \leqslant n$, l'élimination fournit $a$ tel que $a + S\,z = n$ ; alors $2^n = 2^a \times 2^{S\,z}$, et $N = (2^a \times \mathrm O(k)) \times 2^{S\,z}$ donne $2^{S\,z} \mid N$, avec ce témoin ; le point (i) (a) de Modules de Gödel donne la clause $\forall z < n$. Ainsi $\mathrm{dbt}(N) = n$.

Pour $N = 0$, le second cas de la caractérisation, $w = 0$ avec la clause vide $\forall z < 0$ (Modules de Gödel, (i) (a)), donne $\mathrm{dbt}(0) = 0$.

Dernier terme. Soit encore $N = 2^n \times \mathrm O(k)$, de sorte que $\mathrm{dbt}(N) = n$. Comme $\mathrm O(k) \times 2^n + 0 = N$, $\neg(2^n = 0)$ et $0 < 2^n$, (i) donne $q(N, 2^n) = \mathrm O(k)$. Par le point (iii) de Fonctions usuelles dans PA, avec $S\,0 \leqslant \mathrm O(k)$ et $(k + k) + S\,0 = \mathrm O(k)$, on a $\mathrm O(k) \mathbin{\dot{-}} S\,0 = k + k$. Enfin $k \times S\,S\,0 + 0 = k + k$ et $0 < S\,S\,0$, et (i) donne $q(k + k, S\,S\,0) = k$. La chaîne $\mathrm{dr}(N) = q(\mathrm O(k) \mathbin{\dot{-}} S\,0, S\,S\,0) = q(k + k, S\,S\,0) = k$ conclut.

(iii) Par le point (iv) de Lois de + et ×, $2^h \times \mathrm O(v) = 0$ donnerait $2^h = 0$ ou $\mathrm O(v) = 0$, que le point (ii) de Puissances de 2 dans PA et $\mathrm Q_1$ excluent. Ensuite $h < 2^h \leqslant 2^h \times \mathrm O(v)$, comme en (ii). Les deux égalités suivantes sont (ii), appliqué à $n = h$ et $k = v$ ; l'injectivité en découle, en appliquant $\mathrm{dbt}$ et $\mathrm{dr}$ aux deux membres par le point (ii) (c) de Termes fonctionnels. Enfin, si $\neg(N = 0)$, la décomposition (Puissances de 2 dans PA, (iv)) et l'élimination fournissent $n$ et $k$ tels que $N = 2^n \times \mathrm O(k)$ ; (ii) donne $\mathrm{dbt}(N) = n$ et $\mathrm{dr}(N) = k$, d'où $N = \mathrm{aj}(\mathrm{dbt}(N), \mathrm{dr}(N))$, et $\mathrm{dbt}(N) = n < N$ comme ci-dessus.