Formule naturelle de démontrabilité, mise bout à bout des démonstrations et deuxième condition de dérivabilité

On emploie deux règles sur les quantifications bornées strictes, qui découlent du point (i) de Modules de Gödel, puisque $\exists x < t\ \varphi$ abrège $\neg\forall x < t\ \neg\varphi$. Introduction : $\vdash_{\mathsf{PA}} (u < t \wedge \varphi[u/x]) \to \exists x < t\ \varphi$ pour un terme $u$ substituable, par (b) appliqué à $\neg\varphi$ et la contraposition. Élimination : si $x$ n'est libre ni dans $\psi$ ni dans $\Gamma$, et si $\Gamma \cup \{x < t, \varphi\} \vdash_{\mathsf{PA}} \psi$, alors $\Gamma \cup \{\exists x < t\ \varphi\} \vdash_{\mathsf{PA}} \psi$ ; en effet, la contraposition donne $\Gamma \cup \{\neg\psi, x < t\} \vdash_{\mathsf{PA}} \neg\varphi$, le point (a) donne $\Gamma \cup \{\neg\psi\} \vdash_{\mathsf{PA}} \forall x < t\ \neg\varphi$, et la règle des tautologies conclut.

(i) La formule $\hat D(p, v)$ est dans $\mathcal S$, par le texte de Relations p.r. dans PA, et $\mathcal S$ est stable par la quantification existentielle ; ses variables libres sont parmi $p$ et $v$. Comme une formule naturelle définit sa relation, $\mathrm{Pr}_T$ est satisfaite sous une valuation qui vaut $c$ en $v$ si et seulement s'il existe un entier $m$ tel que $D(m, c)$, c'est-à-dire si et seulement si $c$ code un énoncé $\sigma$ et qu'une démonstration formelle de $\sigma$ à partir de $T'$ existe. Par le point (i) du théorème de Craig, c'est dire que $T \vdash \sigma$ : $\mathrm{Pr}_T$ définit $\mathrm{Th}(T)$. Le point (ii) de Collection et forme Σ₁ donne $\vdash_{\mathsf{PA}} \mathrm{Pr}_T \leftrightarrow \exists y\, \delta$, où $\delta$ est Δ₀ et a ses variables libres parmi $v$ et $y$ ; le renommage de la preuve du point (i) de Forme Σ₁ des r.e. permet de prendre $y$ distincte de $v$. Comme $\mathcal N$ est un modèle de $\mathsf{PA}$ (Gödel-Rosser, (iii)), le théorème de correction montre que $\exists y\, \delta$ définit le même ensemble que $\mathrm{Pr}_T$. Enfin, si $T \vdash \sigma$, l'énoncé $\mathrm{Pr}_T\,\ulcorner \sigma \urcorner$, qui est $\exists p\ \hat D(p, \underline{\ulcorner \sigma \urcorner})$ puisque $p$ est distincte de $v$, est un énoncé de $\mathcal S$ vrai dans $\mathcal N$, et le point (iii) de Termes fonctionnels le démontre dans $\mathsf{PA}$ ; l'équivalence, instanciée par le chiffre $\underline{\ulcorner \sigma \urcorner}$ (Récurrence dans PA, (iv)), donne la formule Σ₁ correspondante.

(ii) Chaque clause de la construction se traduit dans $\mathsf{PA}$ par la clause correspondante de Relations p.r. dans PA : la conjonction et la disjonction par le point (iii), les quantifications bornées par le point (iv), et chaque substitution de fonctions, par le point (ii) (d) de Termes fonctionnels, en une formule écrite avec les termes fonctionnels correspondants, dont les fonctions constantes et les projections disparaissent par le point (i) de Fonctions usuelles dans PA. La relation $1 \leqslant \mathrm{lg}(p)$ devient $S\,0 \leqslant \mathrm{lg}(p)$ par le point (ii) de Relations p.r. dans PA, et l'égalité $(p)^{\mathrm{lg}(p) \mathbin{\dot{-}} 1} = c$ devient l'égalité de termes fonctionnels de l'énoncé, par le même point. Le remplacement d'une sous-formule par une formule équivalente dans $\mathsf{PA}$, par la règle des tautologies et la monotonie de Récurrence dans PA, (ii), et du point (i) (e) de Ordre dans PA pour les bornes, donne la première équivalence ; la seconde est le point (iii) de Relations p.r. dans PA, appliqué à la conjonction, avec la substitution de $c$.

