Collection bornée et forme Σ₁ dans l'arithmétique de Peano

(i) Sens réciproque. Sous les hypothèses $\forall x \leqslant t\ \exists y \leqslant w\ \delta$ et $x \leqslant t$, le point (vii) (a) de Ordre dans PA, avec le terme $x$, donne $\exists y \leqslant w\ \delta$, puis $\exists y\, (y \leqslant w \wedge \delta)$ par le point (vii) (c), et $\exists y\, \delta$ par la monotonie de Récurrence dans PA, (ii). Le point (vii) (b) donne $\forall x \leqslant t\ \exists y\, \delta$, et l'élimination de $w$, qui n'est libre ni dans cette formule ni dans $t$, conclut.

Sens direct. Soit $v$ une variable qui ne figure ni dans $\delta$ ni dans $t$, distincte de $x$, $y$, $w$ et des variables liées des bornes. Notons $\theta(v)$ la formule $\forall x \leqslant v\ \exists y\, \delta \to \exists w\, \forall x \leqslant v\ \exists y \leqslant w\ \delta$, et montrons $\vdash_{\mathsf{PA}} \theta(v)$ par récurrence sur $v$. Les occurrences libres de $v$ dans $\theta(v)$ ne sont que dans les bornes $\forall x \leqslant v$, sous $\forall x$, sous la variable liée de la borne et, pour la seconde, sous $\exists w$ : aucune variable de $t$ n'y est quantifiée, et l'axiome (2) donnera, avec le terme $t$, la formule annoncée. Le terme $S\,v$ est substituable à $x$ dans $\exists y\, \delta$, puisque $v$ n'y figure pas ; on emploie le point (vii) (d) de Ordre dans PA avec la formule $\exists y\, \delta$, puis avec la formule $\exists y \leqslant w\ \delta$, et l'on note $\delta'$ la formule $\delta[S\,v/x]$.

Cas $0$. Sous l'hypothèse $\forall x \leqslant 0\ \exists y\, \delta$, le point (vii) (d) donne $\exists y\, \delta[0/x]$, et l'élimination avec une variable nouvelle $b$ donne $\delta[0/x][b/y]$. Par le point (vii) (a), avec $b \leqslant b$, il vient $\exists y \leqslant b\ \delta[0/x]$, qui est $(\exists y \leqslant b\ \delta)[0/x]$, puis $\forall x \leqslant 0\ \exists y \leqslant b\ \delta$ par le point (vii) (d). C'est la formule $(\forall x \leqslant 0\ \exists y \leqslant w\ \delta)[b/w]$, puisque $w$ ne figure pas dans $\delta$, et l'introduction de l'existentiel avec le terme $b$ donne la conclusion.

Pas. Sous les hypothèses $\theta(v)$ et $\forall x \leqslant S\,v\ \exists y\, \delta$, le point (vii) (d) donne $\forall x \leqslant v\ \exists y\, \delta$ et $\exists y\, \delta'$. La première et $\theta(v)$ donnent $\exists w\, \forall x \leqslant v\ \exists y \leqslant w\ \delta$, et l'élimination avec des variables nouvelles $c$ et $b$ donne $\forall x \leqslant v\ \exists y \leqslant c\ \delta$ et $\delta'[b/y]$. Par le point (i) de Ordre dans PA, $c \leqslant c + b$ et $b \leqslant c + b$. Le point (vii) (e), appliqué sous la borne $\forall x \leqslant v$ à l'implication $\exists y \leqslant c\ \delta \to \exists y \leqslant c + b\ \delta$, donne $\forall x \leqslant v\ \exists y \leqslant c + b\ \delta$, et le point (vii) (a) donne $\exists y \leqslant c + b\ \delta'$. Le point (vii) (d) réunit ces deux formules en $\forall x \leqslant S\,v\ \exists y \leqslant c + b\ \delta$, et l'introduction de l'existentiel avec le terme $c + b$, substituable à $w$ puisque $c$ et $b$ sont nouvelles, donne $\exists w\, \forall x \leqslant S\,v\ \exists y \leqslant w\ \delta$. On élimine $b$ et $c$, qui ne sont libres ni dans les hypothèses ni dans la conclusion, et le théorème de la déduction donne $\theta(S\,v)$ sous l'hypothèse $\theta(v)$. Le cas $0$ se décharge de même, et le point (iii) de Récurrence dans PA donne $\vdash_{\mathsf{PA}} \forall v\, \theta(v)$.

