Axiomes du groupe (2), instanciation formalisée, et première et deuxième conditions à un paramètre

On emploie les règles d'introduction et d'élimination des quantifications bornées strictes de la preuve de Deuxième condition (D2), et l'on écrit avec les valeurs, au sens de Termes fonctionnels.

(i) La formule $\widehat{\mathrm{Dem}}(p, v)$ est dans $\mathcal S$ (Relations p.r. dans PA), et $\mathcal S$ est stable par la quantification existentielle. Comme une formule naturelle définit sa relation, $\mathrm{Prf}_T$ est satisfaite sous une valuation qui vaut $c$ en $v$ si et seulement s'il existe une démonstration formelle, à partir de $T'$, de la formule de code $c$, c'est-à-dire, par le point (i) du théorème de Craig, si $c$ code une formule que $T$ démontre. Si $T \vdash \psi$, soit $q$ le code d'une démonstration formelle de $\psi$ à partir de $T'$ ; le point (iv) de Termes fonctionnels donne $\vdash_{\mathsf{PA}} \widehat{\mathrm{Dem}}(\underline q, \underline{\ulcorner \psi \urcorner})$, et l'introduction de l'existentiel donne $\vdash_{\mathsf{PA}} \mathrm{Prf}_T\,\ulcorner \psi \urcorner$. Pour un énoncé $\sigma$, de code $s$, le point (ii) de Deuxième condition (D2), où l'on substitue $\underline s$ à $c$, donne $\hat D(p, \underline s) \leftrightarrow (\widehat{\mathrm{Dem}}(p, \underline s) \wedge \widehat{\mathrm{En}}(\underline s))$, et le calcul clos $\widehat{\mathrm{En}}(\underline s)$ donne $\hat D(p, \underline s) \leftrightarrow \widehat{\mathrm{Dem}}(p, \underline s)$ ; la monotonie (Récurrence dans PA, (ii)), dans les deux sens, donne l'équivalence de $\mathrm{Pr}_T\,\ulcorner \sigma \urcorner$ et de $\mathrm{Prf}_T\,\ulcorner \sigma \urcorner$.

