Propriétés locales des lettres d'un code dans l'arithmétique de Peano

(i) Écrivons $l$ et $l'$ pour les valeurs de $\mathrm{lg}(M)$ et de $\mathrm{lg}(N)$. Par le point (ii) de Concaténation dans PA, $\mathrm{conc}(M, N)$ a pour longueur $l + l'$, son terme de rang $j < l$ est $(M)^j$, et son terme de rang $l + s$, pour $s < l'$, est $(N)^s$ ; par le point (iii) du même nœud, tout $j < l + l'$ vérifie $j < l$ ou s'écrit $l + s$ avec $s < l'$. On emploie la transitivité mixte de la preuve de Facteurs dans PA, et $l \leqslant l + l'$ (Ordre dans PA, (i)).

Absence. La longueur de $\mathrm{aj}(N, v)$ est $S\,l$, ses termes de rang $m < l$ sont ceux de $N$ et son terme de rang $l$ est $v$ (Longueur dans PA, (ii) et (iii)). Le point (i) (c) de Modules de Gödel décompose $\forall m < S\,l$ en $\forall m < l$ et le rang $l$, et les points (i) (a) et (b) du même nœud, sous l'hypothèse $m < l$, remplacent $(\mathrm{aj}(N, v))^m$ par $(N)^m$ ; d'où la première équivalence. Pour la concaténation, sous l'hypothèse $j < l + l'$, les deux cas donnent $\neg((\mathrm{conc}(M, N))^j = \underline k)$ par l'hypothèse sur $M$ au rang $j$, ou sur $N$ au rang $s$.

Préfixe et suffixe. Sous les hypothèses $\mathrm{Nq}_k(\mathrm{conc}(M, N))$, $i < l$ et $S\,i < l$, les rangs $i$ et $S\,i$ sont inférieurs à $l + l'$, les termes de $\mathrm{conc}(M, N)$ en ces rangs sont $(M)^i$ et $(M)^{S\,i}$, et l'hypothèse, instanciée par $i$, donne $\neg((M)^i = \underline 3 \wedge (M)^{S\,i} = \underline k)$ ; on généralise en $i$. Sous les hypothèses $s < l'$ et $S\,s < l'$, les rangs $l + s$ et $S(l + s) = l + S\,s$, par $\mathrm Q_5$, sont inférieurs à $l + l'$ par la compatibilité (Ordre dans PA, (vi)) et la commutativité (Lois de + et ×), et leurs termes sont $(N)^s$ et $(N)^{S\,s}$ ; on conclut de même.

Blocs. Sous les hypothèses $\mathrm{Bl}_k(M)$, $\mathrm{Bl}_k(N)$, $j < l + l'$ et $(\mathrm{conc}(M, N))^j = \underline 3$, distinguons les deux cas. Si $j < l$, alors $(M)^j = \underline 3$, et l'hypothèse sur $M$ donne $S\,j < l$, puis $\underline 8 \leqslant (M)^{S\,j}$ et $\neg((M)^{S\,j} = \underline k)$ ; comme $S\,j < l + l'$ et que $(\mathrm{conc}(M, N))^{S\,j} = (M)^{S\,j}$, le remplacement donne la conclusion au rang $j$. Si $j = l + s$ avec $s < l'$, alors $(N)^s = \underline 3$, l'hypothèse sur $N$ donne $S\,s < l'$, et le rang $S\,j = l + S\,s$ est inférieur à $l + l'$, de terme $(N)^{S\,s}$ ; on conclut de même. On généralise en $j$.

Enfin, sous les hypothèses $\mathrm{Bl}_k(N)$, $i < \mathrm{lg}(N)$ et $S\,i < \mathrm{lg}(N)$, si $(N)^i = \underline 3$, l'hypothèse donne $\neg((N)^{S\,i} = \underline k)$ ; la règle des tautologies donne $\neg((N)^i = \underline 3 \wedge (N)^{S\,i} = \underline k)$. Sous les hypothèses $\mathrm{Ab}_k(N)$ et $S\,i < \mathrm{lg}(N)$, l'instance de $\mathrm{Ab}_k(N)$ en $S\,i$ donne de même cette formule.

(ii) Sous les hypothèses $\mathrm{Ch}(\tau)$ et $m < \mathrm{lg}(\tau)$, on a $(\tau)^m = \underline 4$ ou $(\tau)^m = \underline 5$. Les calculs clos $\underline 4 < \underline 8$, $\underline 5 < \underline 8$, $\neg(\underline 4 = \underline k)$, $\neg(\underline 5 = \underline k)$, $\neg(\underline 4 = \underline 3)$ et $\neg(\underline 5 = \underline 3)$, vrais puisque $k \geqslant 8$, et le remplacement donnent $(\tau)^m < \underline 8$, $\neg((\tau)^m = \underline k)$ et $\neg((\tau)^m = \underline 3)$ ; la généralisation bornée donne $\mathrm{In}(\tau)$ et $\mathrm{Ab}_k(\tau)$, et, l'antécédent $(\tau)^i = \underline 3$ étant réfuté, $\mathrm{Bl}_k(\tau)$. Pour $\mathrm{num}(x)$, le point (iii) de Formation dans PA donne $\mathrm{lg}(\mathrm{num}(x)) = S\,x$ et, sous l'hypothèse $m < S\,x$, $(\mathrm{num}(x))^m = \underline 4 \vee (\mathrm{num}(x))^m = \underline 5$ ; le remplacement et le point (i) (a) de Modules de Gödel concluent.

