Proposition 3β et récurrence dans PA

Addition, soustraction tronquée, signe, sommes et produits bornés dans l'arithmétique de Peano

Les conventions sont celles de Fonctions p.r. dans PA. Chaque fonction de ce nœud est prise avec la construction indiquée ci-dessous, qui est celle qu'écrivent les preuves de Primitives récursives et de Clôture, et avec une définition naturelle du point (vi) de Fonctions p.r. dans PA, pour des variables dont aucune n'est quantifiée dans les définitions employées : il suffit de les mettre dans la partie $V$ . Les énoncés valent pour toutes ces définitions, puisque les preuves n'emploient que les points (ii) à (v) de ce nœud-là ; quand deux définitions d'une même construction, écrites avec des variables différentes, interviennent dans une même preuve, par exemple celle de $f$ et celle qui figure à l'intérieur de $\Sigma_f$ , le point (vii) du même nœud les identifie. On note $\mathrm{add}$ et $\mathrm{mul}$ l'addition et la multiplication, fonctions primitives récursives, pour les distinguer des symboles $+$ et $\times$ du langage, et $\mathbf 1$ la fonction $S \circ Z$ .

Les constructions sont les suivantes. L'addition s'obtient par récurrence primitive à partir de $P^1_1$ et de $S \circ P^3_3$ , la multiplication à partir de $Z$ et de $\mathrm{add} \circ (P^3_3, P^3_1)$ . Le prédécesseur $\mathrm{pr}$ s'obtient sans paramètre, à partir de $0$ et de $P^2_1$ , et la soustraction tronquée $x \mathbin{\dot{-}} y$ à partir de $P^1_1$ et de $\mathrm{pr} \circ P^3_3$ . Le signe est $\overline{\mathrm{sg}} = {\dot{-}} \circ (\mathbf 1, P^1_1)$ , qui calcule $1 \mathbin{\dot{-}} x$ , et $\mathrm{sg} = {\dot{-}} \circ (\mathbf 1, \overline{\mathrm{sg}})$ , qui calcule $1 \mathbin{\dot{-}} (1 \mathbin{\dot{-}} x)$ . Pour une fonction primitive récursive $f$ d'arité $n + 1$ , donnée avec une construction, où $f(v, z) = w$ désigne l'une de ses définitions naturelles, la somme $\Sigma_f(v, y) = \sum_{z < y} f(v, z)$ s'obtient par récurrence primitive à partir de $Z \circ P^n_1$ et de $\mathrm{add} \circ \big(P^{n+2}_{n+2}, f \circ (P^{n+2}_1, \dots, P^{n+2}_{n+1})\big)$ , et le produit $\Pi_f(v, y) = \prod_{z < y} f(v, z)$ à partir de $\mathbf 1 \circ P^n_1$ et de $\mathrm{mul} \circ \big(P^{n+2}_{n+2}, f \circ (P^{n+2}_1, \dots, P^{n+2}_{n+1})\big)$ . Pour $n = 0$ , la somme et le produit s'obtiennent sans paramètre, à partir des entiers $0$ et $1$ et de $\mathrm{add} \circ (P^2_2, f \circ P^2_1)$ et $\mathrm{mul} \circ (P^2_2, f \circ P^2_1)$ ; les énoncés et les preuves ci-dessous ne changent pas.

Énoncé

(i) Égalités et termes. Si $z$ ne figure pas dans le terme $t$ et si $t$ est substituable à $z$ dans $\chi$ , alors $\vdash \exists z\, (z = t \wedge \chi) \leftrightarrow \chi[t/z]$ . Soit $h = f \circ (g_1, \dots, g_m)$ , avec des définitions comme au point (iii) de Fonctions p.r. dans PA. Si $\vdash_{\mathsf{PA}} g_j(v) = z_j \leftrightarrow z_j = t_j$ pour chaque $j$ , où les $t_j$ sont des termes de variables parmi les $v_k$ , alors $\vdash_{\mathsf{PA}} h(v) = w \leftrightarrow f(t_1, \dots, t_m) = w$ , et, si de plus $\vdash_{\mathsf{PA}} f(z) = w \leftrightarrow w = t$ , alors $\vdash_{\mathsf{PA}} h(v) = w \leftrightarrow w = t[t_1, \dots, t_m / z_1, \dots, z_m]$ . La même preuve élimine celles des variables $z_j$ pour lesquelles $g_j$ est ainsi donnée par un terme. Enfin, pour des variables $e_1, \dots, e_m$ qui ne figurent dans aucune des définitions, $\{g_1(v) = e_1, \dots, g_m(v) = e_m\} \vdash_{\mathsf{PA}} h(v) = w \leftrightarrow f(e_1, \dots, e_m) = w$ : on calcule $h$ sur les valeurs $e_j$ .