Démonstrations d'une ligne. Soit $e = \mathrm{aj}(0, b)$. Par le point (ii) de Longueur dans PA, $\mathrm{lg}(e) = S\,\mathrm{lg}(0) = S\,0$, donc $S\,0 \leqslant \mathrm{lg}(e)$, et, par le point (iii) du même nœud et le point (iii) de Fonctions usuelles dans PA, $(e)^{S\,0 \mathbin{\dot{-}} S\,0} = (e)^0 = (e)^{\mathrm{lg}(0)} = b$. Par le point (i) (c) de Modules de Gödel, avec la clause démontrable $\forall j < 0$, la clause bornée du dépliement de $\widehat{\mathrm{Dem}}(e, b)$ (Deuxième condition (D2), (ii)) équivaut à $\Lambda(e, 0)$, c'est-à-dire, par le remplacement, à $\widehat{\mathrm{Fm}}(b) \wedge \big(\widehat{\mathrm{Ax}}(b) \vee (\widehat{\mathrm{Ax}}_{T'}(b) \vee \exists i < 0\ \exists i' < 0\ \cdots)\big)$, qui découle de l'hypothèse par la règle des tautologies.

(ii) Soit $n = \ulcorner \alpha \urcorner$, $n_\forall = \ulcorner \forall x\, \alpha \urcorner$, $\gamma$ la valeur de $\ulcorner \alpha[\dot y/x] \urcorner$ et $M$ celle de $I_\alpha(y)$, de sorte que $M = \mathrm{cc}(\underline{\langle 2 \rangle}, \underline{n_\forall}, \gamma)$. Formule. Le calcul clos $\widehat{\mathrm{Fm}}(\underline{n_\forall})$, le point (iii) de Formules des instances, qui donne $\widehat{\mathrm{Fm}}(\gamma)$, et le point (ii) de Formation dans PA donnent $\widehat{\mathrm{Fm}}(M)$.

Lecture de $\mathrm{Ax}$. Comme au point (ii) de Deuxième condition (D2), la formule naturelle se lit clause par clause : $\widehat{\mathrm{Ax}}(M)$ découle de la formule obtenue avec le témoin $g = 0$ de la quantification bornée sur les généralisations, puisque $0 < S\,\mathrm{lg}(M)$, que $2 \cdot 0$ vaut $0$, que la clause $\forall m < 0$ est démontrable et que $\mathrm{sm}(M, 0, \mathrm{lg}(M)) = M$ (Facteurs dans PA, (iv)). Il suffit donc d'établir le disjonct du groupe (2) en $M$, qui découle de $\widehat{\mathrm{Fm}}(M)$ et de $$\begin{aligned} &\exists k' < M\ \exists a' < S\,M\ \exists T < S\,M \\ &\quad \big(\underline 8 \leqslant k' \wedge \widehat{\mathrm{Fm}}(a') \wedge \widehat{\mathrm{Tm}}(T) \\ &\quad \wedge \widehat{\mathrm{Sbl}}(T, k', a') \\ &\quad \wedge M = \mathrm{cc}\big(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, k'), \\ &\qquad a', \mathrm{Sb}(a', T, k')\big)\big). \end{aligned}$$

Témoins. On prend $k' = \underline k$ et $a' = \underline n$, et, pour $T$, le terme $\mathrm{num}(y)$ si $x$ est libre dans $\alpha$, le chiffre $\underline{\ulcorner x \urcorner}$ sinon. Les calculs clos $\underline 8 \leqslant \underline k$ et $\widehat{\mathrm{Fm}}(\underline n)$ sont démontrables. Dans le premier cas, $\widehat{\mathrm{Tm}}(\mathrm{num}(y))$ par le point (iii) de Formation dans PA, $\widehat{\mathrm{Sbl}}(\mathrm{num}(y), \underline k, \underline n)$ par le point (iii) de Formules des instances, et $\gamma = \mathrm{Sb}(\underline n, \mathrm{num}(y), \underline k)$ par définition. Dans le second, $\widehat{\mathrm{Tm}}(\underline{\ulcorner x \urcorner})$ et $\widehat{\mathrm{Sbl}}(\underline{\ulcorner x \urcorner}, \underline k, \underline n)$ sont des calculs clos, puisque $x$ est substituable à elle-même ; et $\gamma = \underline n$ par le point (iii) de Formules des instances, tandis que $\mathrm{Sb}(\underline n, \underline{\ulcorner x \urcorner}, \underline k) = \underline n$ par un calcul clos, puisque $\alpha[x/x] = \alpha$. Dans les deux cas, $\mathrm{Sb}(\underline n, T, \underline k) = \gamma$. Enfin, le calcul clos $\mathrm{conc}(\underline{\langle 2 \rangle}, \underline{n_\forall}) =\mathrm{conc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), \underline n)$, puisque les deux membres codent le mot ${\to}\, \forall x\, \alpha$, donne $M = \mathrm{cc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), \underline n, \mathrm{Sb}(\underline n, T, \underline k))$.

Bornes. Soit $K = \mathrm{conc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), \underline n)$, de sorte que $M = \mathrm{conc}(K, \gamma)$. Par le point (iii) de Facteurs dans PA, $\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k) \leqslant K \leqslant M$ et $\underline n \leqslant K$, et $\gamma \leqslant M$. Le calcul clos $\underline k < \mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k)$, vrai puisque $2^{224}(2k + 1) > k$, donne $\underline k < M$, par la transitivité mixte. On a $\underline n \leqslant M$, c'est-à-dire $\underline n < S\,M$ (Ordre dans PA, (v)). Dans le premier cas, $\mathrm{num}(y) \leqslant \gamma \leqslant M$, par le point (iii) de Formules des instances ; dans le second, le calcul clos $\underline{\ulcorner x \urcorner} \leqslant \mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k)$, vrai puisque $\ulcorner x \urcorner = 2k + 1$, donne $\underline{\ulcorner x \urcorner} \leqslant M$. Trois introductions des quantifications bornées strictes concluent.

