Substitution lettre à lettre dans un code variable, dans l'arithmétique de Peano

On écrit avec les valeurs, au sens de Termes fonctionnels, et l'on emploie les règles des quantifications bornées strictes de la preuve de Deuxième condition (D2).

(i) Sous l'hypothèse $\hat C(N, j, \underline k)$, la lecture donne $(N)^j = \underline k$. Réciproquement, raisonnons sous les hypothèses $\mathrm{Nq}_k(N)$, $j < \mathrm{lg}(N)$ et $(N)^j = \underline k$. Le calcul clos $\underline 8 \leqslant \underline k$ et le remplacement donnent $\underline 8 \leqslant (N)^j$. Par l'instance de $\mathrm Q_3$, $j = 0$ ou $j = S\,j'$ ; dans le second cas, $j' < j$, donc $j' < \mathrm{lg}(N)$, et $S\,j' < \mathrm{lg}(N)$, de sorte que $\mathrm{Nq}_k(N)$, instanciée par $j'$, donne $\neg((N)^{j'} = \underline 3 \wedge (N)^{S\,j'} = \underline k)$, donc $\neg((N)^{j'} = \underline 3)$ puisque $(N)^{S\,j'} = (N)^j = \underline k$ ; comme $S\,j' \mathbin{\dot{-}} S\,0 = j'$ (Fonctions usuelles dans PA, (iii)), on obtient $\widehat{\mathrm{Oc}}(N, j)$. Pour $\neg\widehat{\mathrm{Li}}(N, j)$, il suffit, par l'élimination des quantifications bornées strictes, de tirer une contradiction des hypothèses $i < j$, $(N)^i = \underline 3$ et $(N)^{S\,i} = (N)^j$, les clauses $\Psi'$ étant affaiblies. Or $i < j$ s'écrit $S\,i \leqslant j$, d'où $S\,i < \mathrm{lg}(N)$ et $i < \mathrm{lg}(N)$ par la transitivité mixte de la preuve de Facteurs dans PA ; l'instance de $\mathrm{Nq}_k(N)$ en $i$ contredit $(N)^i = \underline 3$ et $(N)^{S\,i} = \underline k$. La lecture donne $\hat C(N, j, \underline k)$.

(ii) Le point (ii) de Longueur dans PA donne $\mathrm{lg}(0) = 0$, et les équations du balayage donnent $\mathrm{Sb}(0, T, \underline k) = W(0, T, \underline k, 0) = 0$. Soit $N' = \mathrm{aj}(N, v)$ et $l$ la valeur de $\mathrm{lg}(N)$, de sorte que $\mathrm{lg}(N') = S\,l$ ; raisonnons sous l'hypothèse $\mathrm{Nq}_k(N')$. Comme $N' = \mathrm{conc}(N, \mathrm{aj}(0, v))$, par les égalités $\mathrm{conc}(N, \mathrm{aj}(0, v)) = \mathrm{aj}(\mathrm{conc}(N, 0), v)$ et $\mathrm{conc}(N, 0) = N$ du point (iv) de Concaténation dans PA, le point (i) de Propriétés locales des lettres donne $\mathrm{Nq}_k(N)$.

