Substitution et substituabilité

(i) On parcourt les lettres de $\varphi$ de gauche à droite. Par récurrence primitive sur $j$, posons $W(N, T, k, 0) = 0$ et $$\begin{aligned} &W(N, T, k, j + 1) \\ &\ = \begin{cases} \mathrm{conc}\big(W(N, T, k, j), T\big) & \text{si } C, \\ \mathrm{aj}\big(W(N, T, k, j), (N)^j\big) & \text{sinon,} \end{cases} \end{aligned}$$ où $C$ est la condition $\mathrm{Lib}(N, j) \wedge (N)^j = k$. C'est une récurrence primitive dont l'étape est une définition par cas (Clôture, (ii)), et l'on pose $\mathrm{Sb}(N, T, k) = W(N, T, k, \mathrm{lg}(N))$.

Par récurrence sur $j$, $W(N, T, k, j)$ code le mot obtenu à partir des $j$ premières lettres de $\varphi$ en remplaçant par $t$ chacune de celles qui sont des occurrences libres de $x$, et en gardant les autres. Pour $j = \mathrm{lg}(N)$, c'est $\varphi[t/x]$.

(ii) La définition se traduit, avec $l = \mathrm{lg}(N)$, par : pour tout $j < l$, si $\mathrm{Lib}(N, j)$ et $(N)^j = k$, alors il n'existe pas $i < j$ et $l' < l + 1$ tels que $(N)^i = 3$, que la lettre $(N)^{i+1}$ figure dans $t$, c'est-à-dire $$\exists m < \mathrm{lg}(T)\ \ (T)^m = (N)^{i+1},$$ que $i + 2 \leqslant j < l'$, et que $\mathrm{Fm}(\mathrm{sm}(N, i + 2, l'))$. Une occurrence libre n'est jamais la variable d'un bloc, et elle n'est pas la lettre $\forall$ ; se trouver dans la sous-formule $\forall y\, \psi$, c'est donc se trouver dans $\psi$. La relation obtenue est primitive récursive par Variables libres et Clôture.

(iii) Remplacer des lettres d'un mot $w = w_1 w_2$ revient à remplacer celles de $w_1$, puis celles de $w_2$, et à concaténer. De plus, un rang de $w_2$ qui est une occurrence de variable dans $w$ en est encore une dans $w_2$ : la condition sur la lettre qui précède ne peut que s'affaiblir quand on retire $w_1$. On raisonne par récurrence sur la longueur, avec l'inversion de Termes et de Formules, (i).

Termes. Une variable devient $t$ ou reste elle-même, et $0$ reste $0$ ; ce sont des termes. Dans $S\, u$, $+\, u\, u'$ ou $\times\, u\, u'$, les rangs remplacés sont dans $u$ ou dans $u'$, et le résultat est $S$, $+$ ou $\times$ suivi des termes que donne l'hypothèse de récurrence : c'est un terme.

Formules. Dans ${=}\, u\, u'$, les rangs remplacés sont dans les termes $u$ et $u'$, et l'on conclut par le cas des termes. Dans $\neg\varphi$ et ${\to}\, \varphi\, \psi$, ils sont dans $\varphi$ ou $\psi$, et l'hypothèse de récurrence conclut. Dans $\forall y\, \varphi$, le rang $0$ porte la lettre $\forall$ et le rang $1$, qui suit $\forall$, n'est pas une occurrence : les rangs remplacés sont dans $\varphi$, et le résultat est $\forall y$ suivi d'une formule.

Enfin $\varphi[t/x]$ s'obtient en remplaçant les occurrences libres de $x$, qui sont des occurrences de $x$.