Plus petit élément, récurrence forte et division euclidienne dans l'arithmétique de Peano

(i) Notons $M$ la formule $\forall y \leqslant x\ (y = x \vee \neg\varphi[y/x])$ et $C$ la formule $\exists x\, (\varphi \wedge M)$. La variable $x$ n'est pas libre dans $\varphi[y/x]$ ; pour un terme $w$ substituable à $x$ dans $\varphi$ et où ne figurent ni $y$ ni $u$, $w$ est substituable à $x$ dans $\varphi \wedge M$, et $(\varphi \wedge M)[w/x]$ est $\varphi[w/x] \wedge \forall y \leqslant w\ (y = w \vee \neg\varphi[y/x])$. Comme $\neg C$ est $\neg\neg\forall x\, \neg(\varphi \wedge M)$, l'instance $\neg\neg P \to P$ et l'axiome (2) donnent $\neg C \to \neg(\varphi \wedge M)[w/x]$.

Soit $v$ une variable qui ne figure pas dans $\varphi$ et distincte de $x$, $y$ et $u$, et $\chi = \forall y \leqslant v\ \neg\varphi[y/x]$. Montrons $\{\neg C\} \vdash_{\mathsf{PA}} \chi$ par récurrence sur $v$, qui n'est pas libre dans $\neg C$ ; le terme $S\,v$ est substituable à $y$ dans $\neg\varphi[y/x]$, puisque $v$ n'y figure pas, et $\neg\varphi[y/x][S\,v/y] = \neg\varphi[S\,v/x]$.

Cas $0$. Par le point (vii) (d) de Ordre dans PA, $\chi[0/v] = \forall y \leqslant 0\ \neg\varphi[y/x]$ équivaut à $\neg\varphi[0/x]$. Sous les hypothèses $\neg C$ et $\varphi[0/x]$, le même point donne $\forall y \leqslant 0\ (y = 0 \vee \neg\varphi[y/x])$, qui équivaut à $0 = 0 \vee \neg\varphi[0/x]$, démontrable ; avec $w = 0$, cela contredit $\neg C$. Donc $\{\neg C\} \vdash_{\mathsf{PA}} \neg\varphi[0/x]$, puis $\chi[0/v]$.

Pas. Sous les hypothèses $\neg C$ et $\chi$, il suffit, par le point (vii) (d) de Ordre dans PA, de démontrer $\neg\varphi[S\,v/x]$. Sous l'hypothèse supplémentaire $\varphi[S\,v/x]$, le point (vii) (e), appliqué à $\chi$ avec l'instance $\neg A \to (B \vee \neg A)$, donne $\forall y \leqslant v\ (y = S\,v \vee \neg\varphi[y/x])$, et $S\,v = S\,v \vee \neg\varphi[S\,v/x]$ est démontrable ; le point (vii) (d) donne $\forall y \leqslant S\,v\ (y = S\,v \vee \neg\varphi[y/x])$, ce qui, avec $\varphi[S\,v/x]$ et $w = S\,v$, contredit $\neg C$. Le théorème de la déduction et la règle des tautologies donnent $\neg\varphi[S\,v/x]$.

Le point (iii) de Récurrence dans PA donne $\{\neg C\} \vdash_{\mathsf{PA}} \forall v\, \chi$. Le terme $x$ est substituable à $v$ dans $\chi$, dont les occurrences libres de $v$ ne sont que sous $\forall y$ et $\exists u$ : l'axiome (2) donne $\forall y \leqslant x\ \neg\varphi[y/x]$, et le point (vii) (a) de Ordre dans PA, avec le terme $x$ et $x \leqslant x$, donne $\neg\varphi[y/x][x/y]$, c'est-à-dire $\neg\varphi$. La généralisation en $x$, qui n'est pas libre dans $\neg C$, donne $\{\neg C\} \vdash_{\mathsf{PA}} \forall x\, \neg\varphi$, puis $\neg\exists x\, \varphi$ par l'instance $P \to \neg\neg P$, et la contraposition conclut.

