Instanciation formalisée, première et deuxième conditions et introduction de ∃ à plusieurs paramètres

On écrit avec les valeurs et l'on emploie les règles des quantifications bornées strictes de la preuve de Deuxième condition (D2).

(i) Soit $E = \ulcorner \alpha[\dot{\bar y}/\bar x] \urcorner$, $A = \ulcorner (\forall x\, \alpha)[\dot{\bar y}/\bar x] \urcorner$ et $B = \ulcorner \alpha[\dot{\bar y}, \dot y/\bar x, x] \urcorner$, de sorte que $I = \mathrm{cc}(\underline{\langle 2 \rangle}, A, B)$. Comme $x$ est hors de $\bar x$, $G_{\bar x}(\forall x\, \alpha) = (3)(k)\, G_{\bar x}(\alpha)$, et le point (i) de Gabarits à plusieurs places et un calcul clos donnent $A = \mathrm{conc}(\underline{\langle 3, k \rangle}, E)$. Formule. Les $x_i$ sont des paramètres de $\forall x\, \alpha$, et le point (iv) du même nœud donne $\widehat{\mathrm{Fm}}(A)$ et $\widehat{\mathrm{Fm}}(B)$ ; le point (ii) de Formation dans PA donne $\widehat{\mathrm{Fm}}(I)$.

Lecture de $\mathrm{Ax}$. Comme au point (ii) de Instanciation formalisée, avec le témoin $g = 0$ des généralisations, $\widehat{\mathrm{Ax}}(I)$ découle de $\widehat{\mathrm{Fm}}(I)$ et de $$\begin{aligned} &\exists k' < I\ \exists a' < S\,I\ \exists T < S\,I \\ &\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 I = \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' = E$, et, pour $T$, le terme $\mathrm{num}(y)$ si $x$ figure dans $\alpha$, le chiffre $\underline 9 = \underline{\ulcorner 0 \urcorner}$ sinon. Le calcul clos $\underline 8 \leqslant \underline k$ est démontrable, et $\widehat{\mathrm{Fm}}(E)$ découle du point (iv) de Gabarits à plusieurs places. 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, E)$ par le point (iv) de Propriétés locales des lettres, et $\mathrm{Sb}(E, \mathrm{num}(y), \underline k) = B$ par le point (iv) de Substitution lettre à lettre. Dans le second, $\widehat{\mathrm{Tm}}(\underline 9)$ est un calcul clos, $\widehat{\mathrm{Sbl}}(\underline 9, \underline k, E)$ découle du même point (iv), et $\mathrm{Sb}(E, \underline 9, \underline k) = E$ par la dernière assertion de (iv) de Substitution lettre à lettre ; or $B$ est $E$, puisque la place de $x$ ne figure pas dans $G_{\bar x, x}(\alpha)$. Enfin, le calcul clos $\mathrm{conc}(\underline{\langle 2 \rangle}, \underline{\langle 3, k \rangle}) = \mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k)$, les deux membres valant $\langle 2, 3, k \rangle$, et l'associativité (Facteurs dans PA, (ii)) donnent $\mathrm{conc}(\underline{\langle 2 \rangle}, A) = \mathrm{conc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), E)$, d'où $I = \mathrm{cc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), E, \mathrm{Sb}(E, T, \underline k))$ dans les deux cas.

Bornes. Soit $K = \mathrm{conc}(\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k), E)$, de sorte que $I = \mathrm{conc}(K, B)$. Par le point (iii) de Facteurs dans PA, $\mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k) \leqslant K \leqslant I$, $E \leqslant K$ et $B \leqslant I$. Le calcul clos $\underline k < \mathrm{aj}(\underline{\langle 2, 3 \rangle}, \underline k)$ donne $\underline k < I$, et $E \leqslant I$ donne $E < S\,I$. Dans le premier cas, $\mathrm{num}(y) \leqslant B$ par le point (i) de Gabarits à plusieurs places, puisque la place de $x$ figure dans $G_{\bar x, x}(\alpha)$. Dans le second, le calcul clos $\underline 9 \leqslant \underline{\langle 3, k \rangle}$, vrai puisque $\langle 3, k \rangle = 2^7 (2k + 1) \geqslant 2\,176$, et les inégalités $\underline{\langle 3, k \rangle} \leqslant A \leqslant \mathrm{conc}(\underline{\langle 2 \rangle}, A) \leqslant I$, par le même point (iii), donnent $\underline 9 \leqslant I$. Trois introductions des quantifications bornées strictes concluent.

