Substitution d'un terme dans un mot fixé, dépliée dans l'arithmétique de Peano

(i) Par récurrence sur la longueur de $H$, en métathéorie. Si $H$ est vide, $\llbracket G \rrbracket(\tau) = \mathrm{conc}(\llbracket G \rrbracket(\tau), 0)$ par le point (iv) de Concaténation dans PA. Si $H$ est $H'$ suivi de l'entier $c$, le même point et l'hypothèse de récurrence donnent $$\begin{aligned} &\llbracket GH \rrbracket(\tau) \\ &\ = \mathrm{aj}\big(\mathrm{conc}(\llbracket G \rrbracket(\tau), \llbracket H' \rrbracket(\tau)), \underline c\big) \\ &\ = \mathrm{conc}\big(\llbracket G \rrbracket(\tau), \mathrm{aj}(\llbracket H' \rrbracket(\tau), \underline c)\big). \end{aligned}$$ Si $H$ est $H'$ suivi de $\diamond$, l'associativité (Facteurs dans PA, (ii)) donne de même $\mathrm{conc}(\mathrm{conc}(\llbracket G \rrbracket(\tau), \llbracket H' \rrbracket(\tau)), \tau) = \mathrm{conc}(\llbracket G \rrbracket(\tau), \mathrm{conc}(\llbracket H' \rrbracket(\tau), \tau))$. Si $\diamond$ figure dans $G$, écrivons $G = G_1 \diamond G_2$ ; ce qui précède donne $\llbracket G \rrbracket(\tau) = \mathrm{cc}(\llbracket G_1 \rrbracket(\tau), \tau, \llbracket G_2 \rrbracket(\tau))$, qui est au moins $\tau$ par le point (iv) de Facteurs dans PA.

(ii) Soit $n = \ulcorner w \urcorner$ et $m$ la longueur de $w$, de sorte que $\vdash_{\mathsf{PA}} \mathrm{lg}(\underline n) = \underline m$ et $\vdash_{\mathsf{PA}} (\underline n)^{\underline j} = \underline{c_j}$ pour $j < m$, par le point (iv) de Termes fonctionnels. Pour $j \leqslant m$, notons $G_{<j}$ la suite des $j$ premiers termes de $G_k(w)$, et montrons, par récurrence sur $j$ en métathéorie, que $\vdash_{\mathsf{PA}} W(\underline n, T, \underline k, \underline j) = \llbracket G_{<j} \rrbracket(T)$ pour une variable $T$.

Par le point (iv) de Fonctions p.r. dans PA, comme au nœud Récurrence de valeurs dans PA, $W(N, T, k, 0) = w'$ équivaut à $w' = 0$, et, sous l'hypothèse $W(N, T, k, j) = u$, $W(N, T, k, S\,j) = w'$ équivaut à $g(N, T, k, j, u) = w'$. Pour $j = 0$, $\llbracket G_{<0} \rrbracket(T) = 0$. Pour $j < m$, la relation $C(n, j, k)$ est vraie ou fausse dans $\mathcal N$, et le point (iv) de Termes fonctionnels donne $\vdash_{\mathsf{PA}} \hat C(\underline n, \underline j, \underline k)$ ou $\vdash_{\mathsf{PA}} \neg\hat C(\underline n, \underline j, \underline k)$. Par le point (ii) (d) du même nœud, $\hat R_1(\underline n, T, \underline k, \underline j, u)$ équivaut à $\hat C(\underline n, \underline j, \underline k)$, et $\hat R_2$ à sa négation, par le point (iii) de Relations p.r. dans PA. Dans le premier cas, le point (v) du même nœud, permis par la booléennité, donne $g(\underline n, T, \underline k, \underline j, u) = \mathrm{conc}(u, T)$ ; écrit avec la valeur $u$ de $W(\underline n, T, \underline k, \underline j)$, qui est $\llbracket G_{<j} \rrbracket(T)$ par l'hypothèse de récurrence, cela donne $W(\underline n, T, \underline k, \underline{j + 1}) = \mathrm{conc}(\llbracket G_{<j} \rrbracket(T), T) = \llbracket G_{<j+1} \rrbracket(T)$, puisque le terme de rang $j$ du gabarit est $\diamond$. Dans le second cas, on obtient de même $\mathrm{aj}(\llbracket G_{<j} \rrbracket(T), (\underline n)^{\underline j})$, c'est-à-dire $\mathrm{aj}(\llbracket G_{<j} \rrbracket(T), \underline{c_j}) = \llbracket G_{<j+1} \rrbracket(T)$.

Par le point (ii) (d) de Termes fonctionnels, $\mathrm{Sb}(\underline n, T, \underline k) = W(\underline n, T, \underline k, \mathrm{lg}(\underline n))$, et le remplacement, avec $\mathrm{lg}(\underline n) = \underline m$, donne l'égalité pour $T$ ; le point (ii) (b) du même nœud la donne pour $\tau$, la variable $T$ n'étant libre dans aucune hypothèse. Si $x$ n'a pas d'occurrence libre dans $w$, le gabarit ne contient pas $\diamond$, et $\llbracket G_k(w) \rrbracket = \underline n$.

(iii) Par la définition des occurrences libres (Formules, variables libres), une occurrence de $x$ dans $\varphi$ est libre dans $\neg\varphi$ ou dans ${\to}\, \varphi\, \psi$ si et seulement si elle l'est dans $\varphi$, et de même pour $\psi$ : par le texte de Variables libres, les blocs $\forall$ et leurs portées sont ceux de la construction, c'est-à-dire, pour ces deux formules, ceux de $\varphi$ et de $\psi$. Dans $\forall z\, \varphi$, il s'y ajoute le bloc $\forall z$, de portée $\varphi$, qui ne lie pas $x$ ; dans $\forall x\, \varphi$, ce bloc lie toutes les occurrences de $x$, et la lettre de rang $1$ n'est pas une occurrence. Dans un terme ou dans ${=}\, t\, u$, il n'y a pas de bloc. Ainsi, en notant $(c)$ le gabarit réduit à l'entier $c$, $$\begin{aligned} G_k(\neg\varphi) &= (1)\, G_k(\varphi), \\ G_k({\to}\, \varphi\, \psi) &= (2)\, G_k(\varphi)\, G_k(\psi), \\ G_k(\forall z\, \varphi) &= (3)(c)\, G_k(\varphi), \\ G_k({=}\, t\, u) &= (0)\, G_k(t)\, G_k(u), \end{aligned}$$ de même pour $S\, t$, ${+}\, t\, u$ et ${\times}\, t\, u$, tandis que $G_k(x) = (\diamond)$ et que $G_k(\forall x\, \varphi)$ et $G_k(r)$ ne contiennent pas $\diamond$. Le point (i), les égalités $\llbracket (e) \rrbracket = \mathrm{aj}(0, \underline e) = \underline{\langle e \rangle}$ et $\llbracket (3)(c) \rrbracket = \underline{\langle 3, c \rangle}$, calculs clos, et $\llbracket (\diamond) \rrbracket(\tau) = \mathrm{conc}(0, \tau) = \tau$ (Concaténation dans PA, (iv)) donnent, avec (ii) appliqué à chacun des mots, les égalités annoncées.