(ii) Appliquons (i) à $\neg\varphi$, avec $(\neg\varphi)[y/x] = \neg\varphi[y/x]$. Sous les hypothèses de $\Gamma$, $\neg\varphi$ et $\forall y \leqslant x\ (y = x \vee \neg\neg\varphi[y/x])$, le point (vii) (e) de Ordre dans PA, avec l'instance $(B \vee \neg\neg A) \to (B \vee A)$, donne $\forall y \leqslant x\ (y = x \vee \varphi[y/x])$, donc $\varphi$ par hypothèse, ce qui contredit $\neg\varphi$. Ainsi $\Gamma \vdash_{\mathsf{PA}} \neg(\neg\varphi \wedge \forall y \leqslant x\ (y = x \vee \neg\neg\varphi[y/x]))$ ; la généralisation en $x$ et la règle des tautologies donnent la négation du second membre de (i), puis $\Gamma \vdash_{\mathsf{PA}} \neg\exists x\, \neg\varphi$, c'est-à-dire $\neg\neg\forall x\, \neg\neg\varphi$. L'instance $\neg\neg P \to P$, la monotonie du point (ii) de Récurrence dans PA avec $\neg\neg\varphi \to \varphi$, et l'axiome (2) donnent $\Gamma \vdash_{\mathsf{PA}} \varphi$.

(iii) Existence. Soit $a$ et $m$ deux variables distinctes, différentes de $q$, de $r$ et de la variable liée de $r < m$. On montre $\{\neg(m = 0)\} \vdash_{\mathsf{PA}} \exists q\, \exists r\, (q \times m + r = a \wedge r < m)$ par récurrence sur $a$, qui n'est pas libre dans $\neg(m = 0)$ ; le théorème de la déduction donne l'implication, et le point (iv) de Récurrence dans PA donne ensuite le cas des termes $t$ et $m$. Sous l'hypothèse $\neg(m = 0)$, l'instance de $\mathrm Q_3$ et l'élimination avec une variable nouvelle $k$ permettent de supposer $m = S\,k$ ; alors $0 \leqslant k$ et le point (v) de Ordre dans PA donnent $0 < S\,k$, d'où $0 < m$ par le remplacement, et l'élimination de $k$, qui n'est pas libre dans $0 < m$, donne $0 < m$ sous la seule hypothèse $\neg(m = 0)$.

Pour $0$ : la chaîne $0 \times m + 0 = 0 \times m = 0$ et $0 < m$ donnent la conclusion, par deux introductions de l'existentiel avec le terme $0$. Pas : sous l'hypothèse de récurrence, l'élimination avec des variables nouvelles $c$ et $d$ permet de supposer $c \times m + d = a$ et $d < m$. Par le point (v) de Ordre dans PA, $S\,d \leqslant m$ donne $S\,d < m$ ou $S\,d = m$. Dans le premier cas, la chaîne $c \times m + S\,d = S(c \times m + d) = S\,a$ donne la conclusion pour $S\,a$, avec les termes $c$ et $S\,d$. Dans le second, la chaîne $S\,c \times m + 0 = c \times m + m = c \times m + S\,d = S(c \times m + d) = S\,a$, avec $0 < m$, la donne avec les termes $S\,c$ et $0$.

Unicité. Soit $\Gamma$ formé des trois hypothèses. Par le point (v) de Ordre dans PA, on a $q < q'$, $q = q'$ ou $q' < q$. Sous l'hypothèse $q < q'$, l'élimination avec un témoin $a$ donne $a + S\,q = q'$, et la chaîne $$\begin{aligned} &q \times m + r \\ &\quad = q' \times m + r' \\ &\quad = (a + S\,q) \times m + r' \\ &\quad = q \times m + (a \times m + m + r'), \end{aligned}$$ obtenue par la distributivité, le point (iii) de Lois de + et ×, l'associativité et la commutativité, donne $r = a \times m + r' + m$ par la simplification, puis $m \leqslant r$, avec le témoin $a \times m + r'$, ce qui contredit $r < m$ (Ordre dans PA, (v)). Le cas $q' < q$ est symétrique. Il reste $q = q'$ ; la chaîne $r + q \times m = q \times m + r = q' \times m + r' = r' + q \times m$ et la simplification donnent $r = r'$.