Récurrence sur la longueur, associativité de la concaténation et inégalités des facteurs dans l'arithmétique de Peano

On raisonne, comme aux nœuds du chapitre Suites codées dans PA, par chaînes d'égalités et d'inégalités entre termes fonctionnels, en écrivant avec les valeurs au sens de Termes fonctionnels ; pour (ii) à (iv), il suffit de traiter des variables distinctes, par le point (ii) (b) de ce nœud. On emploie la transitivité mixte : si $a < b$ et $b \leqslant c$, alors $a < c$, puisque $a < b$ est $S\,a \leqslant b$, par le point (iii) de Ordre dans PA, et de même si $a \leqslant b$ et $b < c$, puisque $S\,a \leqslant S\,b$ par le point (vi) du même nœud.

(i) Soit $t$ et $h$, $u$ des variables nouvelles, et $\theta$ la formule $\forall N\, \big(\mathrm{lg}(N) = t \to \varphi\big)$. Par le point (i) de Calcul à variables libres, l'hypothèse donne $\Gamma \vdash_{\mathsf{PA}} \varphi \to \varphi[\mathrm{aj}(N, v)/N]$ ; comme $N$ et $v$ ne sont libres dans aucune formule de $\Gamma$, le point (ii) (b) de Termes fonctionnels, appliqué à $N$ et au terme $h$, puis à $v$ et au terme $u$, donne $\Gamma \vdash_{\mathsf{PA}} \varphi[h/N] \to \varphi[\mathrm{aj}(h, u)/N]$, puisque $v$ ne figure pas dans $\varphi$ et que les occurrences libres de $N$ dans $\varphi[\mathrm{aj}(N, v)/N]$ sont exactement celles du terme $\mathrm{aj}(N, v)$.

Base. Sous l'hypothèse $\mathrm{lg}(N) = 0$, le point (ii) de Longueur dans PA donne $N = 0$, et le remplacement (Termes fonctionnels, (ii) (c)) tire $\varphi$ de $\varphi[0/N]$. Le théorème de la déduction et la généralisation en $N$, qui n'est libre dans aucune formule de $\Gamma$ (Récurrence dans PA, (i)), donnent $\Gamma \vdash_{\mathsf{PA}} \theta[0/t]$.

Pas. Raisonnons sous $\theta$, sous $\mathrm{lg}(N) = S\,t$ et sous les hypothèses $\mathrm{dbt}(N) = h$ et $\mathrm{dr}(N) = u$. Si $N$ était nul, on aurait $S\,t = \mathrm{lg}(0) = 0$, contrairement à $\mathrm Q_1$ ; le point (iii) de Ajout dans PA donne donc $N = \mathrm{aj}(h, u)$. Par le point (ii) de Longueur dans PA, $S\,t = \mathrm{lg}(\mathrm{aj}(h, u)) = S\,\mathrm{lg}(h)$, et $\mathrm Q_2$ donne $\mathrm{lg}(h) = t$. L'axiome (2), avec le terme $h$, qui est substituable puisqu'il est nouveau, donne $\varphi[h/N]$, puis la formule établie plus haut donne $\varphi[\mathrm{aj}(h, u)/N]$, et le remplacement, avec $N = \mathrm{aj}(h, u)$, donne $\varphi$. Le point (ii) (a) de Termes fonctionnels élimine les deux dernières hypothèses, puisque $h$ et $u$ ne figurent ni dans $\Gamma$, ni dans $\theta$, ni dans $\varphi$ ; le théorème de la déduction et la généralisation en $N$, qui n'est libre ni dans $\theta$ ni dans $\Gamma$, donnent $\Gamma \cup \{\theta\} \vdash_{\mathsf{PA}} \theta[S\,t/t]$.

La récurrence (Récurrence dans PA, (iii)), permise puisque $t$ n'est libre dans aucune formule de $\Gamma$, donne $\Gamma \vdash_{\mathsf{PA}} \theta$. L'axiome (2), avec le terme $N$, donne $\mathrm{lg}(N) = t \to \varphi$, et le point (ii) (b) de Termes fonctionnels, avec le terme fonctionnel $\mathrm{lg}(N)$ substitué à $t$, qui ne figure pas dans $\varphi$, donne $\mathrm{lg}(N) = \mathrm{lg}(N) \to \varphi$ ; le point (ii) (c) du même nœud conclut.

