Bornes strictes, multiples communs et modules de Gödel dans l'arithmétique de Peano

(i) (a) Raisonnons sous les hypothèses de $\Gamma$ et sous $x \leqslant t$. Sous l'hypothèse supplémentaire $x = t$, la disjonction $x = t \vee \varphi$ est immédiate. Sous l'hypothèse $\neg(x = t)$, la première équivalence du point (v) de Ordre dans PA donne $x < t$, puis $\varphi$ par hypothèse, et encore $x = t \vee \varphi$. Le raisonnement par cas, sur la tautologie $x = t \vee \neg(x = t)$, donne $\Gamma \cup \{x \leqslant t\} \vdash_{\mathsf{PA}} x = t \vee \varphi$, et le point (vii) (b) du même nœud donne $\Gamma \vdash_{\mathsf{PA}} \forall x < t\ \varphi$, puisque $x$ n'est libre dans aucune formule de $\Gamma$. Pour la borne $0$, l'hypothèse $x < 0$ contredit $\neg(x < 0)$, point (v) du même nœud, et l'instance $P \to (\neg P \to Q)$ donne $\varphi$.

(b) Le terme $u$ est substituable à $x$ dans $x = t \vee \varphi$, et $(x = t \vee \varphi)[u/x]$ est $u = t \vee \varphi[u/x]$, puisque $x$ ne figure pas dans $t$. Le point (vii) (a) de Ordre dans PA donne donc $\vdash \forall x < t\ \varphi \to \big(u \leqslant t \to (u = t \vee \varphi[u/x])\big)$, et la première équivalence du point (v) donne $\vdash_{\mathsf{PA}} u < t \to (u \leqslant t \wedge \neg(u = t))$. L'instance $(A \to (B \to (C \vee D))) \to ((E \to (B \wedge \neg C)) \to (A \to (E \to D)))$ conclut.

(c) Sous l'hypothèse $\forall x < S\,t\ \varphi$ et sous $x < t$, le point (v) de Ordre dans PA donne $x \leqslant t$, puis $x < S\,t$, et (b), avec le terme $x$, donne $\varphi$ ; comme $x$ n'est pas libre dans l'hypothèse, (a) donne $\forall x < t\ \varphi$. De $t \leqslant t$, le même point tire $t < S\,t$, et (b), avec le terme $t$, donne $\varphi[t/x]$. Réciproquement, sous les hypothèses $\forall x < t\ \varphi$, $\varphi[t/x]$ et $x < S\,t$, on a $x \leqslant t$. Si $x = t$, le remplacement d'un terme (Calcul à variables libres, (v)), appliqué à $\varphi$ avec les termes $t$ et $x$, et la symétrie de l'égalité donnent $\varphi$ ; sinon, $x < t$ et (b) donnent $\varphi$. La variable $x$ n'est libre ni dans $\forall x < t\ \varphi$ ni dans $\varphi[t/x]$, puisqu'elle ne figure pas dans $t$, et (a) conclut.

(ii) Récurrence sur $M$, par le point (iii) de Récurrence dans PA, avec $\Gamma$ vide ; on note $\psi$ la formule $\exists b\, (\neg(b = 0) \wedge K(b, M))$.

Cas $0$. Par le point (vii) (d) de Ordre dans PA, $K(S\,0, 0)$ équivaut à $0 = 0 \vee 0 \mid S\,0$, qui découle de la réflexivité de l'égalité. Avec l'instance $\neg(S\,0 = 0)$ de $\mathrm Q_1$, l'introduction de l'existentiel, avec le terme $S\,0$, donne $\psi[0/M]$.

