Séparation de Rosser et représentation des relations récursives

(i) Par le point (ii) de Forme Σ₁ des r.e. et le renommage de sa preuve, $A$ et $B$ sont définis, avec les variables $v_1, \dots, v_k$, par des formules $\exists y\, \alpha$ et $\exists y\, \beta$, avec la même variable $y$, distincte des $v_i$, où $\alpha$ et $\beta$ sont Δ₀ et ont leurs variables libres parmi $v_1, \dots, v_k, y$. Soit $z$ une variable qui ne figure ni dans $\alpha$ ni dans $\beta$ et qui est distincte des $v_i$ et de $y$, et $\beta' = \beta[z/y]$, formule Δ₀ par le point (i) de Σ₁-complétude. On pose $$\theta = \exists y\, \big(\alpha \wedge \forall z \leqslant y\ \neg\beta'\big),$$ où la variable liée $u$ de la borne est nouvelle. C'est une formule Σ₁, de variables libres parmi les $v_i$. Fixons $a \in \mathbb N^k$, et notons $\alpha_a$, $\beta'_a$ les formules obtenues en substituant les chiffres $\underline{a_i}$ aux $v_i$ ; ainsi $\theta(\underline a) = \exists y\, (\alpha_a \wedge \forall z \leqslant y\ \neg\beta'_a)$. Par le lemme de substitution, pour tout entier $j$, l'énoncé $\alpha_a[\underline j/y]$ est vrai dans $\mathcal N$ si et seulement si $\alpha$ est satisfaite sous une valuation qui vaut $a_i$ en $v_i$ et $j$ en $y$, et de même pour $\beta'_a[\underline j/z]$, qui est l'énoncé $\beta_a[\underline j/y]$.

Si $a \in A$. Il existe $m$ tel que $\alpha_a[\underline m/y]$ soit vrai. Comme $a \notin B$, aucun $\beta'_a[\underline j/z]$ n'est vrai ; l'énoncé $(\alpha_a \wedge \forall z \leqslant y\ \neg\beta'_a)[\underline m/y]$ est donc vrai dans $\mathcal N$. Ainsi $\theta(\underline a)$ est vrai ; c'est un énoncé Σ₁, la formule $\alpha_a \wedge \forall z \leqslant y\ \neg\beta'_a$ étant Δ₀ par le point (i) de Σ₁-complétude, et il est démontrable dans $\mathsf Q$ par le point (iii) de Σ₁-complétude.

Si $a \in B$. Il existe $m$ tel que $\beta'_a[\underline m/z]$ soit vrai, donc démontrable dans $\mathsf Q$ par le point (ii) de Σ₁-complétude. Comme $a \notin A$, pour tout $j \leqslant m$, l'énoncé $\alpha_a[\underline j/y]$ est faux, et $\mathsf Q \vdash \neg\alpha_a[\underline j/y]$ par ce même point. Soit $\bot$ l'énoncé $\neg(0 = 0)$, réfuté par $\vdash 0 = 0$. Montrons $$\mathsf Q \cup \{\alpha_a,\ \forall z \leqslant y\ \neg\beta'_a\} \vdash \bot,$$ en employant les règles de Calcul à variables libres. Par le point (vi) de Calculs dans Q, $y \leqslant \underline m \vee \underline m \leqslant y$, la seconde formule étant écrite avec la variable liée $u$.

Sous l'hypothèse $\underline m \leqslant y$, c'est-à-dire $\exists u\, (u + \underline m = y)$ : le chiffre $\underline m$ est clos et $u \neq z$, donc l'axiome (2) donne $\forall z \leqslant y\ \neg\beta'_a \to (\exists u\, (u + \underline m = y) \to \neg\beta'_a[\underline m/z])$, d'où $\neg\beta'_a[\underline m/z]$, qui contredit $\beta'_a[\underline m/z]$.

Sous l'hypothèse $y \leqslant \underline m$ : par le point (v) de Calculs dans Q, $D_m(y)$. Pour $j \leqslant m$, le remplacement d'un terme, appliqué à $\alpha_a$ avec les termes $y$ et $\underline j$, donne $\vdash y = \underline j \to (\alpha_a \to \alpha_a[\underline j/y])$, et $\mathsf Q \vdash \neg\alpha_a[\underline j/y]$ : donc $\mathsf Q \vdash y = \underline j \to \neg\alpha_a$, et le raisonnement par cas donne $\neg\alpha_a$, qui contredit l'hypothèse $\alpha_a$.

Dans les deux cas, on obtient $\bot$ par l'instance $P \to (\neg P \to Q)$, et le raisonnement par cas sur la disjonction conclut. Le théorème de la déduction donne $\mathsf Q \vdash (\alpha_a \wedge \forall z \leqslant y\ \neg\beta'_a) \to \bot$, après l'instance $(P \to (Q \to R)) \to ((P \wedge Q) \to R)$. La variable $y$ n'est pas libre dans $\bot$ : l'élimination donne $\mathsf Q \vdash \theta(\underline a) \to \bot$, et la règle des tautologies, avec $\vdash \neg\bot$, donne $\mathsf Q \vdash \neg\theta(\underline a)$.

(ii) La relation $R$ et son complémentaire sont récursivement énumérables et disjoints (Récursif, r.e., (i) et (ii)) ; la formule $\theta$ de (i), pour $A = R$ et $B = \mathbb N^k \setminus R$, représente $R$ dans $\mathsf Q$. Si une théorie $T$ démontre les axiomes de $\mathsf Q$, elle démontre tout ce que démontre $\mathsf Q$, par le lemme de remplacement de la preuve de Théorème de Craig.