Proposition 1Lemme diagonal et démontrabilité

Représentation des fonctions récursives totales

Les conventions sont celles de Calculs dans Q et de Σ₁-complétude : $\underline n$ est le chiffre de $n$ , et $t \leqslant u$ , comme les quantifications bornées, s'écrit avec le témoin à gauche. Une théorie $T$ contient $\mathsf Q$ si elle en démontre les axiomes ; elle démontre alors tout ce que démontre $\mathsf Q$ (Gödel-Rosser).

Soit $v_1, \dots, v_k, w$ des variables distinctes. Pour une formule $\alpha$ dont les variables libres sont parmi elles et pour $a = (a_1, \dots, a_k) \in {\mathbb N^k}$ , on note $\alpha_a$ la formule obtenue en substituant à chaque $v_i$ le chiffre $\underline{a_i}$ ; ces termes sont clos, donc substituables, et l'ordre des substitutions est indifférent. Les variables libres de $\alpha_a$ sont parmi $w$ , et, pour un entier $c$ , $\alpha_a[\underline c/w]$ est l'énoncé $\alpha\langle s \rangle$ de Σ₁-complétude, pour une valuation $s$ qui vaut $a_i$ en $v_i$ et $c$ en $w$ .

Une fonction totale $f : \mathbb N^k \to \mathbb N$ est représentable dans $T$ s'il existe une formule $\varphi$ , de variables libres parmi $v_1, \dots, v_k, w$ , telle que, pour tout $a \in \mathbb N^k$ , $T \vdash \forall w\, \big(\varphi_a \leftrightarrow w = \underline{f(a)}\big) ;$ on dit que $\varphi$ représente $f$ dans $T$ . Le graphe de $f$ est la relation $\{(a, b) \in \mathbb N^{k+1} : f(a) = b\}$ .

Énoncé

Soit $T$ une théorie qui contient $\mathsf Q$ , et $f : \mathbb N^k \to \mathbb N$ une fonction totale.

(i) Si $f$ est récursive, son graphe est une relation récursive.

(ii) Plus petit témoin. Soit $\theta$ une formule, de variables libres parmi $v_1, \dots, v_k, w$ , qui représente le graphe de $f$ dans $T$ au sens de Astuce de Rosser : pour tous $a \in \mathbb N^k$ et $c \in \mathbb N$ , $T \vdash \theta_a[\underline c/w]$ si $c = f(a)$ , et $T \vdash \neg\theta_a[\underline c/w]$ sinon. Soit $z$ et $u$ deux variables distinctes, qui ne figurent pas dans $\theta$ et sont distinctes des $v_i$ et de $w$ . La formule $\begin{aligned} \varphi = \theta \wedge \forall z \leqslant w\ \big(&z = w \\ &\vee \neg\theta[z/w]\big), \end{aligned}$ où la quantification bornée est écrite avec la variable $u$ , représente $f$ dans $T$ .

(iii) Toute fonction récursive totale est représentable dans $\mathsf Q$ et dans $T$ , avec des variables distinctes $v_1, \dots, v_k, w$ données.

Démonstration

(i) La fonction caractéristique du graphe est $(a, b) \mapsto \chi_=\big(f(a), b\big)$ : c'est la relation $x = y$ , primitive récursive par le point (i) de Clôture, composée avec les fonctions récursives totales $(a, b) \mapsto f(a)$ et $(a, b) \mapsto b$ . Elle est récursive par le point (ii) de Fonctions récursives.

(ii) Comme $z$ ne figure pas dans $\theta$ , elle y est substituable à $w$ , et $\theta[z/w]$ porte la lettre $z$ exactement aux places des occurrences libres de $w$ dans $\theta$ . Les variables libres de $\varphi$ sont parmi $v_1, \dots, v_k, w$ .