(ii) Addition, multiplication. $\vdash_{\mathsf{PA}} \mathrm{add}(x, y) = w \leftrightarrow w = x + y$ , $\vdash_{\mathsf{PA}} \mathrm{mul}(x, y) = w \leftrightarrow w = x \times y$ et $\vdash_{\mathsf{PA}} \mathbf 1(x) = w \leftrightarrow w = S\,0$ .

(iii) Prédécesseur, soustraction tronquée. $\begin{aligned} &\vdash_{\mathsf{PA}} \mathrm{pr}(y) = w \\ &\quad \leftrightarrow \big((y = 0 \wedge w = 0) \vee y = S\,w\big), \\ &\vdash_{\mathsf{PA}} x \mathbin{\dot{-}} y = w \\ &\quad \leftrightarrow \big((x \leqslant y \wedge w = 0) \\ &\qquad \vee (y \leqslant x \wedge w + y = x)\big). \end{aligned}$

(iv) Signes. $\begin{aligned} &\vdash_{\mathsf{PA}} \overline{\mathrm{sg}}(x) = w \\ &\quad \leftrightarrow \big((x = 0 \wedge w = S\,0) \\ &\qquad \vee (\neg(x = 0) \wedge w = 0)\big), \\ &\vdash_{\mathsf{PA}} \mathrm{sg}(x) = w \\ &\quad \leftrightarrow \big((x = 0 \wedge w = 0) \\ &\qquad \vee (\neg(x = 0) \wedge w = S\,0)\big). \end{aligned}$

(v) Sommes et produits bornés. Pour une fonction primitive récursive $f$ d'arité $n + 1$ , donnée avec une construction, $\begin{aligned} &\vdash_{\mathsf{PA}} \Sigma_f(v, y) = 0 \\ &\qquad \leftrightarrow \forall z < y\ f(v, z) = 0, \\ &\vdash_{\mathsf{PA}} \neg(\Pi_f(v, y) = 0) \\ &\qquad \leftrightarrow \forall z < y\ \neg(f(v, z) = 0), \end{aligned}$ et, si $\vdash_{\mathsf{PA}} f(v, z) = w \to (w = 0 \vee w = S\,0)$ , alors $\vdash_{\mathsf{PA}} \Pi_f(v, y) = w \to (w = 0 \vee w = S\,0)$ .

Démonstration

(i) Sous l'hypothèse $z = t \wedge \chi$ , le remplacement d'un terme (Calcul à variables libres, (v)), appliqué à $\chi$ avec les termes $z$ et $t$ , donne $\chi[t/z]$ , où $z$ n'est pas libre puisqu'elle ne figure pas dans $t$ ; l'élimination de $z$ donne un sens. Pour l'autre, $(z = t \wedge \chi)[t/z]$ est $t = t \wedge \chi[t/z]$ , et l'introduction, avec le terme $t$ , et $\vdash t = t$ concluent. De même, si $z$ n'est pas libre dans $\alpha$ , l'introduction et l'élimination donnent $\vdash \exists z\, (\alpha \wedge \chi) \leftrightarrow (\alpha \wedge \exists z\, \chi)$ .

La formule $h(v) = w$ est $\exists z_1 \cdots \exists z_m\, (g_1(v) = z_1 \wedge \cdots \wedge g_m(v) = z_m \wedge f(z) = w)$ . Par la monotonie de Récurrence dans PA, (ii), et la règle des tautologies, elle équivaut à la formule où chaque $g_j(v) = z_j$ est remplacée par $z_j = t_j$ . Aucune $z_l$ ne figure dans les égalités $z_j = t_j$ pour $j \neq l$ : la seconde équivalence ci-dessus fait sortir chacune d'elles de la portée des $\exists z_l$ suivants, et la première, appliquée de l'intérieur vers l'extérieur, élimine $z_m$ , …, $z_1$ . Les termes $t_j$ ne contiennent aucune $z_l$ , et leurs variables ne sont pas quantifiées dans $\varphi_f$ : le résultat est $f(t_1, \dots, t_m) = w$ , puis $w = t[t_1, \dots, t_m / z_1, \dots, z_m]$ sous la seconde hypothèse, par le point (iv) de Récurrence dans PA.

