Troisième condition de dérivabilité, théorème de Löb et second théorème d'incomplétude pour la formule naturelle

(i) Soit $\sigma$ un énoncé de $\mathcal S$. Le point (ii) de Collection et forme Σ₁ lui associe une formule $\exists y\, \delta_0$, où $\delta_0$ est Δ₀ et a ses variables libres parmi $y$, telle que $\vdash_{\mathsf{PA}} \sigma \leftrightarrow \exists y\, \delta_0$. Soit $y^*$ la variable $y$ si elle est distincte de $p$, une variable nouvelle sinon ; par le renommage de la preuve de Collection et forme Σ₁, (ii), $\vdash \exists y\, \delta_0 \leftrightarrow \exists y^*\, \delta_0[y^*/y]$, et $\delta_0[y^*/y]$ est Δ₀ par le point (i) de Σ₁-complétude. Le point (i) de Σ₁-complétude formalisée, avec la partie $\{p, y^*\}$, fournit une formule Δ₀ propre $\delta^*$, de variables libres parmi $y^*$, où ne figure pas $p$ et où $y^*$ n'est pas quantifiée, telle que $\vdash \delta_0[y^*/y] \leftrightarrow \delta^*$ ; la monotonie (Récurrence dans PA, (ii)) donne $\vdash_{\mathsf{PA}} \sigma \leftrightarrow \exists y^*\, \delta^*$.

Le point (iii) de Σ₁-complétude formalisée, sans paramètre et avec la variable $y^*$, donne $\vdash_{\mathsf{PA}} \exists y^*\, \delta^* \to \mathrm{Prf}_T\,\ulcorner \exists y^*\, \delta^* \urcorner$. Comme $T$ démontre les axiomes de $\mathsf{PA}$, $T \vdash \exists y^*\, \delta^* \to \sigma$ ; le point (i) de Instanciation formalisée donne $\vdash_{\mathsf{PA}} \mathrm{Prf}_T\,\ulcorner \exists y^*\, \delta^* \to \sigma \urcorner$, et le point (iv) de Instanciation à plusieurs paramètres, sans paramètre, donne $\vdash_{\mathsf{PA}} \mathrm{Prf}_T\,\ulcorner \exists y^*\, \delta^* \urcorner \to \mathrm{Prf}_T\,\ulcorner \sigma \urcorner$. Enfin, $\sigma$ étant un énoncé, $\vdash_{\mathsf{PA}} \mathrm{Prf}_T\,\ulcorner \sigma \urcorner \leftrightarrow \mathrm{Pr}_T\,\ulcorner \sigma \urcorner$ par le même point (i) de Instanciation formalisée, et la règle des tautologies enchaîne : $\vdash_{\mathsf{PA}} \sigma \to \mathrm{Pr}_T\,\ulcorner \sigma \urcorner$.

(ii) La formule $\mathrm{Pr}_T$ est dans $\mathcal S$ et n'a pas d'autre variable libre que $v$ (Deuxième condition (D2), (i)) ; par le point (i) de Fonctions p.r. dans PA, $\mathrm{Pr}_T\,\ulcorner \varphi \urcorner = \mathrm{Pr}_T[\underline{\ulcorner \varphi \urcorner}/v]$ est un énoncé de $\mathcal S$, puisque le chiffre n'a pas de variable. Le point (i), appliqué à $\sigma = \mathrm{Pr}_T\,\ulcorner \varphi \urcorner$, est la troisième condition. La formule $\exists y\, \delta$ est Σ₁, donc dans $\mathcal S$, et $(\exists y\, \delta)[\underline{\ulcorner \varphi \urcorner}/v]$ est un énoncé de $\mathcal S$ ; le point (i) donne $\vdash_{\mathsf{PA}} (\exists y\, \delta)[\underline{\ulcorner \varphi \urcorner}/v] \to \mathrm{Pr}_T\,\ulcorner (\exists y\, \delta)[\underline{\ulcorner \varphi \urcorner}/v] \urcorner$, et l'équivalence $\vdash_{\mathsf{PA}} \mathrm{Pr}_T \leftrightarrow \exists y\, \delta$, instanciée par le chiffre du code de ce dernier énoncé (Récurrence dans PA, (iv)), donne la troisième condition pour $\exists y\, \delta$. Une théorie qui démontre les axiomes de $\mathsf{PA}$ démontre tout ce que démontre $\mathsf{PA}$, par le lemme de remplacement de la preuve du théorème de Craig.

(iii) La théorie $T$ démontre les axiomes de $\mathsf Q$, puisque $\mathsf{PA}$ démontre $\mathrm Q_3$ (Récurrence dans PA). Les deux formules ont leurs variables libres parmi $v$. Si $T \vdash \varphi$, le point (i) de Deuxième condition (D2) donne $\vdash_{\mathsf{PA}} \mathrm{Pr}_T\,\ulcorner \varphi \urcorner$ et $\vdash_{\mathsf{PA}} (\exists y\, \delta)[\underline{\ulcorner \varphi \urcorner}/v]$, donc ces énoncés sont démontrables dans $T$ : c'est (D1). Le point (iv) du même nœud donne (D2) dans $T$, et (ii) donne (D3) dans $T$. Le point (i) de Löb et second théorème donne le théorème de Löb, et son point (ii), pour la formule $\mathrm{Pr}_T$, donne $T \nvdash \neg\mathrm{Pr}_T\,\ulcorner \bot \urcorner$, c'est-à-dire $T \nvdash \mathrm{Coh}(T)$, si $T$ est cohérente ; il en est de même pour $\exists y\, \delta$.