Variantes propres et Σ₁-complétude formalisée dans l'arithmétique de Peano

(i) Par récurrence sur la construction des formules Δ₀, l'énoncé portant sur toutes les parties finies $V$ à la fois. Une formule atomique est propre, sans variable quantifiée. Si $\delta = \neg\delta_1$, on prend $\neg\delta'_1$, où $\delta'_1$ est donnée par l'hypothèse de récurrence. Si $\delta = (\delta_1 \to \delta_2)$, soit $L$ l'ensemble des variables libres de $\delta$ ; on prend $\delta'_1$ pour la partie $V \cup L$, puis $\delta'_2$ pour la partie $V \cup L$ augmentée des variables quantifiées de $\delta'_1$, et $\delta' = (\delta'_1 \to \delta'_2)$ : chaque variable y est quantifiée au plus une fois, aucune variable de $L$ n'y est quantifiée, et la règle des tautologies donne $\vdash \delta \leftrightarrow \delta'$.

Soit enfin $\delta = \forall x\, (\exists z\, (z + x = t) \to \psi)$. Soit $x'$ et $z'$ deux variables distinctes, hors de $V$, qui ne figurent pas dans $\delta$. Par le point (i) de Σ₁-complétude, $\psi[x'/x]$ est Δ₀, puisque $x'$ n'est pas quantifiée dans $\psi$ ; soit $\psi'$ la formule que donne l'hypothèse de récurrence pour $\psi[x'/x]$ et la partie $V \cup L \cup \{x, z, x', z'\}$, et $\delta' = \forall x'\, (\exists z'\, (z' + x' = t) \to \psi')$. C'est une quantification bornée d'une formule Δ₀, puisque $t$ ne contient ni $x'$ ni $z'$. Elle est propre : $x'$ et $z'$ y sont quantifiées une fois chacune, les variables quantifiées de $\psi'$ évitent $x'$, $z'$ et $L$, et les variables libres de $\delta'$ sont celles de $t$ et celles de $\psi'$ autres que $x'$, c'est-à-dire celles de $\delta$.

Équivalence. Notons $B = \exists z\, (z + x = t)$. Sous l'hypothèse $\delta$, l'axiome (2), avec le terme $x'$, substituable puisqu'il ne figure pas dans $\delta$, donne $B[x'/x] \to \psi[x'/x]$, où $B[x'/x] = \exists z\, (z + x' = t)$ puisque $x$ ne figure pas dans $t$ ; le renommage du point (iii) de Calcul à variables libres donne $\exists z'\, (z' + x' = t) \to \exists z\, (z + x' = t)$, puisque $z$ ne figure pas dans $z' + x' = t$, et l'hypothèse de récurrence donne $\psi[x'/x] \to \psi'$. La règle des tautologies, puis la généralisation en $x'$, qui n'est pas libre dans $\delta$, donnent $\delta \to \delta'$. Réciproquement, sous l'hypothèse $\delta'$, l'axiome (2), avec le terme $x$, substituable puisque $x$ n'est quantifiée ni dans $\psi'$ ni ailleurs dans $\delta'$, donne $\exists z'\, (z' + x = t) \to \psi'[x/x']$. Les occurrences libres de $x'$ dans $\psi[x'/x]$ sont aux places des occurrences libres de $x$ dans $\psi$, dont aucune n'est dans une sous-formule $\forall x\, \chi$ ; ainsi $x$ est substituable à $x'$ dans $\psi[x'/x]$, et $\psi[x'/x][x/x'] = \psi$, comme dans la preuve du renommage citée. L'instanciation du point (ii) de Calcul à variables libres, appliquée à $\psi' \to \psi[x'/x]$, donne $\psi'[x/x'] \to \psi$, et le renommage donne $B \to \exists z'\, (z' + x = t)$ ; la règle des tautologies et la généralisation en $x$, qui n'est pas libre dans $\delta'$, donnent $\delta' \to \delta$.