Pour la dernière assertion, sous les hypothèses $g_j(v) = e_j$ et $h(v) = w$ , l'élimination fournit des variables nouvelles $d_j$ telles que $g_j(v) = d_j$ et $f(d_1, \dots, d_m) = w$ ; le point (ii) de Fonctions p.r. dans PA donne $d_j = e_j$ , et le remplacement donne $f(e_1, \dots, e_m) = w$ . Réciproquement, sous les hypothèses $g_j(v) = e_j$ et $f(e_1, \dots, e_m) = w$ , les introductions de $\exists z_m$ , …, $\exists z_1$ , avec les termes $e_m$ , …, $e_1$ , donnent $h(v) = w$ .

(ii) Par (i), $(S \circ P^3_3)(x, y, u) = w$ équivaut à $w = S\,u$ , et $P^1_1(x) = w$ est $w = x$ . Appliquons le point (v) de Fonctions p.r. dans PA à $\psi = (w = x + y)$ : $\psi[0/y]$ équivaut à $w = x$ par $\mathrm Q_4$ , et $\psi[S\,y/y]$ équivaut à $w = S(x + y)$ par $\mathrm Q_5$ , c'est-à-dire, par (i), à $\exists u\, (u = x + y \wedge w = S\,u)$ , qui équivaut par la monotonie à $\exists u\, (\psi[u/w] \wedge g(x, y, u) = w)$ . Pour la multiplication, (i) et ce qui précède donnent $\mathrm{add}(P^3_3, P^3_1)(x, y, u) = w \leftrightarrow w = u + x$ ; avec $\psi = (w = x \times y)$ , $\mathrm Q_6$ et $\mathrm Q_7$ donnent de même les deux hypothèses du point (v). Enfin $\mathbf 1(x) = w$ est $\exists z\, (z = 0 \wedge w = S\,z)$ , qui équivaut à $w = S\,0$ par (i).

(iii) Prédécesseur. Soit $\psi$ la formule $(y = 0 \wedge w = 0) \vee y = S\,w$ . La formule $\psi[0/y]$ équivaut à $w = 0$ , puisque $0 = S\,w$ est exclu par $\mathrm Q_1$ et la symétrie. La formule $\psi[S\,y/y]$ équivaut à $y = w$ , par $\mathrm Q_1$ , $\mathrm Q_2$ et la congruence. Comme $g(y, u) = w$ est ici $w = y$ , il reste à voir que $\exists u\, (\psi[u/w] \wedge w = y)$ équivaut à $w = y$ : par (i), elle équivaut à $w = y \wedge \exists u\, \psi[u/w]$ , et $\exists u\, \psi[u/w]$ est démontrable, avec le terme $0$ si $y = 0$ , et par l'instance $\neg(y = 0) \to \exists u\, (y = S\,u)$ de $\mathrm Q_3$ et la monotonie sinon. Le point (v) de Fonctions p.r. dans PA, sans paramètre, conclut.

Soustraction tronquée. Par (i) et ce qui précède, $g(x, y, u) = w$ équivaut à $(u = 0 \wedge w = 0) \vee u = S\,w$ . Soit $\psi$ la formule $(x \leqslant y \wedge w = 0) \vee (y \leqslant x \wedge w + y = x)$ . Pour $\psi[0/y]$ : $x \leqslant 0$ donne $x = 0$ (Ordre dans PA, (ii)), donc $w = x$ dans le premier cas, et $w + 0 = x$ donne $w = x$ dans le second ; réciproquement, $w = x$ donne le second cas, avec $0 \leqslant x$ . Pour $\psi[S\,y/y]$ , on raisonne par cas sur $x \leqslant y \vee y < x$ , qui découle des points (iv) et (v) du même nœud.

Si $x \leqslant y$ : alors $\psi[u/w]$ équivaut à $u = 0$ , puisque, dans le second cas, l'antisymétrie donne $x = y$ , puis $u + y = 0 + y$ et $u = 0$ par la simplification. Par (i), $\exists u\, (\psi[u/w] \wedge g(x, y, u) = w)$ équivaut à $(0 = 0 \wedge w = 0) \vee 0 = S\,w$ , c'est-à-dire à $w = 0$ . De son côté, $x \leqslant S\,y$ est vrai et $S\,y \leqslant x$ , qui avec $x \leqslant y$ donnerait $y < y$ , est exclu : $\psi[S\,y/y]$ équivaut aussi à $w = 0$ .