(iii) Raisonnons sous les quatre hypothèses, et écrivons avec les valeurs, au sens de Termes fonctionnels : $r$ pour $\mathrm{aj}(\mathrm{conc}(p, q), c)$, $l_p$ et $l_q$ pour $\mathrm{lg}(p)$ et $\mathrm{lg}(q)$. Par (ii), $S\,0 \leqslant l_p$ et $S\,0 \leqslant l_q$ ; ni $l_p$ ni $l_q$ n'est nul, et l'instance de $\mathrm Q_3$ fournit $k$ et $m$ tels que $l_p = S\,k$ et $l_q = S\,m$. Par le point (iii) de Fonctions usuelles dans PA, $S\,k \mathbin{\dot{-}} S\,0 = k$, et (ii) donne $(p)^k = b$ ; de même $(q)^m = a$. Par le point (ii) de Concaténation dans PA et le point (ii) de Longueur dans PA, $\mathrm{lg}(\mathrm{conc}(p, q)) = l_p + l_q$ et $\mathrm{lg}(r) = S(l_p + l_q)$. Les termes de $r$ sont donnés par le point (iii) de Longueur dans PA et le point (ii) de Concaténation dans PA : $(r)^j = (p)^j$ si $j < l_p$, $(r)^{l_p + s} = (q)^s$ si $s < l_q$, et $(r)^{l_p + l_q} = c$.

Les deux premières clauses. On a $S\,0 \leqslant S(l_p + l_q)$, puisque $0 \leqslant l_p + l_q$, et $S(l_p + l_q) \mathbin{\dot{-}} S\,0 = l_p + l_q$, d'où $(r)^{\mathrm{lg}(r) \mathbin{\dot{-}} S\,0} = (r)^{l_p + l_q} = c$.

La clause bornée. Par le point (i) (c) de Modules de Gödel, $\forall j < S(l_p + l_q)\ \Lambda(r, j)$ équivaut à la conjonction de $\forall j < l_p + l_q\ \Lambda(r, j)$ et de $\Lambda(r, l_p + l_q)$. Sous l'hypothèse $j < l_p + l_q$, le point (iii) de Concaténation dans PA donne deux cas.