(ii) Par récurrence sur la construction de $\delta$, en métathéorie, les deux formules à la fois ; les variables nouvelles sont prises distinctes de $p$. On note $\mathrm D1$, $\mathrm D2$ et $\exists$ les points (iii), (iv) et (v) de Instanciation à plusieurs paramètres, que l'on applique à des théorèmes de $\mathsf{PA}$, donc de $T$, dont les variables $\bar x$ sont des paramètres ; les égalités de codes sont celles des points (ii) et (iii) de Gabarits à plusieurs places.

Formules atomiques. C'est le point (iv) de Valeurs des termes sous Prf.

Négation. Si $\delta = \neg\delta_1$, la première formule est la seconde pour $\delta_1$. Pour la seconde, sous l'hypothèse $\neg\neg\delta_1$, on a $\delta_1$, puis $\mathrm{Prf}_T(\ulcorner \delta_1(\dot{\bar x}) \urcorner)$, et $\mathrm D1$ et $\mathrm D2$, appliqués à l'instance de tautologie $\delta_1 \to \neg\neg\delta_1$, donnent $\mathrm{Prf}_T(\ulcorner \neg\neg\delta_1(\dot{\bar x}) \urcorner)$.

Implication. Si $\delta = (\delta_1 \to \delta_2)$, la règle des tautologies donne $\neg\delta_1$ ou $\delta_2$. Dans le premier cas, l'hypothèse de récurrence pour $\delta_1$, et $\mathrm D1$ et $\mathrm D2$ appliqués à $\neg\delta_1 \to (\delta_1 \to \delta_2)$, concluent ; dans le second, on emploie $\delta_2 \to (\delta_1 \to \delta_2)$. Sous l'hypothèse $\neg(\delta_1 \to \delta_2)$, on a $\delta_1$ et $\neg\delta_2$, et l'on emploie $\delta_1 \to (\neg\delta_2 \to \neg(\delta_1 \to \delta_2))$. Les variables libres de $\delta_1$ et de $\delta_2$ sont parmi les $x_i$, et aucune de celles-ci n'est quantifiée dans $\delta_1$ ou dans $\delta_2$.

Quantification bornée. Soit $\delta = \forall x\, (B \to \psi)$, avec $B = \exists z\, (z + x = t)$. Comme $\delta$ est propre, $x$ et $z$ ne sont pas parmi les $x_i$, $x$ n'est pas quantifiée dans $\psi$, $z$ n'est pas libre dans $\psi$, et $\psi$ est propre ; ses variables libres sont parmi $\bar x$ et $x$, et l'hypothèse de récurrence s'applique à $\psi$ avec les paramètres $\bar x, x$. Soit $w$ une variable nouvelle, distincte de $p$, et $\delta_w = \forall x\, (\exists z\, (z + x = w) \to \psi)$, de sorte que $\delta_w[t/w] = \delta$ et que $\bar x, w$ sont des paramètres de $\delta_w$.

Montrons, par récurrence sur $w$, la formule $\delta_w \to \mathrm{Prf}_T(\ulcorner \delta_w[\dot{\bar x}, \dot w/\bar x, w] \urcorner)$. Pour $0$, le point (vii) (d) de Ordre dans PA donne $\delta_0 \leftrightarrow \psi[0/x]$. L'hypothèse de récurrence pour $\psi$, où l'on substitue $0$ à $x$ (Termes fonctionnels, (ii) (b)), donne $\psi[0/x] \to \mathrm{Prf}_T(\ulcorner \psi \urcorner_{\bar x, x}(\mathrm{num}(\bar x), \mathrm{num}(0)))$, et ce code est $\ulcorner \psi[0/x](\dot{\bar x}) \urcorner$. Le même point (vii) (d) donne $\psi[0/x] \to \delta_0$, et $\mathrm D1$ et $\mathrm D2$, avec les paramètres $\bar x$, donnent $\mathrm{Prf}_T(\ulcorner \delta_0(\dot{\bar x}) \urcorner)$, dont le code est celui de $\delta_w$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(0)$.

