Lemme chinois borné et prolongement d'une suite codée par β dans l'arithmétique de Peano

(i) Notons $\Gamma$ l'ensemble des deux hypothèses, $K(b, n)$ et $\forall i \leqslant n\ \exists u\ \theta$, écrivons $m_t$ pour $m(b, t)$, et soit $j$, $l$ et $P$ des variables nouvelles. Notons $A(j)$ la formule $\forall i < j\ \big(m_i \mid P \wedge \exists u\, (\theta \wedge c \equiv u \pmod{m_i})\big)$, $C(j)$ la formule $\forall l \leqslant n\ (l < j \vee P \perp m_l)$, et $L(j)$ la formule $$\begin{aligned} j \leqslant S\,n \to {}&\exists c\, \exists P\, \big(\neg(P = 0) \\ &\wedge A(j) \wedge C(j)\big). \end{aligned}$$ Dans $\mathcal N$, $L(j)$ dit qu'un multiple commun $P$ des $j$ premiers modules, étranger à tous les suivants, et un entier $c$ qui réalise les $j$ premières congruences existent. Montrons $\Gamma \vdash_{\mathsf{PA}} L(j)$ par récurrence sur $j$, qui n'est pas libre dans $\Gamma$.

Cas $0$. Prenons $c = 0$ et $P = S\,0$. On a $\neg(S\,0 = 0)$ par $\mathrm Q_1$, $A(0)$ par le point (i) (a) de Modules de Gödel, et $S\,0 \perp m_l$, puisque $d \mid S\,0$ donne $d = S\,0$ (Bézout, lemme chinois, (i)) ; le point (vii) (b) de Ordre dans PA donne $C(0)$, et deux introductions donnent $L(0)$.

Pas. Sous les hypothèses de $\Gamma$, $L(j)$ et $S\,j \leqslant S\,n$ : la formule $S\,j \leqslant S\,n$ est $j < S\,n$, qui équivaut à $j \leqslant n$ par le point (v) de Ordre dans PA, et le point (ii) donne $j \leqslant S\,n$. Le modus ponens dans $L(j)$, puis l'élimination, fournissent $c_0$ et $P_0$ tels que $\neg(P_0 = 0)$, $A(j)$ et $C(j)$, écrites avec $c_0$ et $P_0$. Le point (vii) (a) de Ordre dans PA, appliqué à $C(j)$ avec le terme $j$, donne $j < j \vee P_0 \perp m_j$, et $\neg(j < j)$, qui découle de la dernière formule du point (v) et de $j \leqslant j$, donne $P_0 \perp m_j$. Le même point, appliqué à la seconde hypothèse de $\Gamma$ avec le terme $j$, et l'élimination fournissent $e$ tel que $\theta[j/i][e/u]$. Le lemme chinois pour deux modules (Bézout, lemme chinois, (v)), appliqué aux modules $P_0$ et $m_j$ et aux termes $c_0$ et $e$, fournit $c_1$ tel que $c_1 \equiv c_0 \pmod{P_0}$ et $c_1 \equiv e \pmod{m_j}$. Posons $P_1 = P_0 \times m_j$ ; par l'intégrité, $\neg(P_1 = 0)$.

Montrons $A(S\,j)$ avec $c_1$ et $P_1$, par le point (i) (a) de Modules de Gödel, sous l'hypothèse $i < S\,j$, qui donne $i \leqslant j$ par le point (v) de Ordre dans PA. Si $i = j$ : $m_j \mid P_1$, avec le témoin $P_0$, donne $m_i \mid P_1$ par le remplacement, et $\theta[e/u] \wedge c_1 \equiv e \pmod{m_i}$ s'obtient de $\theta[j/i][e/u]$ et de $c_1 \equiv e \pmod{m_j}$ par le remplacement d'un terme et la symétrie, puisque $\theta[j/i][e/u] = \theta[e/u][j/i]$ ; l'introduction, avec le terme $e$, donne le second membre. Si $\neg(i = j)$ : alors $i < j$, et le point (i) (b) du même nœud, appliqué à $A(j)$, donne $m_i \mid P_0$, donc $m_i \mid P_1$, et $\exists u\, (\theta \wedge c_0 \equiv u \pmod{m_i})$. Par le point (ii) de Bézout, lemme chinois, $m_i \mid P_0$ et $c_1 \equiv c_0 \pmod{P_0}$ donnent $c_1 \equiv c_0 \pmod{m_i}$, puis, par la transitivité, $c_0 \equiv u \pmod{m_i} \to c_1 \equiv u \pmod{m_i}$ ; cette dernière hypothèse ne contient pas $u$, et la monotonie de Récurrence dans PA, (ii), donne $\exists u\, (\theta \wedge c_1 \equiv u \pmod{m_i})$.

Montrons $C(S\,j)$ avec $P_1$. Sous l'hypothèse $l \leqslant n$ : si $l \leqslant j$, alors $l < S\,j$. Sinon, l'ordre total donne $j \leqslant l$, et $\neg(j = l)$, puisque $j = l$ donnerait $l \leqslant j$ par la réflexivité et le remplacement ; donc $j < l$ ; alors $\neg(l < j)$, et $C(j)$ donne $P_0 \perp m_l$. Le point (iii) de Modules de Gödel, appliqué aux variables $j$ et $l$, donne $m_j \perp m_l$, et la seconde formule du lemme d'Euclide (Bézout, lemme chinois, (iv)), avec $\neg(m_l = 0)$, donne $P_0 \times m_j \perp m_l$. Dans les deux cas, $l < S\,j \vee P_1 \perp m_l$, et le point (vii) (b) de Ordre dans PA conclut.

