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

(i) Sous les hypothèses $\chi_R(v) = e$, $\neg(e = 0)$ et $\chi_R(v) = 0$, le point (ii) de Fonctions p.r. dans PA donne $e = 0$, contradiction ; l'élimination de $e$ donne $\hat R(v) \to \neg(\chi_R(v) = 0)$. Réciproquement, ce point fournit $e$ tel que $\chi_R(v) = e$ ; si $e = 0$, le remplacement donne $\chi_R(v) = 0$, et sinon l'introduction donne $\hat R(v)$. La formule $\chi_R(v) = 0$ est dans $\mathcal S$ par le point (i) du même nœud. Si $\chi_R$ est booléenne, $\chi_R(v) = e$ et $\neg(e = 0)$ donnent $e = S\,0$, et réciproquement $\chi_R(v) = S\,0$ et $\neg(S\,0 = 0)$ donnent $\hat R(v)$.

Dans la suite, pour une fonction caractéristique donnée par une composition $f \circ (g_1, \dots, g_m)$, on raisonne sous des hypothèses $g_j(v) = e_j$, dont les variables $e_j$ existent par le point (ii) de Fonctions p.r. dans PA et s'éliminent à la fin : le point (i) de Fonctions usuelles dans PA ramène alors la valeur de la composée à $f(e_1, \dots, e_m)$, c'est ce qu'on appelle l'écrire avec les valeurs $e_j$. La définition de $\chi_R$ qui figure dans celle de $\chi_{\neg R}$, de $\chi_{R \wedge R'}$, de $\chi_{R \vee R'}$, de $\chi_R \circ (g_1, \dots, g_m)$, de $\Sigma_{\chi_R}$, de $\Pi_{\chi_R}$ ou de $f'$ est écrite avec d'autres variables que celle qui sert à $\hat R$ ; le point (vii) de Fonctions p.r. dans PA les identifie, et l'on emploie librement l'une pour l'autre. On emploie (i) pour passer de $\hat R$ à $\neg(\chi_R(v) = 0)$ et de $\neg\hat R$ à $\chi_R(v) = 0$.

(ii) Par le point (iv) de Fonctions usuelles dans PA, $\neg(\overline{\mathrm{sg}}(e) = 0)$ équivaut à $e = 0$, et $\neg(\mathrm{sg}(e) = 0)$ à $\neg(e = 0)$ ; les valeurs de $\overline{\mathrm{sg}}$ et de $\mathrm{sg}$ sont $0$ ou $S\,0$, ce qui donne les trois fonctions booléennes. Par le point (iii) du même nœud, $v_1 \mathbin{\dot{-}} v_2 = 0$ équivaut à $v_1 \leqslant v_2 \vee (v_2 \leqslant v_1 \wedge 0 + v_2 = v_1)$, donc à $v_1 \leqslant v_2$, puisque le second cas donne $v_1 = v_2$. Ainsi $\hat R(v_1, v_2)$ équivaut à $v_1 \leqslant v_2$ pour $\chi_\leqslant$, et à $\neg(v_2 \leqslant v_1)$ pour $\chi_<$, qui équivaut à $v_1 < v_2$ par les points (iv) et (v) de Ordre dans PA. Pour $\chi_=$, $\hat R(v_1, v_2)$ équivaut à $(v_1 \mathbin{\dot{-}} v_2) + (v_2 \mathbin{\dot{-}} v_1) = 0$, écrite avec les valeurs $e$, $e'$ des deux différences, puis, par le point (ii) de Lois de + et ×, à $e = 0 \wedge e' = 0$, c'est-à-dire à $v_1 \leqslant v_2 \wedge v_2 \leqslant v_1$, qui équivaut à $v_1 = v_2$ par l'antisymétrie et la réflexivité.

