Règles de formation des termes et des formules, et chiffres, dans l'arithmétique de Peano

Lecture des relations. Par le point (iv) de Récurrence de valeurs dans PA, $\vdash_{\mathsf{PA}} \widehat{\mathrm{Tm}}(N) \leftrightarrow \hat Q(N, F_{\mathrm{Tm}}(N))$, où $Q$ est la disjonction des trois cas de la preuve de Termes. Sa formule naturelle se lit clause par clause, comme au point (ii) de Deuxième condition (D2) : la disjonction et la conjonction par le point (iii) de Relations p.r. dans PA, la quantification bornée par le point (iv), les relations de base par le point (ii), et les substitutions de fonctions par le point (ii) (d) de Termes fonctionnels, les constantes devenant des chiffres par le point (i) de Fonctions usuelles dans PA. Il en résulte que $\widehat{\mathrm{Tm}}(N)$ découle de chacune des deux formules $$\begin{aligned} &(N)^0 = \underline 5 \wedge S\,S\,0 \leqslant \mathrm{lg}(N) \\ &\quad \wedge (F_{\mathrm{Tm}}(N))^{\mathrm{sm}(N, S\,0, \mathrm{lg}(N))} = S\,0, \\[4pt] &(N)^0 = \underline e \wedge \exists j < \mathrm{lg}(N)\ \big(S\,S\,0 \leqslant j \\ &\quad \wedge (F_{\mathrm{Tm}}(N))^{\mathrm{sm}(N, S\,0, j)} = S\,0 \\ &\quad \wedge (F_{\mathrm{Tm}}(N))^{\mathrm{sm}(N, j, \mathrm{lg}(N))} = S\,0\big), \end{aligned}$$ avec $e = 6$ ou $e = 7$. De même, $\widehat{\mathrm{At}}(N)$ découle de $(N)^0 = 0 \wedge \exists j < \mathrm{lg}(N)\ \big(S\,S\,0 \leqslant j \wedge \widehat{\mathrm{Tm}}(\mathrm{sm}(N, S\,0, j)) \wedge \widehat{\mathrm{Tm}}(\mathrm{sm}(N, j, \mathrm{lg}(N)))\big)$, et $\widehat{\mathrm{Fm}}(N)$ découle de $\widehat{\mathrm{At}}(N)$, et des trois formules écrites comme ci-dessus avec $F_{\mathrm{Fm}}$ pour les cas $\neg$, $\to$ et $\forall$ de la preuve de Formules ; le dernier s'écrit $(N)^0 = \underline 3 \wedge S\,S\,S\,0 \leqslant \mathrm{lg}(N) \wedge \underline 8 \leqslant (N)^{S\,0} \wedge (F_{\mathrm{Fm}}(N))^{\mathrm{sm}(N, S\,S\,0, \mathrm{lg}(N))} = S\,0$.

Les fonctions caractéristiques de ces relations $Q$ sont des disjonctions, donc booléennes dans $\mathsf{PA}$ (Relations p.r. dans PA, (iii)), et le point (iv) de Récurrence de valeurs dans PA rend booléennes $\chi_{\mathrm{Tm}}$ et $\chi_{\mathrm{Fm}}$. Par les points (ii) et (iv) du même nœud, sous l'hypothèse $A < N$, on a $(F_{\mathrm{Tm}}(N))^A = \chi_{\mathrm{Tm}}(A)$, valeur égale à $0$ ou à $S\,0$, et $\neg\big((F_{\mathrm{Tm}}(N))^A = 0\big) \leftrightarrow \widehat{\mathrm{Tm}}(A)$ ; d'où $$\begin{aligned} \vdash_{\mathsf{PA}} {}&A < N \to \big(\widehat{\mathrm{Tm}}(A) \\ &\qquad \leftrightarrow (F_{\mathrm{Tm}}(N))^A = S\,0\big), \end{aligned}$$ et de même pour $\mathrm{Fm}$. Enfin, $0$ ne code ni un terme ni une formule, et le point (iv) de Termes fonctionnels donne $\vdash_{\mathsf{PA}} \neg\widehat{\mathrm{Tm}}(0)$ et $\vdash_{\mathsf{PA}} \neg\widehat{\mathrm{Fm}}(0)$ ; par le remplacement, $\widehat{\mathrm{Tm}}(A)$ et $\widehat{\mathrm{Fm}}(A)$ entraînent $\neg(A = 0)$, puis $\neg(\mathrm{lg}(A) = 0)$ et $S\,0 \leqslant \mathrm{lg}(A)$, par le point (ii) de Longueur dans PA et le point (v) de Ordre dans PA.