(ii) Appliquons (i) à la formule $\mathrm{conc}(M, \mathrm{conc}(N, P)) = \mathrm{conc}(\mathrm{conc}(M, N), P)$, avec la variable $P$ et une variable nouvelle $v$. Pour $P = 0$, les deux membres valent $\mathrm{conc}(M, N)$, par le point (iv) de Concaténation dans PA. Pour le pas, ce même point et l'hypothèse de récurrence donnent $$\begin{aligned} &\mathrm{conc}(M, \mathrm{conc}(N, \mathrm{aj}(P, v))) \\ &\quad = \mathrm{conc}(M, \mathrm{aj}(\mathrm{conc}(N, P), v)) \\ &\quad = \mathrm{aj}(\mathrm{conc}(M, \mathrm{conc}(N, P)), v) \\ &\quad = \mathrm{aj}(\mathrm{conc}(\mathrm{conc}(M, N), P), v) \\ &\quad = \mathrm{conc}(\mathrm{conc}(M, N), \mathrm{aj}(P, v)). \end{aligned}$$

(iii) Monotonie de l'ajout. Sous l'hypothèse $h \leqslant h'$, l'élimination fournit $a$ tel que $a + h = h'$. Par le point (ii) de Puissances de 2 dans PA, $2^{h'} = 2^a \times 2^h$ et $2^a$ n'est pas nul ; le point (vi) de Ordre dans PA et la commutativité donnent $2^h \leqslant 2^{h'}$, puis $2^h \times \mathrm O(v) \leqslant 2^{h'} \times \mathrm O(v)$, c'est-à-dire $\mathrm{aj}(h, v) \leqslant \mathrm{aj}(h', v)$, par l'égalité $\mathrm{aj}(h, v) = 2^h \times \mathrm O(v)$ de Ajout dans PA. Sous l'hypothèse $h < h'$, c'est-à-dire $S\,h \leqslant h'$, ce qui précède donne $\mathrm{aj}(S\,h, v) \leqslant \mathrm{aj}(h', v)$, et le point (i) de Puissances de 2 dans PA et la distributivité donnent $\mathrm{aj}(S\,h, v) = c + c$, où $c = \mathrm{aj}(h, v)$. Comme $c$ n'est pas nul (Ajout dans PA, (iii)), $S\,0 \leqslant c$, et la compatibilité donne $S\,c = c + S\,0 \leqslant c + c$ ; la transitivité donne $S\,c \leqslant \mathrm{aj}(h', v)$, c'est-à-dire $\mathrm{aj}(h, v) < \mathrm{aj}(h', v)$.

Premier facteur. Montrons $M \leqslant C(M, N, t)$ par récurrence sur $t$, avec les paramètres $M$ et $N$. Pour $0$, $C(M, N, 0) = M$. Pour le pas, $C(M, N, S\,t) = \mathrm{aj}(C(M, N, t), (N)^t)$, qui est strictement plus grand que $C(M, N, t)$ par le point (iii) de Ajout dans PA ; la transitivité mixte donne $M < C(M, N, S\,t)$, donc $M \leqslant C(M, N, S\,t)$ par le point (v) de Ordre dans PA. Le point (ii) (b) de Termes fonctionnels, avec $\mathrm{lg}(N)$ substitué à $t$, donne $M \leqslant \mathrm{conc}(M, N)$. Si $N$ n'est pas nul, $\mathrm{lg}(N)$ ne l'est pas (Longueur dans PA, (ii)), et l'instance de $\mathrm Q_3$ l'écrit $S\,t'$ ; alors $\mathrm{conc}(M, N) = C(M, N, S\,t')$ est strictement plus grand que $C(M, N, t')$, qui est au moins $M$, d'où $M < \mathrm{conc}(M, N)$.

Second facteur. Appliquons (i) à la formule $N \leqslant \mathrm{conc}(M, N)$, avec la variable $N$ et une variable nouvelle $v$. Pour $N = 0$, c'est $0 \leqslant \mathrm{conc}(M, 0)$ (Ordre dans PA, (i)). Pour le pas, sous l'hypothèse $N \leqslant \mathrm{conc}(M, N)$, la monotonie et le point (iv) de Concaténation dans PA donnent $\mathrm{aj}(N, v) \leqslant \mathrm{aj}(\mathrm{conc}(M, N), v) = \mathrm{conc}(M, \mathrm{aj}(N, v))$. Pour l'inégalité stricte, on applique (i) à la formule $N < \mathrm{conc}(M, N)$, sous l'hypothèse $\neg(M = 0)$, dans laquelle ni $N$ ni $v$ ne figurent : pour $N = 0$, $0 < M = \mathrm{conc}(M, 0)$, par le point (v) de Ordre dans PA ; le pas est le même, avec la monotonie stricte. Le théorème de la déduction conclut.

(iv) Longueur et termes de $\sigma$. Récurrence sur $t$, avec les paramètres $N$ et $i$ : $\mathrm{lg}(\sigma(N, i, 0)) = \mathrm{lg}(0) = 0$, et $\mathrm{lg}(\sigma(N, i, S\,t)) = S\,\mathrm{lg}(\sigma(N, i, t)) = S\,t$, par le point (ii) de Longueur dans PA. Pour les termes, montrons $\forall s\, \big(s < t \to (\sigma(N, i, t))^s = (N)^{i + s}\big)$ par récurrence sur $t$. Pour $0$, $s < 0$ est exclu. Pour le pas, sous $s < S\,t$, c'est-à-dire $s \leqslant t$, on a $s < t$ ou $s = t$ (Ordre dans PA, (v)). Comme $\mathrm{lg}(\sigma(N, i, t)) = t$, le point (iii) de Longueur dans PA donne, si $s = t$, $(\sigma(N, i, S\,t))^t = (N)^{i + t}$, et, si $s < t$, $(\sigma(N, i, S\,t))^s = (\sigma(N, i, t))^s$, qui vaut $(N)^{i + s}$ par l'hypothèse de récurrence. On généralise en $s$, qui n'est libre dans aucune hypothèse.

Le mot entier. Par le point (iii) de Fonctions usuelles dans PA, avec $0 \leqslant \mathrm{lg}(N)$ et $\mathrm{lg}(N) + 0 = \mathrm{lg}(N)$, on a $\mathrm{lg}(N) \mathbin{\dot{-}} 0 = \mathrm{lg}(N)$, donc $\mathrm{sm}(N, 0, \mathrm{lg}(N)) = \sigma(N, 0, \mathrm{lg}(N))$. Sa longueur est $\mathrm{lg}(N)$, et, pour $s < \mathrm{lg}(N)$, son terme de rang $s$ est $(N)^{0 + s} = (N)^s$, par le point (i) de Lois de + et ×. L'extensionnalité (Longueur dans PA, (iv)), avec le point (i) (a) de Modules de Gödel pour la clause $\forall j$, conclut.

Un facteur. Soit $P = \mathrm{cc}(M, A, B)$, et écrivons avec les valeurs $m$ et $a$ de $\mathrm{lg}(M)$ et de $\mathrm{lg}(A)$. Le même point (iii), avec $m \leqslant m + a$ et $a + m = m + a$, donne $(m + a) \mathbin{\dot{-}} m = a$, donc $\mathrm{sm}(P, m, m + a) = \sigma(P, m, a)$, de longueur $a$. Pour $s < a$, son terme de rang $s$ est $(P)^{m + s}$ ; or $m + s < m + a$, par la compatibilité (Ordre dans PA, (vi)), et $m + a = \mathrm{lg}(\mathrm{conc}(M, A))$ par le point (ii) de Concaténation dans PA, qui donne alors $(P)^{m + s} = (\mathrm{conc}(M, A))^{m + s} = (A)^s$. L'extensionnalité donne $\mathrm{sm}(P, m, m + a) = A$. Enfin, par (iii), $A \leqslant \mathrm{conc}(M, A) \leqslant \mathrm{cc}(M, A, B)$, et la première inégalité est stricte si $M$ n'est pas nul.