(iii) Par (i) et le point (iv) de Fonctions usuelles dans PA, $\widehat{\neg R}$ équivaut à $\neg(\overline{\mathrm{sg}}(\chi_R(v)) = 0)$, écrite avec la valeur $e$ de $\chi_R(v)$, donc à $e = 0$, c'est-à-dire à $\chi_R(v) = 0$, et à $\neg\hat R$. Pour $R \wedge R'$, avec les valeurs $e$ et $e'$, $\neg(e \times e' = 0)$ équivaut à $\neg(e = 0) \wedge \neg(e' = 0)$ par l'intégrité et $0 \times e' = 0$, $e \times 0 = 0$ ; pour $R \vee R'$, $\neg(\mathrm{sg}(e + e') = 0)$ équivaut à $\neg(e + e' = 0)$, donc à $\neg(e = 0) \vee \neg(e' = 0)$ par le point (ii) de Lois de + et ×. Pour la substitution, $\exists w\, (\exists z\, (\cdots \wedge \chi_R(z) = w) \wedge \neg(w = 0))$ équivaut à $\exists z\, (\cdots \wedge \hat R(z))$ par les règles du point (i) de Fonctions usuelles dans PA et l'échange de deux quantificateurs existentiels, qui découle de l'introduction et de l'élimination. Les valeurs de $\overline{\mathrm{sg}}$ et de $\mathrm{sg}$ sont $0$ ou $S\,0$ ; un produit de deux éléments de $\{0, S\,0\}$ y est encore, par $e \times 0 = 0$ et $e \times S\,0 = e$ ; et une instance de $\chi_R(z) = w \to (w = 0 \vee w = S\,0)$ donne la dernière assertion.

(iv) Par (i) et le point (iv) de Fonctions usuelles dans PA, $\widehat{\exists z < y\, R}$ équivaut à $\neg(\Sigma_{\chi_R}(v, y) = 0)$, donc, par le point (v) du même nœud, à $\neg\forall z < y\ \chi_R(v, z) = 0$. Par (i), $\chi_R(v, z) = 0$ équivaut à $\neg\hat R(v, z)$, et le point (vii) (e) de Ordre dans PA, appliqué sous la borne aux deux implications, donne $\neg\forall z < y\ \neg\hat R(v, z)$, qui est $\exists z < y\ \hat R$. De même, $\widehat{\forall z < y\, R}$ est $\exists w\, (\Pi_{\chi_R}(v, y) = w \wedge \neg(w = 0))$, qui équivaut par (i) à $\neg(\Pi_{\chi_R}(v, y) = 0)$, donc à $\forall z < y\ \neg(\chi_R(v, z) = 0)$, c'est-à-dire à $\forall z < y\ \hat R$. Les assertions sur les fonctions booléennes viennent de $\mathrm{sg}$ et du point (v) du même nœud.

(v) Par récurrence sur $k$, les points (i) et (ii) de Fonctions usuelles dans PA montrent que, sous les hypothèses $g_l(v) = y_l$ et $\chi_{R_l}(v) = c_l$, avec les valeurs $y_l$ et $c_l$, la formule $f(v) = w$ équivaut à $w = (\cdots(y_1 \times c_1 + y_2 \times c_2) + \cdots) + y_k \times c_k$, et $g_i(v) = w$ à $w = y_i$. Sous l'hypothèse supplémentaire $\hat R_i(v) \wedge \bigwedge_{l \neq i} \neg\hat R_l(v)$, le point (i), le caractère booléen et l'unicité des valeurs donnent $c_i = S\,0$ et $c_l = 0$ pour $l \neq i$ ; les égalités $y \times 0 = 0$, $y \times S\,0 = y$, $0 + t = t$ et $t + 0 = t$ (Lois de + et ×) réduisent la somme à $y_i$, d'où $f(v) = w \leftrightarrow g_i(v) = w$. On élimine enfin les valeurs, qui existent par le point (ii) de Fonctions p.r. dans PA et ne figurent pas dans la conclusion.

(vi) Notons $N(t)$ la formule $\forall z < t\ \neg\hat R(v, z)$ et $\psi$ le second membre. Par le point (iv) de Fonctions usuelles dans PA, $f'$ est booléenne et $\neg(f'(v, z) = 0)$ équivaut à $\chi_R(v, z) = 0$, donc à $\neg\hat R(v, z)$. Par les points (v) et (i) du même nœud, $p$ est booléenne et $\neg(p(v, t) = 0)$ équivaut à $N(S\,t)$ ; ainsi $p(v, t) = S\,0 \leftrightarrow N(S\,t)$ et $p(v, t) = 0 \leftrightarrow \neg N(S\,t)$. Par le point (i) du même nœud, $g(v, y, u) = w$ équivaut à $\exists e\, (p(v, y) = e \wedge w = u + e)$. Appliquons le point (v) de Fonctions p.r. dans PA à $\psi$.

Pour $0$ : $w < 0$ est exclu, et $N(0)$ est démontrable (Modules de Gödel, (i) (a)), donc $\psi[0/y]$ équivaut à $w = 0$. Pour $S\,y$, le point (i) (c) du même nœud donne $N(S\,y) \leftrightarrow (N(y) \wedge \neg\hat R(v, y))$, et l'on raisonne par cas.

Si $N(S\,y)$ : alors $p(v, y) = S\,0$, et le second membre de la seconde hypothèse équivaut à $\exists u\, (\psi[u/w] \wedge w = u + S\,0)$. Sous $N(y)$, la formule $\psi[u/w]$ équivaut à $u = y$, puisque $u < y$ et $\hat R(v, u)$ contrediraient $N(y)$ ; le tout équivaut donc à $w = S\,y$. De même, $\psi[S\,y/y]$ équivaut à $w = S\,y$, puisque $w < S\,y$ et $\hat R(v, w)$ contrediraient $N(S\,y)$.

Si $\neg N(S\,y)$ : alors $p(v, y) = 0$, et le second membre équivaut à $\exists u\, (\psi[u/w] \wedge w = u + 0)$, c'est-à-dire à $\psi$, par (i) de Fonctions usuelles dans PA et $\mathrm Q_4$ ; il reste à voir $\psi[S\,y/y] \leftrightarrow \psi$, dont les seconds cas sont exclus pour $S\,y$. Sous $N(y)$, on a $\hat R(v, y)$ ; $\psi$ équivaut à $w = y$, et $\psi[S\,y/y]$ aussi : $w = y$ en est un témoin, et, si $w < S\,y$ et $\hat R(v, w)$ et $N(w)$, alors $w < y$ contredirait $N(y)$, donc $w = y$. Sous $\neg N(y)$, $\psi$ se réduit à son premier cas, $w = y$ étant exclu, et les premiers cas pour $y$ et pour $S\,y$ sont équivalents : $w < y$ donne $w < S\,y$, et réciproquement $w < S\,y$ donne $w < y$ ou $w = y$, et $w = y$ avec $N(w)$ contredirait $\neg N(y)$.