(iii) Découpage en blocs. Un terme ne contient pas la lettre $\forall$. Dans une formule, chaque lettre $\forall$ est suivie de la variable $a_c$ de son bloc (Variables libres), qui est quantifiée : elle n'est ni l'une des $x_i$, ni $a_k$, et elle reste l'entier $c$ dans $G_{\bar x}(w)$. Le gabarit $G_{\bar x}(w)$ se découpe donc en blocs $B_1, \dots, B_q$, avec $q \geqslant 1$, dont chacun est $(\diamond_i)$, $(c)$ pour un entier $c \neq 3$, ou $(3)(c)$ pour un entier $c \geqslant 8$ différent de $k$ ; les blocs $(3)(c)$ ne se chevauchent pas, puisque $c \neq 3$. Par le point (i) de Gabarits à plusieurs places, $\ulcorner w \urcorner_{\bar x}(\bar\tau)$ est obtenu par concaténations successives des termes $\llbracket B_p \rrbracket(\bar\tau)$, qui sont $\tau_i$, $\underline{\langle c \rangle}$ ou $\underline{\langle 3, c \rangle}$, par $\mathrm{conc}(0, \tau_i) = \tau_i$ et des calculs clos.

Chaque bloc. $\mathrm{Bl}_k(\tau_i)$ découle de $\mathrm{Ch}(\tau_i)$ par (ii). Le code $\underline{\langle c \rangle}$, pour $c \neq 3$, a la longueur $S\,0$ ; sous l'hypothèse $i < S\,0$, les points (v) et (ii) de Ordre dans PA donnent $i = 0$, et le calcul clos $\neg((\underline{\langle c \rangle})^0 = \underline 3)$ réfute l'antécédent. Le code $\underline{\langle 3, c \rangle}$ a la longueur $S\,S\,0$ ; sous l'hypothèse $i < S\,S\,0$, on a $i = 0$ ou $i = S\,0$, par le point (v) de Calculs dans Q ; au rang $0$, les calculs clos $S\,0 < S\,S\,0$, $\underline 8 \leqslant \underline c$ et $\neg(\underline c = \underline k)$, avec $(\underline{\langle 3, c \rangle})^{S\,0} = \underline c$, donnent la conclusion, et au rang $S\,0$, le calcul clos $\neg(\underline c = \underline 3)$ réfute l'antécédent. Enfin $\mathrm{Bl}_k(0)$, puisque $\mathrm{lg}(0) = 0$ et que $\forall i < 0$ est démontrable. Une récurrence sur $q$, en métathéorie, avec la règle des blocs de (i), conclut.

Pour $\mathrm{Ab}_k$, si $k$ ne figure pas dans $G_{\bar x}(w)$, aucun bloc entier ne contient $k$. Par (i), $\mathrm{Ab}_k(\underline{\langle c \rangle})$ équivaut à $\mathrm{Ab}_k(0) \wedge \neg(\underline c = \underline k)$, et $\mathrm{Ab}_k(\underline{\langle 3, c \rangle})$ s'obtient de même en deux pas ; $\mathrm{Ab}_k(\tau_i)$ découle de (ii), et la règle de concaténation de (i) conclut.

(iv) Comme au point (ii) de Formules des instances, mais pour un terme $N$ quelconque à la place du chiffre $\underline n$, la formule naturelle de $\mathrm{Sbl}$ se lit clause par clause, par les points (iii) et (iv) de Relations p.r. dans PA et les points (ii) (b) et (d) de Termes fonctionnels : $\widehat{\mathrm{Sbl}}(T, \underline k, N)$ découle de $$\begin{aligned} &\forall j < \mathrm{lg}(N)\ \neg\exists i < j \\ &\quad \exists l' < S\,\mathrm{lg}(N)\ \big((N)^i = \underline 3 \\ &\quad \wedge \exists m < \mathrm{lg}(T)\ (T)^m = (N)^{S\,i} \\ &\quad \wedge \Psi\big), \end{aligned}$$ où $\Psi$ réunit les clauses qui ne servent pas. Il suffit de tirer une contradiction des hypothèses $\mathrm{In}(T)$, $\mathrm{Bl}_k(N)$, $j < \mathrm{lg}(N)$, $i < j$, $(N)^i = \underline 3$, $m < \mathrm{lg}(T)$ et $(T)^m = (N)^{S\,i}$. La transitivité donne $i < \mathrm{lg}(N)$, et $\mathrm{Bl}_k(N)$, instanciée par $i$, donne $\underline 8 \leqslant (N)^{S\,i} = (T)^m$, alors que $\mathrm{In}(T)$, instanciée par $m$, donne $(T)^m < \underline 8$ : le dernier point de (v) de Ordre dans PA exclut les deux. Pour la dernière assertion, $\mathrm{In}(\mathrm{num}(y))$ et $\mathrm{Bl}_k(\ulcorner \varphi[\dot{\bar y}/\bar x] \urcorner)$ découlent de (ii) et (iii), et $\underline 9$ est $\mathrm{num}(0)$, par le point (iii) de Formation dans PA, de sorte que $\mathrm{In}(\underline 9)$ découle de $\mathrm{Ch}(\mathrm{num}(0))$ et du remplacement.