Pas. Sous l'hypothèse $\psi$, l'élimination avec une variable nouvelle $c$ permet de supposer $\neg(c = 0)$ et $K(c, M)$. Par l'intégrité (Lois de + et ×, (iv)), $c \times S\,M = 0$ donnerait $c = 0$ ou $S\,M = 0$, que l'hypothèse et $\mathrm Q_1$ excluent : donc $\neg(c \times S\,M = 0)$. Par le point (i) de Bézout, lemme chinois, $k \mid c \to k \mid c \times S\,M$, d'où $(k = 0 \vee k \mid c) \to (k = 0 \vee k \mid c \times S\,M)$, et le point (vii) (e) de Ordre dans PA donne $K(c \times S\,M, M)$. Enfin $S\,M \mid c \times S\,M$, avec le témoin $c$. Le point (vii) (d) réunit ces deux formules en $K(c \times S\,M, S\,M)$, et l'introduction de l'existentiel, avec le terme $c \times S\,M$, donne $\psi[S\,M/M]$. On élimine $c$, qui n'est libre ni dans $\psi$ ni dans la conclusion, et le théorème de la déduction décharge l'hypothèse de récurrence.

(iii) Écrivons $m_i$ et $m_j$ pour $m(b, i)$ et $m(b, j)$, et raisonnons sous les trois hypothèses, puis sous $d \mid m_i$ et $d \mid m_j$, pour une variable $d$ nouvelle.

Une différence. L'élimination de $i < j$, c'est-à-dire de $S\,i \leqslant j$, avec un témoin $a$ donne $a + S\,i = j$. Les chaînes $$\begin{aligned} S\,j \times b &= S(a + S\,i) \times b \\ &= (S\,a + S\,i) \times b \\ &= S\,a \times b + S\,i \times b, \\ m_j &= S(S\,a \times b + S\,i \times b) \\ &= S\,a \times b + S(S\,i \times b) \\ &= m_i + S\,a \times b \end{aligned}$$ emploient la congruence, le point (i) de Lois de + et ×, la distributivité, $\mathrm Q_5$ et la commutativité. Par le point (i) de Bézout, lemme chinois, $d \mid m_i + S\,a \times b$ et $d \mid m_i$ donnent $d \mid S\,a \times b$.

L'entier $d$ est étranger à $b$. Sous les hypothèses $e \mid d$ et $e \mid b$, pour une variable $e$ nouvelle, la transitivité de la divisibilité donne $e \mid m_i$, et $e \mid b$ donne $e \mid b \times S\,i$, c'est-à-dire $e \mid S\,i \times b$ par la commutativité et le remplacement. Comme $m_i = S\,i \times b + S\,0$, le point (i) de Bézout, lemme chinois donne $e \mid S\,0$, puis $e = S\,0$. Le théorème de la déduction décharge $e \mid d$ et $e \mid b$, et la généralisation en $e$, qui n'est libre dans aucune des hypothèses restantes, donne $d \perp b$, donc $b \perp d$ par la symétrie établie au nœud Bézout, lemme chinois. De plus $\neg(d = 0)$ : sinon $0 \mid m_i$ donnerait $m_i = 0$, contraire à $\mathrm Q_1$.

L'entier $d$ divise $S\,a$, puis $b$. La commutativité donne $d \mid b \times S\,a$, et le lemme d'Euclide (Bézout, lemme chinois, (iv)), appliqué aux termes $b$, $S\,a$ et au module $d$, donne $d \mid S\,a$. La chaîne $i + S\,a = S(i + a) = S(a + i) = a + S\,i = j$ donne $S\,a \leqslant j$, avec le témoin $i$, puis $S\,a \leqslant n$ par la transitivité. Le point (vii) (a) de Ordre dans PA, appliqué à $K(b, n)$ avec le terme $S\,a$, donne $S\,a = 0 \vee S\,a \mid b$, et $\mathrm Q_1$ exclut le premier cas. La transitivité donne $d \mid b$, puis $d \mid S\,i \times b$ comme ci-dessus.

Conclusion. De $d \mid S\,i \times b + S\,0$ et $d \mid S\,i \times b$, le point (i) de Bézout, lemme chinois tire $d \mid S\,0$, puis $d = S\,0$. On élimine $a$, qui n'est libre ni dans les hypothèses ni dans $d = S\,0$ ; le théorème de la déduction décharge $d \mid m_i$ et $d \mid m_j$, et la généralisation en $d$, qui n'est libre dans aucune des trois hypothèses, donne $m_i \perp m_j$.