Calculs dans l'arithmétique de Robinson

Par le point (ii) de Calcul à variables libres, appliqué après une instanciation de chaque variable par elle-même (Règles dérivées, (iii)), les axiomes sans quantificateur intérieur montrent que, pour tous termes $t$ et $u$, $\mathsf Q$ démontre les formules $$\begin{aligned} &\neg(S\,t = 0), \quad S\,t = S\,u \to t = u, \\ &t + 0 = t, \quad t + S\,u = S(t + u), \\ &t \times 0 = 0, \quad t \times S\,u = t \times u + t. \end{aligned}$$ On les appelle des instances de $\mathrm Q_1$, $\mathrm Q_2$, $\mathrm Q_4$ à $\mathrm Q_7$. Les règles d'égalité (réflexivité, symétrie, transitivité, congruence) sont celles du point (vi) du même nœud, le remplacement d'un terme celui du point (v). Dire que, « sous les hypothèses $H_1, \dots, H_p$ », on a $C$, c'est dire que $\mathsf Q \cup \{H_1, \dots, H_p\} \vdash C$ ; le point (i) du même nœud donne alors $\mathsf Q \vdash H_1 \to (\cdots \to (H_p \to C) \cdots)$, et toute formule démontrable dans $\mathsf Q$ peut servir sous ces hypothèses.

(i) Par récurrence sur $n$. L'instance $\underline m + 0 = \underline m$ de $\mathrm Q_4$ est le cas $n = 0$. Si $\mathsf Q \vdash \underline m + \underline n = \underline{m + n}$, l'instance $\underline m + S\,\underline n = S(\underline m + \underline n)$ de $\mathrm Q_5$, la congruence $S(\underline m + \underline n) = S\,\underline{m + n}$ et la transitivité donnent $\mathsf Q \vdash \underline m + \underline{n + 1} = \underline{m + n + 1}$, puisque $S\,\underline{m + n}$ est le terme $\underline{m + n + 1}$.

Pour le produit, $\mathrm Q_6$ donne le cas $n = 0$. Si $\mathsf Q \vdash \underline m \times \underline n = \underline{mn}$, l'instance $\underline m \times S\,\underline n = \underline m \times \underline n + \underline m$ de $\mathrm Q_7$, la congruence $\underline m \times \underline n + \underline m = \underline{mn} + \underline m$, le cas de la somme $\underline{mn} + \underline m = \underline{mn + m}$ et la transitivité donnent $\mathsf Q \vdash \underline m \times \underline{n + 1} = \underline{m(n + 1)}$.

Pour un terme clos quelconque, on raisonne par récurrence sur $t$, grâce à la lecture unique. Si $t = 0$, la réflexivité conclut. Si $t = S\,t_1$ et $\mathsf Q \vdash t_1 = \underline{k_1}$, la congruence donne $\mathsf Q \vdash S\,t_1 = \underline{k_1 + 1}$. Si $t = t_1 + t_2$, avec $\mathsf Q \vdash t_i = \underline{k_i}$, deux congruences donnent $\mathsf Q \vdash t_1 + t_2 = \underline{k_1} + \underline{k_2}$, et le cas de la somme conclut ; de même pour $\times$.

(ii) Si $m > n$, il suffit de montrer $\mathsf Q \vdash \neg(\underline n = \underline m)$, puis d'appliquer la symétrie et l'instance $(P \to Q) \to (\neg Q \to \neg P)$. On suppose donc $m < n$, et l'on raisonne par récurrence sur $m$. Si $m = 0$, alors $n = j + 1$ ; l'instance $\neg(S\,\underline j = 0)$ de $\mathrm Q_1$ et la symétrie $0 = S\,\underline j \to S\,\underline j = 0$ donnent $\mathsf Q \vdash \neg(0 = S\,\underline j)$ par contraposition. Si $m = i + 1$, alors $n = j + 1$ avec $i < j$, l'hypothèse de récurrence donne $\mathsf Q \vdash \neg(\underline i = \underline j)$, et l'instance $S\,\underline i = S\,\underline j \to \underline i = \underline j$ de $\mathrm Q_2$ donne $\mathsf Q \vdash \neg(S\,\underline i = S\,\underline j)$ par contraposition.