Si $y < x$ , c'est-à-dire $S\,y \leqslant x$ : alors $x \leqslant y$ est exclu, et $\psi[u/w]$ équivaut à $u + y = x$ . Le cas $u = 0$ donnerait $x = y$ , exclu ; par (i), $\exists u\, (u + y = x \wedge u = S\,w)$ équivaut à $S\,w + y = x$ , c'est-à-dire à $w + S\,y = x$ (Lois de + et ×, (i)). De son côté, le second cas de $\psi[S\,y/y]$ se réduit à $w + S\,y = x$ , et le premier, $x \leqslant S\,y \wedge w = 0$ , donne $x = S\,y$ par l'antisymétrie, donc $w + S\,y = 0 + S\,y = x$ : $\psi[S\,y/y]$ équivaut à $w + S\,y = x$ . Dans les deux cas, la seconde hypothèse du point (v) de Fonctions p.r. dans PA est établie, et ce point conclut.

(iv) Par (i) et (ii), $\overline{\mathrm{sg}}(x) = w$ équivaut à $S\,0 \mathbin{\dot{-}} x = w$ , c'est-à-dire, par (iii) et le point (iv) de Récurrence dans PA, à $(S\,0 \leqslant x \wedge w = 0) \vee (x \leqslant S\,0 \wedge w + x = S\,0)$ . Si $x = 0$ : le premier cas est exclu, puisque $S\,0 \leqslant 0$ donnerait $S\,0 = 0$ , et le second se réduit, avec $0 \leqslant S\,0$ , à $w + 0 = S\,0$ , c'est-à-dire à $w = S\,0$ . Si $x = S\,k$ , par l'instance de $\mathrm Q_3$ : $0 \leqslant k$ donne $S\,0 \leqslant S\,k$ par le point (v) de Ordre dans PA, et le premier cas se réduit à $w = 0$ ; le second, par le point (ii) du même nœud, donne $x \leqslant 0$ ou $x = S\,0$ , le premier cas donnant $S\,k = 0$ , contraire à $\mathrm Q_1$ , d'où $x = S\,0$ , puis $S\,w = w + S\,0 = S\,0$ et $w = 0$ par $\mathrm Q_2$ . La formule équivaut donc à $w = 0$ . Pour $\mathrm{sg}$ , (i) donne $\mathrm{sg}(x) = w \leftrightarrow \exists e\, (\overline{\mathrm{sg}}(x) = e \wedge S\,0 \mathbin{\dot{-}} e = w)$ , et $S\,0 \mathbin{\dot{-}} e = w$ équivaut à $\overline{\mathrm{sg}}(e) = w$ par ce qui précède, la définition de $\dot{-}$ qui figure dans celle de $\mathrm{sg}$ étant identifiée à celle de $\overline{\mathrm{sg}}$ par le point (vii) de Fonctions p.r. dans PA. Si $x = 0$ , l'unique valeur $e$ est $S\,0$ , et $\overline{\mathrm{sg}}(S\,0) = w$ équivaut à $w = 0$ ; sinon, $e = 0$ , et $\overline{\mathrm{sg}}(0) = w$ équivaut à $w = S\,0$ .

(v) Par (i) et (ii), la fonction initiale de $\Sigma_f$ est donnée par $w = 0$ , et $g(v, y, u) = w$ équivaut à $\exists e\, (f(v, y) = e \wedge w = u + e)$ ; pour $\Pi_f$ , ce sont $w = S\,0$ et $\exists e\, (f(v, y) = e \wedge w = u \times e)$ . Ici $f(v, y) = e$ est, par (i), la définition de $f$ qui figure dans la construction de $\Sigma_f$ ou de $\Pi_f$ , écrite avec les variables $v, y, e$ ; par le point (vii) de Fonctions p.r. dans PA, elle équivaut dans $\mathsf{PA}$ à la définition de $f$ de l'énoncé, où l'on a substitué $y$ et $e$ à $z$ et $w$ , ce qui permet d'écrire les conclusions avec celle-ci.