(ii) C'est la preuve du point (iii) de Instanciation formalisée, avec le terme $A$ à la place du chiffre $\underline{n_\forall}$ et $B$ à la place de $\gamma$. Sous l'hypothèse $\widehat{\mathrm{Dem}}(q, A)$, pour une variable $q$ nouvelle, distincte des $y_i$ et de $y$, soit $e = \mathrm{aj}(0, I)$. Par (i) et le point (i) de Instanciation formalisée, $\widehat{\mathrm{Dem}}(e, I)$. La formule naturelle de $\mathrm{MP}(a, b, c) \iff b = \mathrm{cc}(\langle 2 \rangle, a, c)$ donne $\widehat{\mathrm{MP}}(A, I, B)$ par la définition de $I$, et $\widehat{\mathrm{Fm}}(B)$ découle du point (iv) de Gabarits à plusieurs places. Le point (iii) de Deuxième condition (D2), écrit avec des variables distinctes des $y_i$ et de $y$, où l'on substitue $e$, $q$, $A$, $I$ et $B$, donne $\widehat{\mathrm{Dem}}(\mathrm{aj}(\mathrm{conc}(e, q), B), B)$, puis $\mathrm{Prf}_T(B)$ par l'introduction de l'existentiel. On élimine les valeurs ; l'hypothèse est $\widehat{\mathrm{Dem}}(p, A)[q/p]$, et $q$ ne figure ni dans $\widehat{\mathrm{Dem}}(p, A)$ ni dans la conclusion : la troisième règle du point (i) de Récurrence dans PA la remplace par $\mathrm{Prf}_T(A)$, et le théorème de la déduction conclut.

(iii) Par récurrence sur $r$, en métathéorie. Si $T \vdash \psi$, la généralisation, qui vaut pour toute théorie (Récurrence dans PA, (i)), donne $T \vdash \forall x_1 \cdots \forall x_r\, \psi$. Pour $j \leqslant r$, soit $\alpha_j = \forall x_{j+1} \cdots \forall x_r\, \psi$, et montrons $\vdash_{\mathsf{PA}} \mathrm{Prf}_T(\ulcorner \alpha_j[\dot y_1, \dots, \dot y_j/x_1, \dots, x_j] \urcorner)$. Pour $j = 0$, c'est le point (i) de Instanciation formalisée, puisque, sans place, le code est le chiffre $\underline{\ulcorner \alpha_0 \urcorner}$. Pour le pas, $\alpha_j = \forall x_{j+1}\, \alpha_{j+1}$, et $x_1, \dots, x_{j+1}$ sont des paramètres de $\alpha_{j+1}$, puisqu'elles sont distinctes de $x_{j+2}, \dots, x_r$ et ne sont pas quantifiées dans $\psi$ ; (ii), appliqué à $\alpha_{j+1}$, aux paramètres $x_1, \dots, x_j$ et à la variable $x_{j+1}$, et le modus ponens donnent le rang $j + 1$. Pour $j = r$, c'est l'énoncé.

(iv) Par le texte de Gabarits à plusieurs places, $G_{\bar x}({\to}\, \alpha\, \beta) = (2)\, G_{\bar x}(\alpha)\, G_{\bar x}(\beta)$, et le point (i) de ce nœud donne $\ulcorner (\alpha \to \beta)[\dot{\bar y}/\bar x] \urcorner = \mathrm{cc}(\underline{\langle 2 \rangle}, \gamma_\alpha, \gamma_\beta)$, où $\gamma_\alpha$ et $\gamma_\beta$ sont les deux autres codes ; d'où $\widehat{\mathrm{MP}}(\gamma_\alpha, \ulcorner (\alpha \to \beta)[\dot{\bar y}/\bar x] \urcorner, \gamma_\beta)$, et le point (iv) du même nœud donne $\widehat{\mathrm{Fm}}(\gamma_\beta)$. La suite est celle de la seconde formule du point (iv) de Instanciation formalisée : sous les hypothèses $\widehat{\mathrm{Dem}}(p, \cdot)$ et $\widehat{\mathrm{Dem}}(q, \gamma_\alpha)$, pour une variable $q$ nouvelle, la mise bout à bout (Deuxième condition (D2), (iii)) donne $\mathrm{Prf}_T(\gamma_\beta)$ ; on élimine $q$, puis $p$, et l'on applique deux fois le théorème de la déduction.

(v) Soit $u$ une variable qui ne figure pas dans $\alpha$, distincte de $x$ et des $x_i$. Comme $x$ n'est pas quantifiée dans $\alpha$ et que $u$ n'y figure pas, $u$ est substituable à $x$ dans $\alpha$, et le point (iii) de Calcul à variables libres donne $\vdash \alpha[u/x] \to \exists x\, \alpha$, donc $T \vdash \alpha[u/x] \to \exists x\, \alpha$ par le point (i) du même nœud. Les variables $\bar x$ et $u$ sont des paramètres de cette formule, où seules $x$ et les variables quantifiées de $\alpha$ sont quantifiées. Par (iii) et (iv), avec les valeurs $\bar y$ et $y$, il vient $$\begin{aligned} \vdash_{\mathsf{PA}} {}&\mathrm{Prf}_T\big(\ulcorner \alpha[u/x][\dot{\bar y}, \dot y/\bar x, u] \urcorner\big) \\ &\to \mathrm{Prf}_T\big(\ulcorner (\exists x\, \alpha)[\dot{\bar y}, \dot y/\bar x, u] \urcorner\big). \end{aligned}$$ Par le texte de Gabarits à plusieurs places, le premier code est $\ulcorner \alpha[\dot{\bar y}, \dot y/\bar x, x] \urcorner$, puisque renommer un paramètre ne change pas le gabarit, et le second est $\ulcorner (\exists x\, \alpha)[\dot{\bar y}/\bar x] \urcorner$, puisque $u$ ne figure pas dans $\exists x\, \alpha$.

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.