Si $j < l_p$, le point (i) (b) de Modules de Gödel, appliqué à la clause bornée de $\widehat{\mathrm{Dem}}(p, b)$, donne $\Lambda(p, j)$. Comme $(r)^j = (p)^j$, le remplacement (Termes fonctionnels, (ii) (c)) transporte $\widehat{\mathrm{Fm}}$, $\widehat{\mathrm{Ax}}$ et $\widehat{\mathrm{Ax}}_{T'}$ de $(p)^j$ à $(r)^j$. Pour le dernier cas, l'élimination fournit $i < j$ et $i' < j$ tels que $\widehat{\mathrm{MP}}((p)^i, (p)^{i'}, (p)^j)$ ; comme $i$ et $i'$ sont inférieurs à $l_p$, par la transitivité, $(p)^i = (r)^i$ et $(p)^{i'} = (r)^{i'}$, et deux introductions donnent $\exists i < j\ \exists i' < j\ \widehat{\mathrm{MP}}((r)^i, (r)^{i'}, (r)^j)$. Dans tous les cas, $\Lambda(r, j)$.

Si $j = l_p + s$ avec $s < l_q$, le même raisonnement, appliqué à $\widehat{\mathrm{Dem}}(q, a)$ au rang $s$, transporte les clauses de $(q)^s$ à $(r)^j$ ; pour le dernier cas, des rangs $i < s$ et $i' < s$ donnent les rangs $l_p + i$ et $l_p + i'$, inférieurs à $l_p + s = j$ par la compatibilité, et inférieurs à $l_p + l_q$, de termes $(r)^{l_p + i} = (q)^i$ et $(r)^{l_p + i'} = (q)^{i'}$. Le point (i) (a) de Modules de Gödel donne $\forall j < l_p + l_q\ \Lambda(r, j)$, la variable $j$ n'étant libre dans aucune hypothèse.

Le dernier rang. Au rang $l_p + l_q$, le terme est $c$, et $\widehat{\mathrm{Fm}}(c)$ est une hypothèse. Le rang $l_p + m$ est inférieur à $l_p + S\,m = l_p + l_q$, et son terme est $(q)^m = a$, puisque $m < S\,m$ ; le rang $k$ est inférieur à $S\,k = l_p \leqslant l_p + l_q$, et son terme est $(p)^k = b$, puisque $k < l_p$. Avec l'hypothèse $\widehat{\mathrm{MP}}(a, b, c)$ et le remplacement, deux introductions, avec les termes $l_p + m$ et $k$, donnent la troisième disjonction de $\Lambda(r, l_p + l_q)$.

Les trois clauses donnent $\widehat{\mathrm{Dem}}(r, c)$ par (ii), et l'on élimine les valeurs et les variables $k$ et $m$, qui ne figurent pas dans la conclusion.

(iv) Soit $n_1$, $n_2$ et $n_3$ les codes de $\varphi \to \psi$, de $\varphi$ et de $\psi$. Par le point (i) de Démonstrations, $\mathrm{MP}(n_2, n_1, n_3)$ est vraie ; $n_3$ code une formule et un énoncé. Le point (iv) de Termes fonctionnels donne donc $\vdash_{\mathsf{PA}} \widehat{\mathrm{MP}}(\underline{n_2}, \underline{n_1}, \underline{n_3})$, $\vdash_{\mathsf{PA}} \widehat{\mathrm{Fm}}(\underline{n_3})$ et $\vdash_{\mathsf{PA}} \widehat{\mathrm{En}}(\underline{n_3})$. Comme $p$ est distincte de $v$, $\mathrm{Pr}_T\,\ulcorner \varphi \to \psi \urcorner$ est $\exists p\ \hat D(p, \underline{n_1})$, et de même pour $\varphi$ et $\psi$.

Sous les hypothèses $\hat D(p, \underline{n_1})$ et $\hat D(q, \underline{n_2})$, pour une variable $q$ nouvelle, (ii) donne $\widehat{\mathrm{Dem}}(p, \underline{n_1})$ et $\widehat{\mathrm{Dem}}(q, \underline{n_2})$. Le point (iii), où l'on substitue les chiffres $\underline{n_2}$, $\underline{n_1}$, $\underline{n_3}$ à $a$, $b$, $c$ (Récurrence dans PA, (iv)), donne $\widehat{\mathrm{Dem}}(\mathrm{aj}(\mathrm{conc}(p, q), \underline{n_3}), \underline{n_3})$ ; avec $\widehat{\mathrm{En}}(\underline{n_3})$, (ii) donne $\hat D$ en ce terme fonctionnel, écrit avec sa valeur $e$, et l'introduction de l'existentiel, avec le terme $e$, donne $\exists p\ \hat D(p, \underline{n_3})$. On élimine $e$, qui n'est libre ni dans les hypothèses ni dans la conclusion. L'hypothèse $\hat D(q, \underline{n_2})$ est $\hat D(p, \underline{n_2})[q/p]$, et $q$ ne figure ni dans $\hat D(p, \underline{n_2})$, ni dans la conclusion, ni dans l'autre hypothèse : la troisième règle du point (i) de Récurrence dans PA, l'élimination avec la variable nouvelle $b := q$, remplace cette hypothèse par $\exists p\ \hat D(p, \underline{n_2})$, c'est-à-dire $\mathrm{Pr}_T\,\ulcorner \varphi \urcorner$. L'élimination ordinaire de $p$, qui n'est libre ni dans cette formule ni dans la conclusion, remplace ensuite $\hat D(p, \underline{n_1})$ par $\mathrm{Pr}_T\,\ulcorner \varphi \to \psi \urcorner$, et deux applications du théorème de la déduction concluent. Pour $\exists y\, \delta$, l'équivalence de (i), instanciée par les chiffres $\underline{n_1}$, $\underline{n_2}$, $\underline{n_3}$, et la règle des tautologies transportent le résultat. Une théorie qui démontre les axiomes de $\mathsf{PA}$ démontre tout ce que démontre $\mathsf{PA}$, par le lemme de remplacement de la preuve du théorème de Craig.