Montrons, par récurrence sur $j$, la formule $j \leqslant l \to W(N', T, \underline k, j) = W(N, T, \underline k, j)$, où $j$ n'est pas libre dans l'hypothèse $\mathrm{Nq}_k(N')$. Pour $0$, les deux membres valent $0$. Sous l'hypothèse de récurrence et sous $S\,j \leqslant l$, c'est-à-dire $j < l$, on a $j \leqslant l$ (Ordre dans PA, (v)), et l'hypothèse de récurrence donne une valeur commune $u$ des deux balayages au rang $j$. Comme $j < l < S\,l$, le point (i), appliqué à $N'$ et à $N$, et l'égalité $(N')^j = (N)^j$ du point (iii) de Longueur dans PA donnent $\hat C(N', j, \underline k) \leftrightarrow \hat C(N, j, \underline k)$. Si $\hat C(N, j, \underline k)$, les équations du balayage donnent la valeur $\mathrm{conc}(u, T)$ aux deux balayages au rang $S\,j$ ; sinon, elles donnent $\mathrm{aj}(u, (N')^j) = \mathrm{aj}(u, (N)^j)$. La récurrence (Récurrence dans PA, (iii)), puis la substitution de $l$ à $j$, donnent $W(N', T, \underline k, l) = W(N, T, \underline k, l) = \mathrm{Sb}(N, T, \underline k)$.

Enfin $\mathrm{Sb}(N', T, \underline k) = W(N', T, \underline k, S\,l)$. Comme $(N')^l = v$ et $l < S\,l$, le point (i) donne $\hat C(N', l, \underline k) \leftrightarrow v = \underline k$, et les équations du balayage, au rang $l$, donnent $\mathrm{conc}(\mathrm{Sb}(N, T, \underline k), T)$ si $v = \underline k$, et $\mathrm{aj}(\mathrm{Sb}(N, T, \underline k), v)$ sinon.

(iii) Appliquons la récurrence sur la longueur (Facteurs dans PA, (i)) à la formule $\mathrm{Nq}_k(\mathrm{conc}(M, N)) \to \mathrm{Sb}(\mathrm{conc}(M, N), T, \underline k) = \mathrm{conc}(\mathrm{Sb}(M, T, \underline k), \mathrm{Sb}(N, T, \underline k))$, avec la variable $N$ et une variable nouvelle $v$. Pour $N = 0$, $\mathrm{conc}(M, 0) = M$ et $\mathrm{Sb}(0, T, \underline k) = 0$, et la conclusion est $\mathrm{Sb}(M, T, \underline k) = \mathrm{conc}(\mathrm{Sb}(M, T, \underline k), 0)$, par le point (iv) de Concaténation dans PA. Pour le pas, raisonnons sous l'hypothèse de récurrence et sous $\mathrm{Nq}_k(\mathrm{conc}(M, \mathrm{aj}(N, v)))$. Par le même point (iv), $\mathrm{conc}(M, \mathrm{aj}(N, v)) = \mathrm{aj}(\mathrm{conc}(M, N), v)$, et le point (i) de Propriétés locales des lettres, appliqué comme dans la preuve de (ii), donne $\mathrm{Nq}_k(\mathrm{conc}(M, N))$, puis, avec la règle des suffixes, $\mathrm{Nq}_k(\mathrm{aj}(N, v))$. L'hypothèse de récurrence donne $\mathrm{Sb}(\mathrm{conc}(M, N), T, \underline k) = \mathrm{conc}(S_M, S_N)$, où $S_M$ et $S_N$ sont les valeurs de $\mathrm{Sb}(M, T, \underline k)$ et de $\mathrm{Sb}(N, T, \underline k)$. Si $v = \underline k$, (ii), appliqué à $\mathrm{aj}(\mathrm{conc}(M, N), v)$, puis l'associativité (Facteurs dans PA, (ii)) et (ii) appliqué à $\mathrm{aj}(N, v)$, donnent $$\begin{aligned} &\mathrm{Sb}(\mathrm{conc}(M, \mathrm{aj}(N, v)), T, \underline k) \\ &\quad = \mathrm{conc}(\mathrm{conc}(S_M, S_N), T) \\ &\quad = \mathrm{conc}(S_M, \mathrm{conc}(S_N, T)) \\ &\quad = \mathrm{conc}\big(S_M, \mathrm{Sb}(\mathrm{aj}(N, v), T, \underline k)\big). \end{aligned}$$ Si $\neg(v = \underline k)$, on obtient de même $\mathrm{aj}(\mathrm{conc}(S_M, S_N), v) = \mathrm{conc}(S_M, \mathrm{aj}(S_N, v))$, par le point (iv) de Concaténation dans PA, et (ii) conclut.

Pour l'identité, appliquons la même récurrence à la formule $\mathrm{Ab}_k(N) \to \mathrm{Sb}(N, T, \underline k) = N$. Le cas $0$ est (ii). Sous l'hypothèse $\mathrm{Ab}_k(\mathrm{aj}(N, v))$, le point (i) de Propriétés locales des lettres donne $\mathrm{Ab}_k(N)$, $\neg(v = \underline k)$ et $\mathrm{Nq}_k(\mathrm{aj}(N, v))$ ; l'hypothèse de récurrence et (ii) donnent $\mathrm{Sb}(\mathrm{aj}(N, v), T, \underline k) = \mathrm{aj}(N, v)$.

(iv) Il suffit de traiter une variable $T$, prise hors des $\tau_i$, à la place de $\tau$, puis de substituer $\tau$ par le point (ii) (b) de Termes fonctionnels, $T$ n'étant libre dans aucune hypothèse. Soit $G = G_{\bar x}(w) = (g_0, \dots, g_{m-1})$, $G'$ le gabarit $G_{\bar x, x}(w)$, qui s'obtient en remplaçant chaque entier $k$ de $G$ par $\diamond_{r+1}$, et, pour $j \leqslant m$, $P_j = \llbracket (g_0, \dots, g_{j-1}) \rrbracket(\bar\tau)$ et $P'_j = \llbracket (g'_0, \dots, g'_{j-1}) \rrbracket(\bar\tau, T)$. Raisonnons sous les hypothèses $\mathrm{Ch}(\tau_i)$. Le point (iii) de Propriétés locales des lettres, où $a_k$ n'est pas quantifiée dans $w$, donne $\mathrm{Bl}_k(P_m)$, donc $\mathrm{Nq}_k(P_m)$. Par le point (i) de Gabarits à plusieurs places, pour $j < m$, $P_m = \mathrm{conc}(P_{j+1}, \llbracket (g_{j+1}, \dots, g_{m-1}) \rrbracket(\bar\tau))$ et $P_{j+1} = \mathrm{conc}(P_j, \llbracket (g_j) \rrbracket(\bar\tau))$. La règle des préfixes, appliquée à la première égalité, donne $\mathrm{Nq}_k(P_{j+1})$ ; la règle des suffixes, appliquée à la seconde, donne $\mathrm{Nq}_k(\llbracket (g_j) \rrbracket(\bar\tau))$.

Montrons $\mathrm{Sb}(P_j, T, \underline k) = P'_j$ par récurrence sur $j$, en métathéorie. Pour $j = 0$, c'est (ii). Pour le pas, (iii) donne $\mathrm{Sb}(P_{j+1}, T, \underline k) = \mathrm{conc}(P'_j, \mathrm{Sb}(\llbracket (g_j) \rrbracket(\bar\tau), T, \underline k))$, et il reste à calculer le dernier terme. Si $g_j = \diamond_i$, c'est $\mathrm{Sb}(\tau_i, T, \underline k) = \tau_i$, par l'identité de (iii) et $\mathrm{Ab}_k(\tau_i)$ (Propriétés locales des lettres, (ii)). Si $g_j$ est un entier $c \neq k$, c'est $\mathrm{Sb}(\mathrm{aj}(0, \underline c), T, \underline k) = \mathrm{aj}(0, \underline c)$, par (ii) et le calcul clos $\neg(\underline c = \underline k)$. Si $g_j = k$, c'est $\mathrm{conc}(0, T) = T$, par (ii) et le point (iv) de Concaténation dans PA. Dans les trois cas, le dernier terme est $\llbracket (g'_j) \rrbracket(\bar\tau, T)$, et (i) de Gabarits à plusieurs places donne $P'_{j+1}$. Pour $j = m$, c'est l'égalité annoncée. Les cas particuliers s'en déduisent par $\mathrm{Ch}(\mathrm{num}(y_i))$ (Propriétés locales des lettres, (ii)) ; si $x$ ne figure pas dans $w$, $G'$ est $G$, et les deux codes sont le même terme fonctionnel.