Divisibilité, congruences, Bézout et lemme chinois dans l'arithmétique de Peano

Les chaînes d'égalités emploient les lois de Lois de + et × sans les nommer.

(i) Les témoins de $t \mid 0$ et $t \mid t$ sont $0$ et $S\,0$. Sous les hypothèses $a \times t = u$ et $b \times u = r$, la chaîne $(b \times a) \times t = b \times (a \times t) = r$ donne $t \mid r$ ; sous l'hypothèse $a \times t = u$, la chaîne $(r \times a) \times t = r \times u = u \times r$ donne $t \mid u \times r$. Sous les hypothèses $a \times r = t + u$ et $b \times r = t$, le point (iv) de Ordre dans PA donne $b \leqslant a$ ou $a \leqslant b$. Sous l'hypothèse $c + b = a$, la chaîne $c \times r + t = c \times r + b \times r = a \times r = t + u = u + t$ et la simplification donnent $c \times r = u$. Sous l'hypothèse $c + a = b$, la chaîne $t + 0 = t = c \times r + a \times r = t + (c \times r + u)$, réordonnée, et la simplification donnent $c \times r + u = 0$, donc $u = 0$, et $r \mid u$ par le premier point. Sous l'hypothèse $a \times 0 = t$, $\mathrm Q_6$ donne $t = 0$.

Sous l'hypothèse $a \times t = S\,0$, on raisonne par cas sur $t$ et sur $a$. Si $t = 0$, alors $S\,0 = a \times 0 = 0$, ce que $\mathrm Q_1$ exclut. Si $a = 0$, de même $S\,0 = 0 \times t = 0$. Si $t = S\,k$ et $a = S\,b$, la chaîne $S(S\,b \times k + b) = S\,b \times k + S\,b = S\,b \times S\,k = S\,0$ et $\mathrm Q_2$ donnent $S\,b \times k + b = 0$, donc $b = 0$ et $S\,b \times k = 0$ ; alors $k = S\,0 \times k = 0$, et $t = S\,0$.

(ii) La réflexivité a les témoins $0$ et $0$ ; la symétrie échange les témoins. Sous les hypothèses $t + a \times m = u + b \times m$ et $u + c \times m = r + e \times m$, la chaîne $$\begin{aligned} &t + (a + c) \times m \\ &\quad = t + a \times m + c \times m \\ &\quad = u + b \times m + c \times m \\ &\quad = u + c \times m + b \times m \\ &\quad = r + e \times m + b \times m \\ &\quad = r + (e + b) \times m \end{aligned}$$ donne la transitivité. Sous l'hypothèse $t + a \times m = u + b \times m$, les chaînes $t + r + a \times m = u + r + b \times m$ et $t \times r + (a \times r) \times m = (t + a \times m) \times r = u \times r + (b \times r) \times m$ donnent les deux compatibilités. Les témoins de $t + r \times m \equiv t$ sont $0$ et $r$.

Si $a \times m = t$, les témoins $0$ et $a$ donnent $t + 0 \times m = 0 + a \times m$. Réciproquement, sous l'hypothèse $t + a \times m = 0 + b \times m$, on a $b \leqslant a$ ou $a \leqslant b$. Si $c + a = b$, la chaîne $t + a \times m = c \times m + a \times m$ et la simplification donnent $c \times m = t$. Si $c + b = a$, la chaîne $t + c \times m + b \times m = b \times m = 0 + b \times m$ et la simplification donnent $t + c \times m = 0$, donc $t = 0$, et $m \mid t$. Pour le module $S\,0$, les témoins $u$ et $t$ donnent $t + u \times S\,0 = t + u = u + t \times S\,0$. Enfin, sous les hypothèses $k \times m = P$ et $t + a \times P = u + b \times P$, la chaîne $t + (a \times k) \times m = t + a \times P = u + b \times P = u + (b \times k) \times m$ conclut.

(iii) Soit $x$ et $m$ deux variables distinctes, différentes des variables liées de l'énoncé ; le point (iv) de Récurrence dans PA donnera le cas des termes $t$ et $m$. On raisonne sous les hypothèses $\neg(m = 0)$ et $x \perp m$ ; la conclusion $\exists e\, (e \times x \equiv S\,0 \pmod m)$ est notée $E$.

Si $x = 0$. L'axiome (2), avec le terme $m$, donne $(m \mid x \wedge m \mid m) \to m = S\,0$, et (i) donne $m \mid 0$ et $m \mid m$ ; donc $m = S\,0$, et (ii), avec le remplacement, donne $0 \times x \equiv S\,0 \pmod m$, puis $E$.

Si $\neg(x = 0)$. Soit $\varphi(d)$ la formule $\neg(d = 0) \wedge \exists e\, \exists f\, (e \times x = f \times m + d)$, où $d$, $e$, $f$ sont des variables distinctes, différentes de $x$ et de $m$. On a $\varphi(x)$ : la chaîne $S\,0 \times x = x = 0 \times m + x$ fournit les témoins $S\,0$ et $0$. Le point (i) de Plus petit élément, division donne alors un $d$ tel que $\varphi(d)$ et $\forall y \leqslant d\ (y = d \vee \neg\varphi(y))$, et l'on élimine $e$ et $f$ de $\varphi(d)$ : $e \times x = f \times m + d$. Par le point (vii) (a) de Ordre dans PA et la première équivalence de (v), pour tout terme $s$ convenable, $s < d$ entraîne $\neg\varphi(s)$ : c'est la minimalité de $d$.