(iii) Choisissons une variable $w'$ distincte de $x_0$, $x_1$, $x$ et $w$. L'instanciation de $x_0$ par lui-même et le renommage du point (iii) de Calcul à variables libres donnent $\mathsf Q \vdash \neg(x_0 = 0) \to \exists w'\, (x_0 = S\,w')$. La variable $x$ est substituable à $x_0$ dans cette formule, puisque $x \neq w'$, d'où $\mathsf Q \vdash \neg(x = 0) \to \exists w'\, (x = S\,w')$ ; un dernier renommage, permis puisque $w$ ne figure pas dans $x = S\,w'$, donne la première assertion.

La seconde se démontre par récurrence sur $k$. Pour $k = 0$, les instances $S\,w + 0 = S\,w$ de $\mathrm Q_4$, $w + S\,0 = S(w + 0)$ de $\mathrm Q_5$ et $w + 0 = w$ de $\mathrm Q_4$, la congruence $S(w + 0) = S\,w$, la symétrie et la transitivité donnent $\mathsf Q \vdash S\,w + 0 = w + S\,0$. Si $\mathsf Q \vdash S\,w + \underline k = w + S\,\underline k$, les instances $S\,w + S\,\underline k = S(S\,w + \underline k)$ et $w + S\,S\,\underline k = S(w + S\,\underline k)$ de $\mathrm Q_5$ et la congruence $S(S\,w + \underline k) = S(w + S\,\underline k)$ donnent $\mathsf Q \vdash S\,w + \underline{k + 1} = w + S\,\underline{k + 1}$.

(iv) Par (i), $\mathsf Q \vdash \underline{n - k} + \underline k = \underline n$, et le point (iii) de Calcul à variables libres, avec le terme clos $\underline{n - k}$, donne $\mathsf Q \vdash \exists z\, (z + \underline k = \underline n)$.

(v) La formule $x \leqslant \underline n$ est $\exists z\, (z + x = \underline n)$, avec $z \neq x$. Comme $z$ n'est pas libre dans $D_n(x)$, il suffit, par l'élimination du point (iii) de Calcul à variables libres, de montrer $\mathsf Q \vdash z + x = \underline n \to D_n(x)$, ce que l'on fait par récurrence sur $n$, pour tous les couples de variables distinctes $(x, z)$.

Soit $w$ une variable distincte de $x$ et de $z$. On a $\vdash x = 0 \to D_n(x)$, puisque $x = \underline 0$ est le premier terme de la disjonction. Montrons que $$\mathsf Q \cup \{x = S\,w,\ z + x = \underline n\} \vdash D_n(x).$$ Le point (v) de Calcul à variables libres, avec la formule $z + v = \underline n$, donne $z + S\,w = \underline n$ ; l'instance $z + S\,w = S(z + w)$ de $\mathrm Q_5$, la symétrie et la transitivité donnent $S(z + w) = \underline n$.

Si $n = 0$, l'instance $\neg(S(z + w) = 0)$ de $\mathrm Q_1$ contredit cette formule, et l'instance $P \to (\neg P \to Q)$ donne $D_0(x)$. Si $n = j + 1$, alors $\underline n = S\,\underline j$, et l'instance $S(z + w) = S\,\underline j \to z + w = \underline j$ de $\mathrm Q_2$ donne $z + w = \underline j$, puis $D_j(w)$ par l'hypothèse de récurrence, appliquée au couple $(w, z)$. Pour chaque $i \leqslant j$, la congruence $w = \underline i \to S\,w = S\,\underline i$ et la transitivité donnent $\vdash x = S\,w \to (w = \underline i \to x = \underline{i + 1})$, et $x = \underline{i + 1}$ est un terme de $D_n(x)$ ; le raisonnement par cas sur $D_j(w)$ donne $D_n(x)$.