Fixons $a \in \mathbb N^k$ et posons $b = f(a)$ . Substituer un chiffre à $v_i$ traverse les blocs $\forall z$ et $\forall u$ , puisque $v_i$ est distincte de $z$ et de $u$ , et commute avec la substitution de $z$ à $w$ , puisque les chiffres n'ont pas de variable et que $z \neq v_i$ . Ainsi $\varphi_a = \theta_a \wedge B_a$ , avec $\begin{aligned} B_a = \forall z\, \Big(&\exists u\, (u + z = w) \\ &\to \big(z = w \vee \neg\theta_a[z/w]\big)\Big). \end{aligned}$ Comme $z$ ne figure pas dans $\theta_a$ , on a $\theta_a[z/w][\underline c/z] = \theta_a[\underline c/w]$ pour tout entier $c$ . Par hypothèse, $T \vdash \theta_a[\underline b/w]$ , et $T \vdash \neg\theta_a[\underline c/w]$ pour $c \neq b$ . On emploie les règles de Calcul à variables libres : une variable est toujours substituable à elle-même, puisqu'une occurrence libre de $y$ n'est dans la portée d'aucun $\forall y$ , et un chiffre, qui est clos, est substituable à toute variable.

La théorie $T$ démontre $\varphi_a[\underline b/w]$ . Soit $c \leqslant b$ . Si $c = b$ , l'instance $P \to (P \vee Q)$ donne $\vdash z = \underline b \to (z = \underline b \vee \neg\theta_a[z/w])$ . Si $c < b$ , le remplacement d'un terme (point (v) de Calcul à variables libres), appliqué à la formule $\neg\theta_a[z/w]$ , à la variable $z$ et aux termes $\underline c$ et $z$ , donne $\vdash \underline c = z \to (\neg\theta_a[\underline c/w] \to \neg\theta_a[z/w])$ ; avec la symétrie de l'égalité et $T \vdash \neg\theta_a[\underline c/w]$ , il vient $T \vdash z = \underline c \to \neg\theta_a[z/w]$ , puis $T \vdash z = \underline c \to (z = \underline b \vee \neg\theta_a[z/w])$ par l'instance $Q \to (P \vee Q)$ . Le raisonnement par cas sur $D_b(z)$ de Calculs dans Q, puis le point (v) de ce nœud, $\mathsf Q \vdash \exists u\, (u + z = \underline b) \to D_b(z)$ , donnent $\begin{aligned} T \vdash {}&\exists u\, (u + z = \underline b) \\ &\to \big(z = \underline b \vee \neg\theta_a[z/w]\big). \end{aligned}$ Les seules occurrences libres de $w$ dans $B_a$ sont celles de $u + z = w$ et de $z = w$ ; la généralisation en $z$ (Règles dérivées, (ii)) donne donc $T \vdash B_a[\underline b/w]$ . Avec $T \vdash \theta_a[\underline b/w]$ , la règle des tautologies donne $T \vdash \varphi_a[\underline b/w]$ .

Si $w = \underline b$ , alors $\varphi_a$ . Le remplacement d'un terme, appliqué à $\varphi_a$ , à la variable $w$ et aux termes $\underline b$ et $w$ , et la symétrie donnent $\vdash w = \underline b \to (\varphi_a[\underline b/w] \to \varphi_a)$ , d'où $T \vdash w = \underline b \to \varphi_a$ .

Si $\varphi_a$ , alors $w = \underline b$ . Par le point (vi) de Calculs dans Q, $T \vdash \exists u\, (u + w = \underline b) \vee \exists u\, (u + \underline b = w)$ : ce sont les formules $w \leqslant \underline b$ et $\underline b \leqslant w$ , écrites avec la variable liée $u$ . On traite les deux termes de la disjonction.

Le chiffre $\underline b$ est clos et $u \neq z$ : l'axiome (2), qui instancie $z$ par $\underline b$ dans $B_a$ , donne $\begin{aligned} \vdash B_a \to \Big(&\exists u\, (u + \underline b = w) \\ &\to \big(\underline b = w \vee \neg\theta_a[\underline b/w]\big)\Big). \end{aligned}$ Avec $T \vdash \theta_a[\underline b/w]$ , la symétrie et la règle des tautologies, $T \vdash \exists u\, (u + \underline b = w) \to (B_a \to w = \underline b)$ .