Symétrisation. Montrons que, sous les hypothèses $\neg(x = 0)$, $\neg(m = 0)$ et $V \times m = U \times x + s$, pour des termes $U$, $V$, $s$, il existe $U'$ et $V'$ tels que $U' \times x = V' \times m + s$. Soit $K = U + V$. Par le point (i) et le point (vi) de Ordre dans PA, et la transitivité, $U \leqslant K \times m$ et $V \leqslant K \times x$ ; l'élimination fournit $U'$ et $V'$ tels que $U' + U = K \times m$ et $V' + V = K \times x$. La chaîne $$\begin{aligned} &U' \times x + U \times x \\ &\quad = (K \times m) \times x \\ &\quad = (K \times x) \times m \\ &\quad = V' \times m + V \times m \\ &\quad = V' \times m + s + U \times x \end{aligned}$$ et la simplification donnent $U' \times x = V' \times m + s$. Il en résulte que, si $\neg(s = 0)$, alors $\varphi(s)$.

$d$ divise $m$. Le point (iii) de Plus petit élément, division, avec $\neg(d = 0)$, fournit $g$ et $s$ tels que $g \times d + s = m$ et $s < d$. La chaîne $$\begin{aligned} &(g \times f + S\,0) \times m \\ &\quad = (g \times f) \times m + S\,0 \times m \\ &\quad = g \times (f \times m) + m \\ &\quad = g \times (f \times m) + (g \times d + s) \\ &\quad = g \times (f \times m + d) + s \\ &\quad = g \times (e \times x) + s \\ &\quad = (g \times e) \times x + s \end{aligned}$$ est de la forme $V \times m = U \times x + s$ ; si $\neg(s = 0)$, la symétrisation donne $\varphi(s)$, contraire à la minimalité. Donc $s = 0$ et $g \times d = m$ : $d \mid m$.

$d$ divise $x$. De même, soit $g \times d + s = x$ avec $s < d$, et $h = g \times e$. La chaîne $$\begin{aligned} &h \times x + s \\ &\quad = g \times (e \times x) + s \\ &\quad = g \times (f \times m + d) + s \\ &\quad = (g \times f) \times m + (g \times d + s) \\ &\quad = (g \times f) \times m + x \end{aligned}$$ donne $h \times x + s = (g \times f) \times m + x$. Si $h = 0$, la chaîne $s = h \times x + s = (g \times f) \times m + x$ donne $x \leqslant s$ ; or $\varphi(x)$ et la minimalité excluent $x < d$, donc $d \leqslant x$ par le point (v) de Ordre dans PA, puis $d \leqslant s$, ce qui contredit $s < d$. Si $h = S\,k$, la chaîne $k \times x + s + x = h \times x + s = (g \times f) \times m + x$ et la simplification donnent $(g \times f) \times m = k \times x + s$ ; la symétrisation et la minimalité donnent $s = 0$ comme ci-dessus, et $d \mid x$.

Conclusion. L'axiome (2), avec le terme $d$, et $x \perp m$ donnent $d = S\,0$. Alors $e \times x = f \times m + S\,0$, et la chaîne $e \times x + 0 \times m = S\,0 + f \times m$ donne $e \times x \equiv S\,0 \pmod m$, puis $E$. On élimine les variables introduites, qui ne sont libres ni dans les hypothèses ni dans $E$, et le raisonnement par cas sur $x = 0$ conclut.

(iv) Sous les hypothèses de la première formule, (iii) fournit $e$ tel que $e \times t \equiv S\,0 \pmod m$, et (ii) donne $(e \times t) \times u \equiv S\,0 \times u \pmod m$, c'est-à-dire $u \equiv (e \times t) \times u \pmod m$ par la symétrie et $S\,0 \times u = u$. Par (ii), $m \mid t \times u$ donne $t \times u \equiv 0 \pmod m$, puis $(t \times u) \times e \equiv 0 \times e \pmod m$, et $(e \times t) \times u = (t \times u) \times e$, $0 \times e = 0$. La transitivité donne $u \equiv 0 \pmod m$, et (ii) donne $m \mid u$.

Pour la seconde, raisonnons sous ses hypothèses et sous $d \mid t \times u$ et $d \mid m$, avec une variable $d$ nouvelle. On a $\neg(d = 0)$, puisque $0 \mid m$ donnerait $m = 0$ par (i). Sous les hypothèses supplémentaires $k \mid t$ et $k \mid d$, la transitivité de (i) donne $k \mid m$, et $t \perp m$ donne $k = S\,0$ ; le théorème de la déduction décharge $k \mid t$ et $k \mid d$, puis la généralisation en $k$, qui n'est libre dans aucune des hypothèses restantes, donne $t \perp d$, écrite avec la variable liée $k$. La première formule, appliquée aux termes $d$, $t$, $u$, donne $d \mid u$, et $u \perp m$ donne $d = S\,0$. Le théorème de la déduction et la généralisation en $d$ donnent $t \times u \perp m$.

(v) Sous les hypothèses, l'instance de $\mathrm Q_3$ permet de supposer $m = S\,k$. Comme $n \perp m$, le point (iii) fournit $e$ tel que $e \times n \equiv S\,0 \pmod m$. Posons $s = t + k \times u$ et $c_0 = u + (e \times s) \times n$. Les témoins $0$ et $e \times s$ donnent $c_0 \equiv u \pmod n$. Par (ii), $(e \times n) \times s \equiv S\,0 \times s \pmod m$, et $(e \times s) \times n = (e \times n) \times s$, $S\,0 \times s = s$ ; la compatibilité avec l'addition de $u$ et la commutativité donnent $c_0 \equiv u + s \pmod m$. Or la chaîne $u + s = t + (k \times u + u) = t + u \times S\,k = t + u \times m$ et (ii) donnent $u + s \equiv t \pmod m$, et la transitivité donne $c_0 \equiv t \pmod m$. L'introduction de l'existentiel, avec le terme $c_0$, conclut.