Les instances d'une formule fixée sont des formules, et les chiffres y sont substituables, dans l'arithmétique de Peano

(i) Par récurrence sur la construction de $t$, puis de $\varphi$, en métathéorie, sous l'hypothèse $\widehat{\mathrm{Tm}}(\tau)$, avec les égalités du point (iii) de Substitution dépliée et le remplacement (Termes fonctionnels, (ii) (c)). Si $t$ est $x$, $\mathrm{Sb}\ulcorner x \urcorner = \tau$, qui code un terme par hypothèse. Si $t$ est $0$ ou une autre variable, $\mathrm{Sb}\ulcorner t \urcorner = \underline{\ulcorner t \urcorner}$, et $\widehat{\mathrm{Tm}}(\underline{\ulcorner t \urcorner})$ est un calcul clos. Si $t$ est $S\, t_1$, ${+}\, t_1\, t_2$ ou ${\times}\, t_1\, t_2$, l'hypothèse de récurrence et le point (i) de Formation dans PA concluent. Pour les formules, le cas atomique ${=}\, t\, u$ découle du cas des termes et du point (ii) du même nœud ; les cas $\neg\varphi$, ${\to}\, \varphi\, \psi$ et $\forall z\, \varphi$, avec $z = a_c$ distincte de $x$, découlent de l'hypothèse de récurrence et du même point, avec l'entier $c \geqslant 8$ ; enfin, $\mathrm{Sb}\ulcorner \forall x\, \varphi \urcorner = \underline{\ulcorner \forall x\, \varphi \urcorner}$, et $\widehat{\mathrm{Fm}}(\underline{\ulcorner \forall x\, \varphi \urcorner})$ est un calcul clos.

(ii) Soit $n = \ulcorner \varphi \urcorner$ et $l$ la longueur de $\varphi$. La formule naturelle de $\mathrm{Sbl}$ se lit clause par clause, comme au point (ii) de Deuxième condition (D2) : $\widehat{\mathrm{Sbl}}(\tau, \underline k, \underline n)$ découle de $$\begin{aligned} &\forall j < \mathrm{lg}(\underline n)\ \neg\exists i < j \\ &\quad \exists l' < S\,\mathrm{lg}(\underline n)\ \big((\underline n)^i = \underline 3 \\ &\quad \wedge \exists m < \mathrm{lg}(\tau)\ (\tau)^m = (\underline n)^{S\,i} \\ &\quad \wedge \Psi\big), \end{aligned}$$ où $\Psi$ réunit les clauses $S\,S\,i \leqslant j$, $j < l'$ et $\widehat{\mathrm{Fm}}(\mathrm{sm}(\underline n, S\,S\,i, l'))$, qui ne servent pas, et où $i + 1$ et $i + 2$ sont écrits $S\,i$ et $S\,S\,i$ par $\mathrm Q_4$ et $\mathrm Q_5$. Par le point (i) (a) de Modules de Gödel et l'élimination des quantifications bornées strictes (preuve de Deuxième condition (D2)), il suffit de tirer une contradiction des hypothèses $\mathrm{In}(\tau)$, $j < \mathrm{lg}(\underline n)$, $i < j$, $(\underline n)^i = \underline 3$, $m < \mathrm{lg}(\tau)$ et $(\tau)^m = (\underline n)^{S\,i}$.

Comme $\mathrm{lg}(\underline n) = \underline l$, la transitivité donne $i < \underline l$ ; en particulier $l \geqslant 1$, et $i \leqslant \underline{l - 1}$, de sorte que le point (v) de Calculs dans Q donne la disjonction des formules $i = \underline r$, pour $r < l$. Raisonnons par cas. Si la lettre de rang $r$ de $\varphi$ n'est pas $\forall$, le calcul clos $\neg((\underline n)^{\underline r} = \underline 3)$ et le remplacement contredisent $(\underline n)^i = \underline 3$. Si elle l'est, le texte de Variables libres dit qu'elle est suivie de la variable de son bloc, de sorte que $r + 1 < l$ et que le calcul clos $\underline 8 \leqslant (\underline n)^{S\,\underline r}$ est démontrable ; alors $\underline 8 \leqslant (\tau)^m$, alors que $\mathrm{In}(\tau)$, instanciée par $m$ (Modules de Gödel, (i) (b)), donne $(\tau)^m < \underline 8$, ce qu'exclut le dernier point de (v) de Ordre dans PA.

(iii) Par le point (iii) de Formation dans PA, $\widehat{\mathrm{Tm}}(\mathrm{num}(y))$, et, pour $m < \mathrm{lg}(\mathrm{num}(y)) = S\,y$, $(\mathrm{num}(y))^m$ vaut $\underline 4$ ou $\underline 5$, qui sont plus petits que $\underline 8$ ; le point (i) (a) de Modules de Gödel donne $\mathrm{In}(\mathrm{num}(y))$, et (i) et (ii), appliqués au terme $\mathrm{num}(y)$, donnent les deux premières formules. Si $x$ est libre dans $\varphi$, le signe $\diamond$ figure dans $G_k(\varphi)$, et les points (i) et (ii) de Substitution dépliée donnent $\mathrm{num}(y) \leqslant \llbracket G_k(\varphi) \rrbracket(\mathrm{num}(y)) = \ulcorner \varphi[\dot y/x] \urcorner$ ; sinon, le point (ii) du même nœud donne la dernière égalité.