Par le point (v) de Calculs dans Q, $T \vdash \exists u\, (u + w = \underline b) \to D_b(w)$ . Pour $c < b$ , le remplacement d'un terme, appliqué à $\theta_a$ , à la variable $w$ et aux termes $w$ et $\underline c$ , donne $\vdash w = \underline c \to (\theta_a \to \theta_a[\underline c/w])$ , et, avec $T \vdash \neg\theta_a[\underline c/w]$ , la règle des tautologies donne $T \vdash w = \underline c \to (\theta_a \to w = \underline b)$ ; pour $c = b$ , c'est une instance de tautologie. Le raisonnement par cas donne $T \vdash D_b(w) \to (\theta_a \to w = \underline b)$ , d'où $T \vdash \exists u\, (u + w = \underline b) \to (\theta_a \to w = \underline b)$ .

La règle des tautologies, appliquée à la disjonction et à ces deux implications, donne $T \vdash \theta_a \to (B_a \to w = \underline b)$ , puis $T \vdash \varphi_a \to w = \underline b$ par l'instance $(P \to (Q \to R)) \to ((P \wedge Q) \to R)$ .

Conclusion. L'instance $(P \to Q) \to ((Q \to P) \to (P \leftrightarrow Q))$ donne $T \vdash \varphi_a \leftrightarrow w = \underline b$ , et la généralisation en $w$ donne $T \vdash \forall w\, (\varphi_a \leftrightarrow w = \underline b)$ . Aucune hypothèse à variable libre n'a été introduite : toutes les généralisations portent sur des théorèmes de $T$ .

(iii) Par (i), le graphe de $f$ est une relation récursive de $\mathbb N^{k+1}$ . Par le point (ii) de Astuce de Rosser, il est représentable dans $\mathsf Q$ , et dans $T$ , par une formule $\theta$ de variables libres parmi $v_1, \dots, v_k, w$ , prises pour les variables de la définition ; (ii) conclut.

□

Remarque

Représenter le graphe ne suffit pas. Pour l'identité de $\mathbb N$ , avec $k = 1$ , la formule $\theta = \big(w = v_1 \vee \neg(0 + w = w)\big)$ représente le graphe dans $\mathsf Q$ : pour $c = n$ , la réflexivité de l'égalité donne $\mathsf Q \vdash \theta_n[\underline c/w]$ ; pour $c \neq n$ , $\mathsf Q$ démontre $\neg(\underline c = \underline n)$ et $0 + \underline c = \underline c$ par les points (i) et (ii) de Calculs dans Q, donc $\neg\theta_n[\underline c/w]$ . Soit $\mathcal M$ la structure de la deuxième remarque de ce même nœud, où $0 + a = b \neq a$ . L'élément $a$ y satisfait $\theta_0 = \big(w = 0 \vee \neg(0 + w = w)\big)$ sans être égal à $0$ , et le théorème de correction montre que $\mathsf Q$ ne démontre pas $\forall w\, (\theta_0 \to w = 0)$ . La clause du plus petit témoin écarte $a$ : on a $a + 0 = a$ , donc $0 \leqslant a$ dans $\mathcal M$ , et $0$ , différent de $a$ , satisfait $\theta_0$ . L'erreur la plus répandue est de croire qu'une formule qui donne la bonne réponse sur chaque chiffre définit une fonction aux yeux de la théorie ; c'est le point (vi) de Calculs dans Q, « $w \leqslant \underline b$ ou $\underline b \leqslant w$ », qui ramène tout élément, standard ou non, à la comparaison avec le chiffre $\underline b$ .

Remarque

La clause $\forall z \leqslant w\ (z = w \vee \cdots)$ dit qu'aucun $z < w$ ne convient : c'est la forme de la minimisation au point (ii) de Forme Σ₁ des r.e., et la même comparaison des témoins que dans la séparation de Rosser. Elle ne demande rien de plus à $\mathsf Q$ que les calculs sur les chiffres, sans aucune récurrence interne.

Repose sur

Représentation dans l'arithmétique de Robinson et théorème de Gödel-Rosser

Sert à

Lemme diagonal