(iii) Raisonnons sous l'hypothèse $\widehat{\mathrm{Dem}}(q, \underline{n_\forall})$, pour une variable $q$ nouvelle, distincte de $y$, et soit $e = \mathrm{aj}(0, M)$. Par (i) et (ii), $\widehat{\mathrm{Dem}}(e, M)$. La relation $\mathrm{MP}(a, b, c)$ est $b = \mathrm{cc}(\langle 2 \rangle, a, c)$ (Démonstrations, (i)), et sa formule naturelle équivaut à cette égalité de termes fonctionnels par le point (ii) de Relations p.r. dans PA et le point (ii) (d) de Termes fonctionnels : $\widehat{\mathrm{MP}}(\underline{n_\forall}, M, \gamma)$ découle de la définition de $M$. Avec $\widehat{\mathrm{Fm}}(\gamma)$, le point (iii) de Deuxième condition (D2), écrit avec des variables $p$, $q$, $a$, $b$, $c$ distinctes de $y$ et des valeurs introduites, où l'on substitue $e$, $q$, $\underline{n_\forall}$, $M$ et $\gamma$ à $p$, $q$, $a$, $b$ et $c$ (Termes fonctionnels, (ii) (b)), les variables de chaque terme substitué n'étant pas parmi celles qu'on substitue ensuite, donne $\widehat{\mathrm{Dem}}(\mathrm{aj}(\mathrm{conc}(e, q), \gamma), \gamma)$, et l'introduction de l'existentiel, avec la valeur de ce terme fonctionnel, donne $\mathrm{Prf}_T(\gamma)$. On élimine les valeurs. L'hypothèse est $\widehat{\mathrm{Dem}}(p, \underline{n_\forall})[q/p]$, et $q$ ne figure ni dans $\widehat{\mathrm{Dem}}(p, \underline{n_\forall})$ ni dans la conclusion $\mathrm{Prf}_T(\gamma)$, où $p$ est liée et où $y$, distincte de $p$, reste libre : la troisième règle du point (i) de Récurrence dans PA la remplace par $\mathrm{Prf}_T\,\ulcorner \forall x\, \alpha \urcorner$, et le théorème de la déduction conclut.

(iv) Si $T \vdash \psi$, la généralisation, qui vaut pour toute théorie (Récurrence dans PA, (i)), donne $T \vdash \forall x\, \psi$ ; (i) donne $\vdash_{\mathsf{PA}} \mathrm{Prf}_T\,\ulcorner \forall x\, \psi \urcorner$, et (iii) et le modus ponens donnent $\vdash_{\mathsf{PA}} \mathrm{Prf}_T(\ulcorner \psi[\dot y/x] \urcorner)$.

Pour la seconde formule, notons $\gamma_\alpha$, $\gamma_\beta$ et $\gamma_{\alpha \to \beta}$ les valeurs des trois codes. Par le point (iii) de Substitution dépliée, $\gamma_{\alpha \to \beta} = \mathrm{cc}(\underline{\langle 2 \rangle}, \gamma_\alpha, \gamma_\beta)$, d'où $\widehat{\mathrm{MP}}(\gamma_\alpha, \gamma_{\alpha \to \beta}, \gamma_\beta)$, et le point (iii) de Formules des instances donne $\widehat{\mathrm{Fm}}(\gamma_\beta)$. Sous les hypothèses $\widehat{\mathrm{Dem}}(p, \gamma_{\alpha \to \beta})$ et $\widehat{\mathrm{Dem}}(q, \gamma_\alpha)$, pour une variable $q$ nouvelle, distincte de $y$, le point (iii) de Deuxième condition (D2) donne $\widehat{\mathrm{Dem}}(\mathrm{aj}(\mathrm{conc}(p, q), \gamma_\beta), \gamma_\beta)$, puis $\mathrm{Prf}_T(\gamma_\beta)$. On élimine $q$, puis $p$, et l'on applique deux fois le théorème de la déduction, exactement comme au point (iv) du même nœud.

(v) Par le point (iii) de Calcul à variables libres, avec le terme $x$, substituable à $x$ dans $\alpha$, on a $\vdash \alpha \to \exists x\, \alpha$, donc $T \vdash \alpha \to \exists x\, \alpha$ par le point (i) du même nœud. Comme $x$ n'est pas libre dans $\exists x\, \alpha = \neg\forall x\, \neg\alpha$, le point (ii) de Substitution dépliée donne $\ulcorner (\exists x\, \alpha)[\dot y/x] \urcorner = \underline{\ulcorner \exists x\, \alpha \urcorner}$. La première formule de (iv), appliquée à $\psi = \alpha \to \exists x\, \alpha$, puis la seconde, avec $\beta = \exists x\, \alpha$, donnent $\vdash_{\mathsf{PA}} \mathrm{Prf}_T(\ulcorner \alpha[\dot y/x] \urcorner) \to \mathrm{Prf}_T(\underline{\ulcorner \exists x\, \alpha \urcorner})$, par le remplacement.

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.