Concaténation des codes dans l'arithmétique de Peano

Il suffit de traiter des variables, et l'on raisonne par chaînes d'égalités entre termes fonctionnels.

(i) Longueur. Récurrence sur $t$, avec les paramètres $M$ et $N$ : $\mathrm{lg}(C(M, N, 0)) = \mathrm{lg}(M) = \mathrm{lg}(M) + 0$ par $\mathrm Q_4$, et, par le point (ii) de Longueur dans PA et $\mathrm Q_5$, $$\begin{aligned} \mathrm{lg}(C(M, N, S\,t)) &= S\,\mathrm{lg}(C(M, N, t)) \\ &= S(\mathrm{lg}(M) + t) \\ &= \mathrm{lg}(M) + S\,t. \end{aligned}$$

Premiers termes. Récurrence sur $t$ de la formule $j < \mathrm{lg}(M) \to (C(M, N, t))^j = (M)^j$, avec les paramètres $M$, $N$, $j$. Pour $0$, c'est $C(M, N, 0) = M$. Pour le pas, sous $j < \mathrm{lg}(M)$, on a $\mathrm{lg}(M) \leqslant \mathrm{lg}(M) + t = \mathrm{lg}(C(M, N, t))$, donc $j < \mathrm{lg}(C(M, N, t))$, et le point (iii) de Longueur dans PA donne $(C(M, N, S\,t))^j = (C(M, N, t))^j$, qui vaut $(M)^j$ par l'hypothèse de récurrence.

Termes ajoutés. Récurrence sur $t$ de la formule $s < t \to (C(M, N, t))^{\mathrm{lg}(M) + s} = (N)^s$, avec les paramètres $M$, $N$, $s$. Pour $0$, $s < 0$ est exclu (Ordre dans PA, (v)). Pour le pas, sous $s < S\,t$, c'est-à-dire $s \leqslant t$, le point (v) du même nœud donne $s < t$ ou $s = t$. Si $s = t$, le rang $\mathrm{lg}(M) + t$ est $\mathrm{lg}(C(M, N, t))$, et le point (iii) de Longueur dans PA donne $(C(M, N, S\,t))^{\mathrm{lg}(M) + t} = (N)^t$. Si $s < t$, la compatibilité (Ordre dans PA, (vi)) donne $\mathrm{lg}(M) + s < \mathrm{lg}(M) + t$, puisque $S(\mathrm{lg}(M) + s) = \mathrm{lg}(M) + S\,s$, et le même point (iii) et l'hypothèse de récurrence donnent $(C(M, N, S\,t))^{\mathrm{lg}(M) + s} = (C(M, N, t))^{\mathrm{lg}(M) + s} = (N)^s$.

(ii) C'est (i), où l'on substitue le terme fonctionnel $\mathrm{lg}(N)$ à $t$, par le point (ii) (b) de Termes fonctionnels, avec $\mathrm{conc}(M, N) = C(M, N, \mathrm{lg}(N))$.

(iii) Par l'ordre total (Ordre dans PA, (iv) et (v)), $j < a$ ou $a \leqslant j$. Dans le second cas, l'élimination fournit $s$ tel que $s + a = j$, d'où $j = a + s$ par la commutativité ; sous l'hypothèse $j < a + b$, on a $S(a + s) \leqslant a + b$, c'est-à-dire $a + S\,s \leqslant a + b$, et la compatibilité donne $S\,s \leqslant b$, c'est-à-dire $s < b$. L'introduction de l'existentiel conclut.

(iv) On applique l'extensionnalité (Longueur dans PA, (iv)), avec le point (i) (a) de Modules de Gödel pour la clause $\forall j$. Pour $\mathrm{conc}(M, 0)$ : sa longueur est $\mathrm{lg}(M) + 0 = \mathrm{lg}(M)$, et ses termes de rang $j < \mathrm{lg}(M)$ sont ceux de $M$, par (ii). Pour $\mathrm{conc}(0, N)$ : sa longueur est $0 + \mathrm{lg}(N) = \mathrm{lg}(N)$, et, pour $s < \mathrm{lg}(N)$, son terme de rang $0 + s = s$ est $(N)^s$, par (ii) et le point (i) de Lois de + et ×.

Pour la dernière égalité, notons $L = \mathrm{conc}(M, \mathrm{aj}(N, v))$ et $L' = \mathrm{aj}(\mathrm{conc}(M, N), v)$, écrites avec leurs valeurs, ainsi que $m = \mathrm{lg}(M)$ et $n = \mathrm{lg}(N)$. Par (ii) et le point (ii) de Longueur dans PA, $\mathrm{lg}(L) = m + S\,n = S(m + n) = \mathrm{lg}(L')$. Soit $j < S(m + n)$ ; par (iii), $j < m$, ou bien $j = m + s$ avec $s < S\,n$, c'est-à-dire $s < n$ ou $s = n$. Si $j < m$, on a $j < m + n$, et (ii) et le point (iii) de Longueur dans PA donnent $(L)^j = (M)^j = (\mathrm{conc}(M, N))^j = (L')^j$. Si $j = m + s$ avec $s < n$, ils donnent de même $(L)^j = (\mathrm{aj}(N, v))^s = (N)^s = (\mathrm{conc}(M, N))^{m + s} = (L')^j$. Si $j = m + n$, ils donnent $(L)^j = (\mathrm{aj}(N, v))^n = v$, et, comme $m + n = \mathrm{lg}(\mathrm{conc}(M, N))$, $(L')^j = v$. L'extensionnalité conclut.