(ii) On reprend la récurrence sur la construction de $\mathcal S$ de la preuve citée, avec ses conditions sur les variables, en démontrant chaque équivalence dans $\mathsf{PA}$. On emploie ces trois faits. Si $\vdash_{\mathsf{PA}} \varphi_1 \leftrightarrow \psi_1$ et $\vdash_{\mathsf{PA}} \varphi_2 \leftrightarrow \psi_2$, alors $\varphi_1 \wedge \varphi_2$ et $\varphi_1 \vee \varphi_2$ équivalent à $\psi_1 \wedge \psi_2$ et $\psi_1 \vee \psi_2$, par la règle des tautologies, et $\exists x\, \varphi_1$, $\forall x \leqslant t\ \varphi_1$ à $\exists x\, \psi_1$, $\forall x \leqslant t\ \psi_1$, par la monotonie de Récurrence dans PA, (ii), et le point (vii) (e) de Ordre dans PA. Si $y'$ ne figure pas dans $\delta$, alors $\vdash \exists y\, \delta \leftrightarrow \exists y'\, \delta[y'/y]$ : un sens est le renommage du point (iii) de Calcul à variables libres ; pour l'autre, l'introduction avec le terme $y'$ donne $\delta[y'/y] \to \exists y\, \delta$, et l'élimination de $y'$, qui n'est pas libre dans $\exists y\, \delta$, conclut. Enfin, si $y$ ne figure pas dans la formule Δ₀ $\delta$, l'introduction avec le terme $y$ et l'élimination donnent $\vdash \delta \leftrightarrow \exists y\, \delta$.

Conjonction. Il reste à voir $\vdash_{\mathsf{PA}} (\exists y_1\, \delta_1 \wedge \exists y_2\, \delta_2) \leftrightarrow \exists w\, \exists y_1 \leqslant w\ \exists y_2 \leqslant w\ (\delta_1 \wedge \delta_2)$, sous les conditions de la preuve citée : $y_1$, $y_2$, $w$ distinctes, $y_1$ absente de $\delta_2$, $y_2$ absente de $\delta_1$, $w$ et les variables liées des bornes nouvelles. Sous les hypothèses $\delta_1[a/y_1]$ et $\delta_2[b/y_2]$, avec des variables nouvelles $a$ et $b$ : le point (vii) (a) de Ordre dans PA, avec $b \leqslant a + b$, donne $\exists y_2 \leqslant a + b\ (\delta_1[a/y_1] \wedge \delta_2)$, qui est $(\exists y_2 \leqslant a + b\ (\delta_1 \wedge \delta_2))[a/y_1]$, puisque $y_1$ ne figure ni dans $\delta_2$ ni dans la borne, et le même point, avec $a \leqslant a + b$, donne $\exists y_1 \leqslant a + b\ \exists y_2 \leqslant a + b\ (\delta_1 \wedge \delta_2)$ ; l'introduction avec le terme $a + b$, substituable à $w$, et l'élimination de $b$ et $a$ donnent le sens direct. Réciproquement, le point (vii) (c) et la monotonie donnent $\vdash \exists y_2 \leqslant w\ (\delta_1 \wedge \delta_2) \to \exists y_2\, (\delta_1 \wedge \delta_2)$ ; le point (vii) (e), qui fait passer cette implication sous $\exists y_1 \leqslant w$, puis de nouveau le point (vii) (c) et la monotonie, donnent $\vdash_{\mathsf{PA}} \exists y_1 \leqslant w\ \exists y_2 \leqslant w\ (\delta_1 \wedge \delta_2) \to \exists y_1\, \exists y_2\, (\delta_1 \wedge \delta_2)$ ; sous l'hypothèse $\delta_1 \wedge \delta_2$, l'introduction donne $\exists y_1\, \delta_1 \wedge \exists y_2\, \delta_2$, formule où ni $y_1$ ni $y_2$ ne sont libres, et deux éliminations, puis celle de $w$, concluent.

Disjonction. Pour $w$ nouvelle, $\exists y_1\, \delta_1 \to \exists w\, \delta_1[w/y_1]$ par le renommage, et $\exists w\, \delta_1[w/y_1] \to \exists w\, (\delta_1[w/y_1] \vee \delta_2[w/y_2])$ par la monotonie, et de même pour $\delta_2$ ; le raisonnement par cas donne le sens direct. Réciproquement, l'introduction avec le terme $w$ donne $\delta_1[w/y_1] \to \exists y_1\, \delta_1$ et $\delta_2[w/y_2] \to \exists y_2\, \delta_2$, et l'élimination de $w$ conclut.

Quantification existentielle. Pour $x \neq y_1$ et $w$ nouvelle, $\vdash_{\mathsf{PA}} \exists x\, \exists y_1\, \delta_1 \leftrightarrow \exists w\, \exists x \leqslant w\ \exists y_1 \leqslant w\ \delta_1$ se démontre comme la conjonction, sous les hypothèses $\delta_1[a/x][b/y_1]$, avec le témoin $a + b$.

Quantification bornée. Pour $\varphi = \forall x \leqslant t\ \varphi_1$, avec $\varphi_1$ équivalente à $\exists y_1\, \delta_1$, et $y_1$, $w$ absentes de $t$ et distinctes de $x$ et de la variable liée de la borne, c'est le point (i).

Dans chaque cas, la formule obtenue est celle de la preuve citée, et ses variables libres sont celles qui y sont indiquées.