Termes fonctionnels et énoncés vrais de la classe 𝒮 dans l'arithmétique de Peano

(i) Par récurrence sur les termes, la définition de la traduction montre que chaque occurrence de $f(t)$ produit, dans la traduction de la formule atomique où elle figure, une sous-formule $\exists e'\, (f(t) = e' \wedge \beta)$, où $e'$ est une variable nouvelle et $\beta$ la traduction du reste, écrite avec $e'$ à la place de $f(t)$ ; comme $e$ est un terme ordinaire, la traduction de $\Phi_e$, écrite avec les mêmes variables nouvelles, ce que permet l'équivalence des traductions établie dans le texte, porte au même endroit la formule $\beta[e/e']$, où $e$ est substituable puisque les variables nouvelles de la traduction sont prises hors de $e$.

Sous l'hypothèse $f(t) = e$, montrons $\exists e'\, (f(t) = e' \wedge \beta) \leftrightarrow \beta[e/e']$. Sous l'hypothèse supplémentaire $f(t) = e' \wedge \beta$, le point (ii) de Fonctions p.r. dans PA donne $e' = e$, et le remplacement d'un terme (Calcul à variables libres, (v)) donne $\beta[e/e']$ ; l'élimination de $e'$, qui n'est libre ni dans $f(t) = e$ ni dans $\beta[e/e']$, donne un sens. Pour l'autre, $(f(t) = e' \wedge \beta)[e/e']$ est $f(t) = e \wedge \beta[e/e']$, et l'introduction de l'existentiel, avec le terme $e$, conclut.

Les variables liées au-dessus de cette sous-formule, dans la traduction de $\Phi$, sont des variables quantifiées dans $\Phi$ ou introduites par la traduction ; par hypothèse et par le choix des variables nouvelles, aucune n'est $e$ ni une variable des $t_k$, et aucune n'est donc libre dans $f(t) = e$. Une récurrence sur la formule, avec la règle des tautologies pour les connecteurs et la monotonie du point (ii) de Récurrence dans PA pour les quantificateurs, permise sous l'hypothèse $f(t) = e$, remplace la sous-formule par son équivalente. On traite ainsi les occurrences choisies une à une.

(ii) (a) Par le point (ii) de Fonctions p.r. dans PA, $\vdash_{\mathsf{PA}} \exists e\ f(t) = e$, puisque $e$ ne figure pas dans les $t_k$. L'élimination de l'existentiel (Récurrence dans PA, (i)), permise puisque $e$ n'est libre ni dans $\Gamma$ ni dans $\Psi$, donne $\Gamma \cup \{\exists e\ f(t) = e\} \vdash_{\mathsf{PA}} \Psi$, puis $\Gamma \vdash_{\mathsf{PA}} \Psi$.

(b) Par récurrence sur le nombre de symboles de fonctions primitives récursives de $\tau$. Si $\tau$ est ordinaire, la traduction de $\Phi[\tau/x]$ est celle de $\Phi$ où l'on a substitué $\tau$ à $x$, puisqu'on prend les variables nouvelles de la traduction hors de $\tau$, ce que permet l'équivalence des traductions établie dans le texte. La généralisation sous hypothèses (Récurrence dans PA, (i)) donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, \Phi$, et l'axiome (2), avec le terme $\tau$, qui est substituable puisqu'aucune de ses variables n'est quantifiée dans la traduction, donne $\Gamma \vdash_{\mathsf{PA}} \Phi[\tau/x]$. Sinon, soit $f(t)$ un sous-terme de $\tau$ dont les arguments sont ordinaires, $e$ une variable nouvelle, et $\tau_e$ le terme obtenu en remplaçant cette occurrence par $e$. L'hypothèse de récurrence donne $\Gamma \vdash_{\mathsf{PA}} \Phi[\tau_e/x]$. Les occurrences de $f(t)$ qui viennent de $\tau$ ne sont dans la portée d'aucun quantificateur sur une variable des $t_k$, puisqu'aucune variable de $\tau$ n'est quantifiée dans $\Phi$ ; le point (i) donne donc $\{f(t) = e\} \vdash_{\mathsf{PA}} \Phi[\tau/x] \leftrightarrow \Phi[\tau_e/x]$, d'où $\Gamma \cup \{f(t) = e\} \vdash_{\mathsf{PA}} \Phi[\tau/x]$, et (a) conclut.

(c) Par des applications répétées de (i), en commençant par les termes intérieurs, on remplace $\tau$, $\sigma$ et $\rho$, sous des hypothèses $f(t) = e$ portant sur des variables nouvelles, par des variables $e_\tau$, $e_\sigma$, $e_\rho$ : on dit qu'on écrit avec les valeurs. Les quatre formules deviennent $e_\tau = e_\tau$, $e_\tau = e_\sigma \to e_\sigma = e_\tau$, la transitivité, et $e_\tau = e_\sigma \to (\Phi[e_\tau/x] \leftrightarrow \Phi[e_\sigma/x])$, qui découlent des points (v) et (vi) de Calcul à variables libres, appliqués à la traduction de $\Phi$, où $e_\tau$ et $e_\sigma$ sont substituables. Le point (a) élimine les hypothèses.

(d) Par le point (i) de Fonctions usuelles dans PA, dernière assertion, on a, pour des variables nouvelles $e_j$, $\{g_1(v) = e_1, \dots, g_m(v) = e_m\} \vdash_{\mathsf{PA}} h(v) = w \leftrightarrow f(e_1, \dots, e_m) = w$. Sous les mêmes hypothèses, le point (i) donne $f(g_1(v), \dots, g_m(v)) = w \leftrightarrow f(e_1, \dots, e_m) = w$, et (a) élimine les hypothèses : $\vdash_{\mathsf{PA}} h(v) = w \leftrightarrow f(g_1(v), \dots, g_m(v)) = w$. Écrite avec la valeur $w$ de $h(v)$, c'est l'égalité annoncée pour les variables $v$, et (b) la donne pour les termes $\tau$. Pour la relation, le point (iii) de Relations p.r. dans PA donne $\vdash_{\mathsf{PA}} \hat P(v) \leftrightarrow \exists z_1 \cdots \exists z_m\, \big(g_1(v) = z_1 \wedge \cdots \wedge g_m(v) = z_m \wedge \hat R(z)\big)$, et la traduction de $\hat R(g_1(v), \dots, g_m(v))$ imbrique les $g_j$ dans l'ordre inverse, puisque la dernière substitution est la plus extérieure : c'est $\exists z_m\, \big(g_m(v) = z_m \wedge \cdots \exists z_1\, (g_1(v) = z_1 \wedge \hat R(z)) \cdots\big)$. Elles sont équivalentes par la logique pure. D'une part, si $z$ n'est pas libre dans $\alpha$, alors $\vdash \exists z\, (\alpha \wedge \beta) \leftrightarrow (\alpha \wedge \exists z\, \beta)$, par l'introduction et l'élimination de l'existentiel du point (iii) de Calcul à variables libres et la règle des tautologies ; cela fait sortir chaque $g_j(v) = z_j$, où les autres $z_l$ ne figurent pas, de la portée des quantificateurs qu'il précède ou qui le suivent. D'autre part, $\vdash \exists z\, \exists z'\, \gamma \leftrightarrow \exists z'\, \exists z\, \gamma$, par deux introductions et deux éliminations, ce qui permet de ranger les quantificateurs dans le même ordre. Le point (b) conclut.

(iii) Soit $\sigma$ un énoncé de $\mathcal S$, vrai dans $\mathcal N$. Par le point (ii) de Collection et forme Σ₁, une construction de $\sigma$ lui associe une formule $\exists y\, \delta$, où $\delta$ est Δ₀ et n'a pas d'autre variable libre que $y$, telle que $\vdash_{\mathsf{PA}} \sigma \leftrightarrow \exists y\, \delta$ ; c'est un énoncé Σ₁. La structure $\mathcal N$ est un modèle de $\mathsf{PA}$ (Gödel-Rosser, (iii)), et le théorème de correction y rend vraie cette équivalence : $\exists y\, \delta$ est vrai dans $\mathcal N$. La Σ₁-complétude, (iii), donne $\mathsf Q \vdash \exists y\, \delta$, donc $\vdash_{\mathsf{PA}} \exists y\, \delta$, puisque $\mathsf{PA}$ démontre tout ce que démontre $\mathsf Q$ (Récurrence dans PA), et la règle des tautologies donne $\vdash_{\mathsf{PA}} \sigma$.

(iv) Remplaçons dans $\Phi$ chaque formule $\neg\hat R(\tau_1, \dots, \tau_n)$ par $\chi_R(\tau_1, \dots, \tau_n) = 0$, et notons $\Phi'$ le résultat. Par le point (i) de Relations p.r. dans PA, $\vdash_{\mathsf{PA}} \neg\hat R(v) \leftrightarrow \chi_R(v) = 0$, et (b), appliqué d'abord à des variables nouvelles $u_k$ substituées aux $v_k$, puis aux termes $\tau_k$ substitués aux $u_k$, donne ces équivalences pour les termes $\tau_k$, en une substitution simultanée ; la règle des tautologies donne $\vdash_{\mathsf{PA}} \Phi \leftrightarrow \Phi'$. La traduction de $\Phi'$ est dans $\mathcal S$ : elle s'obtient par $\wedge$, $\vee$ et des quantifications existentielles à partir de formules atomiques, de formules $f(e_1, \dots, e_n) = e$, qui sont dans $\mathcal S$ par le point (i) de Fonctions p.r. dans PA, et de formules $\hat R(e_1, \dots, e_n)$, qui y sont aussi. Par le lemme de substitution et parce que chaque définition naturelle définit le graphe de sa fonction et chaque formule naturelle sa relation, une récurrence sur les termes montre que la traduction de $\tau = \sigma$ est vraie dans $\mathcal N$ si et seulement si les valeurs de $\tau$ et de $\sigma$, calculées avec les fonctions $f$, sont égales, et de même pour $\hat R(\tau)$ et $\chi_R(\tau) = 0$. La traduction de $\Phi'$ est donc vraie dans $\mathcal N$, et (iii) donne $\vdash_{\mathsf{PA}} \Phi'$, puis $\vdash_{\mathsf{PA}} \Phi$. Les cas particuliers sont ceux d'une seule égalité et d'une seule formule $\hat R$ ou $\neg\hat R$.