Préfixes fixés. Soit $P = \langle c_0, \dots, c_{p-1} \rangle$ le code d'un mot fixé de longueur $p \geqslant 1$. Par le point (iv) de Termes fonctionnels, $\vdash_{\mathsf{PA}} \mathrm{lg}(\underline P) = \underline p$ et $\vdash_{\mathsf{PA}} (\underline P)^{\underline r} = \underline{c_r}$ pour $r < p$. Soit $N = \mathrm{cc}(\underline P, A, B)$. Par les points (ii) de Concaténation dans PA et (iv) de Facteurs dans PA, avec $\vdash_{\mathsf{PA}} \underline r < \underline p$, on a $\mathrm{lg}(N) = \underline p + \mathrm{lg}(A) + \mathrm{lg}(B)$, $(N)^{\underline r} = \underline{c_r}$ pour $r < p$, $\mathrm{sm}(N, \underline p, \underline p + \mathrm{lg}(A)) = A$, et $\mathrm{sm}(N, \underline p + \mathrm{lg}(A), \mathrm{lg}(N)) = B$, ce dernier en appliquant le même point (iv) à $\mathrm{cc}(\mathrm{conc}(\underline P, A), B, 0)$, qui est $N$ par le point (iv) de Concaténation dans PA. Comme $\underline P$ n'est pas nul, le point (iv) de Facteurs dans PA donne $A < N$, et le point (iii) du même nœud donne $B < N$, puisque $\mathrm{conc}(\underline P, A)$, qui est au moins $\underline P$, n'est pas nul. Pour $B = 0$, $N = \mathrm{conc}(\underline P, A)$, et ces égalités donnent $\mathrm{sm}(N, \underline p, \mathrm{lg}(N)) = A$.

(i) Sous l'hypothèse $\widehat{\mathrm{Tm}}(A)$, soit $N = \mathrm{conc}(\underline{\langle 5 \rangle}, A)$ ; ici $p = 1$. On a $(N)^0 = \underline 5$, et $\mathrm{lg}(N) = S\,0 + \mathrm{lg}(A) \geqslant S\,0 + S\,0 = S\,S\,0$, par la compatibilité. Comme $A < N$, la lecture donne $(F_{\mathrm{Tm}}(N))^A = S\,0$, et le remplacement, avec $\mathrm{sm}(N, S\,0, \mathrm{lg}(N)) = A$, donne la première formule de la lecture : $\widehat{\mathrm{Tm}}(N)$. Sous les hypothèses $\widehat{\mathrm{Tm}}(A)$ et $\widehat{\mathrm{Tm}}(B)$, soit $N = \mathrm{cc}(\underline{\langle e \rangle}, A, B)$ et $j = S\,0 + \mathrm{lg}(A)$. Alors $S\,S\,0 \leqslant j$, et $j < \mathrm{lg}(N) = j + \mathrm{lg}(B)$ puisque $S\,0 \leqslant \mathrm{lg}(B)$ ; les facteurs $\mathrm{sm}(N, S\,0, j) = A$ et $\mathrm{sm}(N, j, \mathrm{lg}(N)) = B$ sont plus petits que $N$, et la lecture donne $(F_{\mathrm{Tm}}(N))^A = S\,0$ et $(F_{\mathrm{Tm}}(N))^B = S\,0$. L'introduction de la quantification bornée stricte, avec le terme $j$ (Modules de Gödel, (i) (b), appliqué à la négation, et contraposition), donne la seconde formule de la lecture.