Le théorème de la déduction, sous la forme (i) de Calcul à variables libres, donne $\mathsf Q \vdash x = S\,w \to (z + x = \underline n \to D_n(x))$. La variable $w$ n'est libre ni dans $z + x = \underline n$ ni dans $D_n(x)$, et l'élimination donne $\mathsf Q \vdash \exists w\, (x = S\,w) \to (z + x = \underline n \to D_n(x))$. Avec $\vdash x = 0 \to D_n(x)$ et la première assertion de (iii), la règle des tautologies donne $\mathsf Q \vdash z + x = \underline n \to D_n(x)$.

(vi) Par récurrence sur $n$, pour tous les choix des variables liées des deux formules. Pour $n = 0$, l'instance $x + 0 = x$ de $\mathrm Q_4$ et l'introduction de l'existentiel, avec le terme $x$, donnent $\mathsf Q \vdash \exists z'\, (z' + 0 = x)$, c'est-à-dire $\mathsf Q \vdash \underline 0 \leqslant x$, et la disjonction s'en déduit.

Soit $n = j + 1$. Si $\mathsf Q \vdash x = \underline i \to x \leqslant \underline n$ pour tout $i \leqslant n$, alors, par (v) et le raisonnement par cas, $\mathsf Q \vdash x \leqslant \underline j \to x \leqslant \underline n$. Or, pour $i \leqslant n$, on a $\mathsf Q \vdash \underline i \leqslant \underline n$ par (iv), et le point (v) de Calcul à variables libres, appliqué à $\exists z\, (z + v = \underline n)$ avec les termes $\underline i$ et $x$, et la symétrie donnent $\mathsf Q \vdash x = \underline i \to x \leqslant \underline n$.

Il reste, par l'hypothèse de récurrence, à montrer $\mathsf Q \vdash \exists w\, (w + \underline j = x) \to (x \leqslant \underline n \vee \underline n \leqslant x)$, pour une variable $w$ distincte de $x$ et des variables liées de la conclusion, que l'on note $C$. Comme $w$ n'est pas libre dans $C$, l'élimination du point (iii) de Calcul à variables libres, appliquée dans $\mathsf Q$, ramène à $\mathsf Q \vdash w + \underline j = x \to C$, c'est-à-dire, par le théorème de la déduction, à montrer $C$ sous l'hypothèse $w + \underline j = x$. Soit $u$ une variable distincte de $w$, de $x$ et de ces variables liées. Par (iii), $w = 0$ ou $\exists u\, (w = S\,u)$. Sous l'hypothèse $w = 0$, le remplacement donne $0 + \underline j = x$, et (i) donne $0 + \underline j = \underline j$, d'où $x = \underline j$ et $x \leqslant \underline n$ comme ci-dessus. Sous l'hypothèse $w = S\,u$, le remplacement donne $S\,u + \underline j = x$, et (iii) donne $u + S\,\underline j = x$, d'où $\exists z'\, (z' + \underline n = x)$, c'est-à-dire $\underline n \leqslant x$, par introduction de l'existentiel avec le terme $u$. Le théorème de la déduction donne alors $\mathsf Q \vdash w + \underline j = x \to (w = S\,u \to C)$. On ne peut pas éliminer $u$ sous l'hypothèse $w + \underline j = x$, qui a des variables libres ; on applique l'élimination dans $\mathsf Q$, sous la forme avec hypothèse $\chi = (w + \underline j = x)$ du point (iii) de Calcul à variables libres, puisque $u$ n'est libre ni dans $\chi$ ni dans $C$ : $\mathsf Q \vdash w + \underline j = x \to (\exists u\, (w = S\,u) \to C)$. Le cas $w = 0$ donne de même $\mathsf Q \vdash w + \underline j = x \to (w = 0 \to C)$, et le raisonnement par cas, avec la première assertion de (iii), donne $\mathsf Q \vdash w + \underline j = x \to C$.