Deux introductions, avec les termes $c_1$ et $P_1$, donnent $\exists c\, \exists P\, (\neg(P = 0) \wedge A(S\,j) \wedge C(S\,j))$. On élimine $c_1$, $e$, $c_0$ et $P_0$, qui ne figurent pas dans cette formule, et le théorème de la déduction, qui décharge $S\,j \leqslant S\,n$, donne $\Gamma \cup \{L(j)\} \vdash_{\mathsf{PA}} L(S\,j)$. Le point (iii) de Récurrence dans PA donne $\Gamma \vdash_{\mathsf{PA}} \forall j\, L(j)$.

Conclusion. Le terme $S\,n$ est substituable à $j$ dans $L(j)$, et $S\,n \leqslant S\,n$ ; l'axiome (2) et l'élimination fournissent $c$ et $P$ tels que $A(S\,n)$. Sous l'hypothèse $i \leqslant n$, on a $i < S\,n$, et le point (i) (b) de Modules de Gödel donne $\exists u\, (\theta \wedge c \equiv u \pmod{m_i})$ ; le point (vii) (b) de Ordre dans PA donne $\forall i \leqslant n\ \exists u\, (\theta \wedge c \equiv u \pmod{m_i})$, l'introduction de $\exists c$ conclut, et l'on élimine $P$.

(ii) Soit $M$ le terme $n + a + x$. Par le point (i) de Ordre dans PA et la transitivité, $n \leqslant M$, $a \leqslant M$ et $x \leqslant M$. Le point (ii) de Modules de Gödel, écrit avec une variable nouvelle à la place de $b$ et instancié par le terme $M$, et l'élimination fournissent $b_1$ tel que $\neg(b_1 = 0)$ et $K(b_1, M)$, et le point (vii) (e) de Ordre dans PA, avec $n \leqslant M$, donne $K(b_1, n)$.

Le multiple majore les valeurs. On raisonne par cas sur $M = 0 \vee \neg(M = 0)$. Si $M = 0$, alors $M \leqslant b_1$ par le point (i) du même nœud. Sinon, le point (vii) (a), appliqué à $K(b_1, M)$ avec le terme $M$, donne $M \mid b_1$, et l'élimination fournit $g$ tel que $g \times M = b_1$ ; on a $\neg(g = 0)$, puisque $g = 0$ donnerait $b_1 = 0 \times M = 0$, et le point (vi) donne $M \leqslant M \times g = b_1$. Pour tout terme $t$, le même point donne $b_1 \leqslant b_1 \times S\,t$, et la transitivité donne $M \leqslant S\,t \times b_1$.

Les valeurs à réaliser. Soit $\theta$ la formule $(i = n \wedge u = x) \vee (\neg(i = n) \wedge B(a, b, i, u))$. Sous l'hypothèse $i \leqslant n$ : si $i = n$, l'introduction avec le terme $x$ donne $\exists u\, \theta$ ; sinon, le point (ii) de Graphe de β dans PA donne $\exists u\, B(a, b, i, u)$, et la monotonie, sous l'hypothèse $\neg(i = n)$ où $u$ n'est pas libre, donne $\exists u\, \theta$. Le point (vii) (b) donne $\forall i \leqslant n\ \exists u\, \theta$, et le point (i), appliqué à la variable $b_1$, fournit $c_1$ tel que $\forall i \leqslant n\ \exists u\, \big(\theta \wedge c_1 \equiv u \pmod{m(b_1, i)}\big)$.

Ce sont les valeurs de β. Sous l'hypothèse $i \leqslant n$, le point (vii) (a) et l'élimination fournissent $e$ tel que $\theta[e/u]$ et $c_1 \equiv e \pmod{m(b_1, i)}$. Dans les deux cas de $\theta[e/u]$, on a $e \leqslant M$ : si $e = x$, par ce qui précède ; si $B(a, b, i, e)$, par le point (iii) de Graphe de β dans PA, qui donne $e \leqslant a$. Donc $e \leqslant S\,i \times b_1$, et le point (iv) du même nœud donne $B(c_1, b_1, i, e)$.

Pour $i < n$, sous l'hypothèse $B(a, b, i, u)$ : on a $i \leqslant n$ et $\neg(i = n)$, donc $B(a, b, i, e)$, et l'unicité du point (ii) du même nœud donne $u = e$, puis $B(c_1, b_1, i, u)$ par le remplacement. On élimine $e$, qui ne figure ni dans les hypothèses $i < n$ et $B(a, b, i, u)$ ni dans la conclusion ; le théorème de la déduction et la généralisation en $u$, qui n'est libre dans aucune hypothèse restante, donnent $\forall u\, (B(a, b, i, u) \to B(c_1, b_1, i, u))$, et le point (i) (a) de Modules de Gödel donne la première formule de la conclusion, avec $c_1$ et $b_1$. Pour $i = n$, le même raisonnement, mené avec le terme $n$ et $n \leqslant n$, fournit $e$ tel que $\theta[n/i][e/u]$ et $B(c_1, b_1, n, e)$ ; la formule $\theta[n/i][e/u]$ donne $e = x$, puisque $\neg(n = n)$ est exclu, et le remplacement donne $B(c_1, b_1, n, x)$, formule où $e$ ne figure pas.

Deux introductions, avec les termes $c_1$ et $b_1$, donnent la conclusion, et l'on élimine $c_1$ et $b_1$.