(ii) Le cas atomique est celui de la seconde formule de (i), avec $\widehat{\mathrm{Tm}}(A)$ et $\widehat{\mathrm{Tm}}(B)$ en place des valeurs de l'historique : il n'y a pas d'historique pour $\mathrm{At}$, et $\widehat{\mathrm{At}}(N)$ donne $\widehat{\mathrm{Fm}}(N)$. Les cas $\neg$ et $\to$ sont ceux de (i), avec $\mathrm{Fm}$, les lettres $1$ et $2$, et l'historique $F_{\mathrm{Fm}}$. Pour $N = \mathrm{conc}(\underline{\langle 3, c \rangle}, A)$, ici $p = 2$ : on a $(N)^0 = \underline 3$, $(N)^{S\,0} = \underline c$, qui est au moins $\underline 8$ par le point (iv) de Termes fonctionnels, $\mathrm{lg}(N) = S\,S\,0 + \mathrm{lg}(A) \geqslant S\,S\,S\,0$, et $\mathrm{sm}(N, S\,S\,0, \mathrm{lg}(N)) = A < N$, d'où la troisième formule de la lecture pour $\mathrm{Fm}$.

(iii) Par le point (iv) de Fonctions p.r. dans PA, sans paramètre, $\mathrm{num}(0) = w$ équivaut à $w = \underline 9$, et, sous l'hypothèse $\mathrm{num}(x) = u$, $\mathrm{num}(S\,x) = w$ équivaut à $\mathrm{conc}(\mathbf c_{11}(x), u) = w$, par le point (ii) (d) de Termes fonctionnels, c'est-à-dire à $\mathrm{conc}(\underline{11}, u) = w$, par le point (i) de Fonctions usuelles dans PA ; écrites avec la valeur $u$, ce sont les deux équations, puisque $\langle 5 \rangle = 11$.

Longueur. Récurrence sur $x$ : $\mathrm{lg}(\underline 9) = S\,0$ par un calcul clos, et $\mathrm{lg}(\mathrm{num}(S\,x)) = S\,0 + \mathrm{lg}(\mathrm{num}(x)) = S\,0 + S\,x = S\,S\,x$, par le point (ii) de Concaténation dans PA et le point (i) de Lois de + et ×.

Lettres. Montrons $\forall m\, \big(m < S\,x \to ((\mathrm{num}(x))^m = \underline 4 \vee (\mathrm{num}(x))^m = \underline 5)\big)$ par récurrence sur $x$. Pour $0$, $m < S\,0$ donne $m = 0$ (Ordre dans PA, (ii) et (v)), et $(\underline 9)^0 = \underline 4$ par un calcul clos. Pour le pas, sous $m < S\,S\,x$, distinguons $m = 0$ et $m = S\,m'$, par l'instance de $\mathrm Q_3$. Si $m = 0$, le point (ii) de Concaténation dans PA, avec $0 < \mathrm{lg}(\underline{11}) = S\,0$, donne $(\mathrm{num}(S\,x))^0 = (\underline{11})^0 = \underline 5$. Si $m = S\,m'$, alors $m' < S\,x = \mathrm{lg}(\mathrm{num}(x))$, et le même point donne $(\mathrm{num}(S\,x))^{S\,0 + m'} = (\mathrm{num}(x))^{m'}$, avec $S\,0 + m' = S\,m'$ ; l'hypothèse de récurrence, instanciée par $m'$, conclut. On généralise en $m$, puis on instancie.

Terme. Récurrence sur $x$ : $\widehat{\mathrm{Tm}}(\underline 9)$ est un calcul clos, et le pas est (i). Enfin, $\mathrm{num}(n) = \ulcorner \underline n \urcorner$ dans $\mathcal N$, et le point (iv) de Termes fonctionnels donne la dernière égalité.