Somme. Montrons $\Sigma_f(v, y) = 0 \leftrightarrow \forall z < y\ f(v, z) = 0$ par récurrence sur $y$ . Pour $0$ , la première équation de Fonctions p.r. dans PA donne $\Sigma_f(v, 0) = 0$ , et le point (i) (a) de Modules de Gödel donne $\forall z < 0\ f(v, z) = 0$ . Pour le pas, la seconde équation donne $\Sigma_f(v, S\,y) = 0 \leftrightarrow \exists u\, \exists e\, (\Sigma_f(v, y) = u \wedge f(v, y) = e \wedge 0 = u + e)$ . Par le point (ii) de Lois de + et × et $0 + 0 = 0$ , $0 = u + e$ équivaut à $u = 0 \wedge e = 0$ , et (i) donne l'équivalence avec $\Sigma_f(v, y) = 0 \wedge f(v, y) = 0$ . L'hypothèse de récurrence et le point (i) (c) de Modules de Gödel, appliqué à la formule $f(v, z) = 0$ , concluent.

Produit. De même, $\Pi_f(v, 0) = 0$ équivaut à $0 = S\,0$ , exclu par $\mathrm Q_1$ . Pour le pas, $\Pi_f(v, S\,y) = 0$ équivaut à $\exists u\, \exists e\, (\Pi_f(v, y) = u \wedge f(v, y) = e \wedge 0 = u \times e)$ ; par l'intégrité et les égalités $0 \times e = 0$ , $u \times 0 = 0$ (Lois de + et ×, (iii), (iv)), $0 = u \times e$ équivaut à $u = 0 \vee e = 0$ , et l'existence des valeurs $u$ et $e$ , point (ii) de Fonctions p.r. dans PA, et (i) donnent l'équivalence avec $\Pi_f(v, y) = 0 \vee f(v, y) = 0$ . La contraposition, l'hypothèse de récurrence et le point (i) (c) de Modules de Gödel concluent.

Valeurs 0 et 1. Sous l'hypothèse sur $f$ , montrons $\forall w\, \big(\Pi_f(v, y) = w \to (w = 0 \vee w = S\,0)\big)$ par récurrence sur $y$ . Pour $0$ , $\Pi_f(v, 0) = w$ équivaut à $w = S\,0$ . Pour le pas, sous l'hypothèse $\Pi_f(v, S\,y) = w$ , l'élimination fournit $u$ et $e$ tels que $\Pi_f(v, y) = u$ , $f(v, y) = e$ et $w = u \times e$ ; l'hypothèse de récurrence, instanciée par $u$ , et l'hypothèse sur $f$ donnent $u, e \in \{0, S\,0\}$ au sens des disjonctions, et $u \times 0 = 0$ , $u \times S\,0 = u$ donnent $w = 0 \vee w = S\,0$ dans les quatre cas.

□

Remarque

L'addition et la multiplication du langage sont des symboles, alors que celles de Primitives récursives sont des fonctions construites par récurrence ; leurs définitions naturelles sont de longues formules, qui passent par la fonction $\beta$ . Le point (ii) dit que $\mathsf{PA}$ les démontre équivalentes à $w = x + y$ et à $w = x \times y$ : on retrouve, à l'intérieur de $\mathsf{PA}$ , le fait que les axiomes $\mathrm Q_4$ à $\mathrm Q_7$ sont les équations qui définissent l'addition et la multiplication par récurrence, comme chez Grassmann (troisième remarque du nœud Lois de + et ×). L'erreur la plus répandue est de croire que cette identification va de soi : elle demande le point (v) du nœud précédent, c'est-à-dire une récurrence dans $\mathsf{PA}$ .

Remarque

Les caractérisations (iii) et (iv) ont été vérifiées sur les entiers par un calcul : pour $x, y, w \leqslant 40$ , la formule de (iii) vaut exactement quand $w = x \mathbin{\dot{-}} y$ , et elle satisfait les deux équations de récurrence de la soustraction tronquée ; la variante $y \leqslant x \wedge w + y = x$ , sans le premier cas, viole la seconde dès $x = y = 0$ , ce qui montre que le cas $x \leqslant y$ n'est pas une précaution. Les sommes et les produits de (v) servent au nœud suivant, où ils traduisent les quantifications bornées de Clôture.

Repose sur

Les fonctions primitives récursives dans l'arithmétique de Peano

Sert à

Formule naturelle d'une relation primitive récursive et clauses de clôture dans l'arithmétique de Peano