Formules Δ₀ et Σ₁-complétude de l'arithmétique de Robinson

(i) Par récurrence sur la construction des formules Δ₀ : l'ensemble des formules Δ₀ $\varphi$ telles que $\varphi[t/v]$ soit Δ₀ pour tous $v$ et $t$ comme dans l'énoncé contient les formules atomiques, dont les substituées sont atomiques (Substitution, (iii)), et il est stable par $\neg$ et $\to$, qui commutent à la substitution. Soit $\varphi = \forall x\, (\exists z\, (z + x = u) \to \psi)$, avec $\psi$ dans cet ensemble. Si $v = x$, la variable $v$ n'est pas libre dans $\varphi$, qui ne change pas. Si $v = z$, ses occurrences dans $\exists z\, (z + x = u)$ sont liées, et $\varphi[t/v] = \forall x\, (\exists z\, (z + x = u) \to \psi[t/z])$. Sinon, $\varphi[t/v] = \forall x\, (\exists z\, (z + x = u[t/v]) \to \psi[t/v])$, et $u[t/v]$ ne contient ni $x$ ni $z$, puisque ni $u$ ni $t$ n'en contiennent, $x$ et $z$ étant quantifiées dans $\varphi$. Dans chaque cas, on obtient une quantification bornée d'une formule Δ₀.

(ii) Par récurrence sur la construction des formules Δ₀ ; la propriété démontrée porte sur $\varphi$ et sur toutes les valuations à la fois. On note $\vdash_{\mathsf Q}$ la démontrabilité dans $\mathsf Q$ et l'on emploie les règles de Calcul à variables libres.

Formules atomiques. Soit $\varphi = (t_1 = t_2)$, de sorte que $\varphi\langle s \rangle$ est $t'_1 = t'_2$, où les $t'_i$ sont des termes clos de valeurs $a$ et $b$, celles de $t_1$ et $t_2$ sous $s$. Par le point (i) de Calculs dans Q, $\vdash_{\mathsf Q} t'_1 = \underline a$ et $\vdash_{\mathsf Q} t'_2 = \underline b$. Si $a = b$, la symétrie et la transitivité donnent $\vdash_{\mathsf Q} t'_1 = t'_2$. Sinon, ces mêmes règles donnent $\vdash_{\mathsf Q} t'_1 = t'_2 \to \underline a = \underline b$, et le point (ii) de Calculs dans Q donne $\vdash_{\mathsf Q} \neg(t'_1 = t'_2)$ par contraposition.

Connecteurs. On a $(\neg\varphi)\langle s \rangle = \neg\, \varphi\langle s \rangle$ et $(\varphi \to \psi)\langle s \rangle = \varphi\langle s \rangle \to \psi\langle s \rangle$, puisque substituer un chiffre à une variable non libre ne change rien. Chacun des cas se conclut par la règle des tautologies : de $\varphi\langle s \rangle$ on tire $\neg\neg\varphi\langle s \rangle$ ; de $\neg\varphi\langle s \rangle$ ou de $\psi\langle s \rangle$, on tire $\varphi\langle s \rangle \to \psi\langle s \rangle$ ; de $\varphi\langle s \rangle$ et $\neg\psi\langle s \rangle$, on tire $\neg(\varphi\langle s \rangle \to \psi\langle s \rangle)$.

Quantification bornée. Soit $\varphi = \forall x\, (\exists z\, (z + x = t) \to \psi)$. Substituer un chiffre à une variable libre $v \neq x$ de $\varphi$ traverse $\forall x$ ; si $v = z$, elle ne touche que $\psi$, et $t$ ne contient ni $x$ ni $z$. Ainsi $$\varphi\langle s \rangle = \forall x\, \big(\exists z\, (z + x = t') \to \psi'\big),$$ où $t'$ est un terme clos, de valeur $m$, celle de $t$ sous $s$, et où $\psi'$ s'obtient en substituant à chaque variable libre $v \neq x$ de $\psi$ le chiffre $\underline{s(v)}$ ; pour tout entier $k$, $\psi'[\underline k/x] = \psi\langle s(x \mid k) \rangle$. La formule $\varphi$ est satisfaite sous $s$ si et seulement si $\psi$ l'est sous $s(x \mid k)$ pour tout $k \leqslant m$.

Supposons-le. Par l'hypothèse de récurrence, $\vdash_{\mathsf Q} \psi'[\underline k/x]$ pour tout $k \leqslant m$. Le remplacement d'un terme, appliqué à $\psi'$ avec les termes $x$ et $\underline k$, et la symétrie donnent $\vdash_{\mathsf Q} x = \underline k \to (\psi'[\underline k/x] \to \psi')$, donc $\vdash_{\mathsf Q} x = \underline k \to \psi'$, et le raisonnement par cas donne $\vdash_{\mathsf Q} D_m(x) \to \psi'$. Par (i) de Calculs dans Q, $\vdash_{\mathsf Q} t' = \underline m$, et le remplacement, appliqué à $\exists z\, (z + x = a)$ pour une variable $a$ nouvelle, donne $\vdash_{\mathsf Q} \exists z\, (z + x = t') \to \exists z\, (z + x = \underline m)$. Le point (v) de Calculs dans Q enchaîne : $\vdash_{\mathsf Q} \exists z\, (z + x = t') \to \psi'$, et la généralisation donne $\vdash_{\mathsf Q} \varphi\langle s \rangle$.

Sinon, soit $k \leqslant m$ tel que $\psi$ ne soit pas satisfaite sous $s(x \mid k)$ ; l'hypothèse de récurrence donne $\vdash_{\mathsf Q} \neg\psi'[\underline k/x]$. Par le point (iv) de Calculs dans Q, $\vdash_{\mathsf Q} \exists z\, (z + \underline k = \underline m)$, d'où $\vdash_{\mathsf Q} \exists z\, (z + \underline k = t')$ par le remplacement et la symétrie. Le chiffre $\underline k$ est clos, et $z \neq x$ : l'axiome (2) donne $$\vdash \varphi\langle s \rangle \to \big(\exists z\, (z + \underline k = t') \to \psi'[\underline k/x]\big),$$ et la règle des tautologies donne $\vdash_{\mathsf Q} \neg\varphi\langle s \rangle$.

(iii) Soit $\sigma = \exists y_1 \cdots \exists y_k\ \delta$ un énoncé Σ₁ vrai dans $\mathcal N$, les $y_i$ distincts et $\delta$ Δ₀. Par la définition de la satisfaction de $\exists = \neg\forall\neg$, il existe des entiers $m_1, \dots, m_k$ tels que $\delta$ soit satisfaite sous toute valuation $s$ qui vaut $m_i$ en $y_i$ ; les variables libres de $\delta$ sont parmi les $y_i$. Par (ii), $\vdash_{\mathsf Q} \delta\langle s \rangle$. Pour $j \leqslant k$, soit $\theta_j$ l'énoncé obtenu en substituant $\underline{m_1}, \dots, \underline{m_j}$ à $y_1, \dots, y_j$ dans $\exists y_{j+1} \cdots \exists y_k\ \delta$ ; ainsi $\theta_k = \delta\langle s \rangle$ et $\theta_0 = \sigma$. Comme les $y_i$ sont distincts, $\theta_{j-1} = \exists y_j\, \chi$, où $\chi$ est une formule telle que $\theta_j = \chi[\underline{m_j}/y_j]$, et l'introduction de l'existentiel donne $\vdash \theta_j \to \theta_{j-1}$. De proche en proche, $\vdash_{\mathsf Q} \sigma$.