Pour le pas, sous l'hypothèse de récurrence et sous $\delta_{S\,w}$, le point (vii) (d) de Ordre dans PA, permis puisque $S\,w$ est substituable à $x$ dans $\psi$, donne $\delta_w$ et $\psi[S\,w/x]$. L'hypothèse de récurrence donne $\mathrm{Prf}_T(\ulcorner \delta_w[\dot{\bar x}, \dot w] \urcorner)$ ; celle qui porte sur $\psi$, où l'on substitue $S\,w$ à $x$, donne le code de $\psi$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(S\,w)$, qui est celui de $\psi[S\,w/x]$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(w)$. Le même point (vii) (d) donne $\delta_w \to (\psi[S\,w/x] \to \delta_{S\,w})$, formule dont $\bar x, w$ sont des paramètres, et $\mathrm D1$ et deux applications de $\mathrm D2$ donnent le code de $\delta_{S\,w}$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(w)$, c'est-à-dire, par le point (iii) de Gabarits à plusieurs places avec $s = S\,w$, celui de $\delta_w$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(S\,w)$. La récurrence (Récurrence dans PA, (iii)) conclut.

Substituons $t$ à $w$ : $t$ y est substituable, puisqu'il ne contient ni $x$ ni $z$, et l'on obtient $\delta \to \mathrm{Prf}_T(\ulcorner \delta_w \urcorner_{\bar x, w}(\mathrm{num}(\bar x), \mathrm{num}(t)))$. Le point (iii) de Valeurs des termes sous Prf donne le code de $t = w$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(t)$, et $\mathrm D1$ et $\mathrm D2$, appliqués à $t = w \to (\delta_w \to \delta)$, que donnent le remplacement d'un terme (Calcul à variables libres, (v)) et la symétrie, avec les places $\bar x, w$ et les valeurs $\bar x, t$, donnent $\mathrm{Prf}_T(\ulcorner \delta(\dot{\bar x}) \urcorner)$, la place $w$ ne figurant pas dans $\delta$.

Négation d'une quantification bornée. Sous l'hypothèse $\neg\delta$, la règle des tautologies et la monotonie (Récurrence dans PA, (ii)) donnent $\neg\forall x\, \neg\neg(B \to \psi)$, et l'élimination avec une variable nouvelle $a$, distincte de $p$ (troisième règle du point (i) du même nœud), permet de raisonner sous $B[a/x]$ et $\neg\psi[a/x]$, puis, par l'élimination de $z$ avec une variable nouvelle $c$, sous $c + a = t$. Soit $u$ une variable nouvelle. Le point (iv) de Valeurs des termes sous Prf, appliqué à la formule atomique $z + u = t$ avec les paramètres $\bar x, z, u$, où l'on substitue $c$ et $a$ à $z$ et $u$, donne le code de $z + u = t$ rempli par $\mathrm{num}(\bar x)$, $\mathrm{num}(c)$ et $\mathrm{num}(a)$ ; le point $\exists$, avec la variable quantifiée $z$ et les paramètres $\bar x, u$, donne celui de $B[u/x] = \exists z\, (z + u = t)$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(a)$. L'hypothèse de récurrence pour $\psi$, où l'on substitue $a$ à $x$, donne celui de $\neg\psi$ rempli par $\mathrm{num}(\bar x)$ et $\mathrm{num}(a)$, qui est le code de $\neg\psi[u/x]$ avec les places $\bar x, u$, puisque renommer un paramètre ne change pas le gabarit. Enfin, l'axiome (2), avec le terme $u$, et la règle des tautologies donnent $\vdash B[u/x] \to (\neg\psi[u/x] \to \neg\delta)$, dont $\bar x, u$ sont des paramètres ; $\mathrm D1$ et deux applications de $\mathrm D2$ donnent le code de $\neg\delta$, où la place $u$ ne figure pas. On élimine $c$, puis $a$, qui ne figurent pas dans la conclusion.

(iii) Le point (ii), avec les paramètres $\bar x, y$, donne $\delta \to \mathrm{Prf}_T(\ulcorner \delta[\dot{\bar x}, \dot y/\bar x, y] \urcorner)$, et le point (v) de Instanciation à plusieurs paramètres, où $\bar x$ et $y$ sont des paramètres de $\delta$, donne $\mathrm{Prf}_T(\ulcorner (\exists y\, \delta)(\dot{\bar x}) \urcorner)$. L'élimination de $y$, qui n'est libre ni dans cette conclusion ni dans aucune hypothèse, conclut.