Formule de démontrabilité et première condition de dérivabilité

(i) Par le point (iii) de Théorèmes r.e., $\mathrm{Th}(T)$ est récursivement énumérable. Le point (ii) de Forme Σ₁ des r.e., avec $n = 1$ et la variable $v$, et le renommage de sa preuve, qui permet de prendre $y$ pour variable quantifiée, fournissent la formule $\exists y\, \delta$.

(ii) Soit $\sigma$ un énoncé, de code $c$. La variable $v$ étant distincte de $y$, $\mathrm{Pr}\,\ulcorner \sigma \urcorner = \exists y\, \delta[\underline c/v]$, et $\delta[\underline c/v]$ est une formule Δ₀ par le point (i) de Σ₁-complétude, le chiffre $\underline c$ n'ayant pas de variable : $\mathrm{Pr}\,\ulcorner \sigma \urcorner$ est un énoncé Σ₁. Par le lemme de substitution et la définition de la satisfaction de $\exists$, il est vrai dans $\mathcal N$ si et seulement s'il existe $m$ tel que $\delta$ soit satisfaite sous une valuation qui vaut $c$ en $v$ et $m$ en $y$, c'est-à-dire si et seulement si $T \vdash \sigma$.

S'il est vrai, $\mathsf Q$ le démontre par le point (iii) de Σ₁-complétude. Réciproquement, si $\mathsf Q \vdash \mathrm{Pr}\,\ulcorner \sigma \urcorner$, cet énoncé est vrai dans $\mathcal N$, qui est un modèle de $\mathsf Q$ (preuve du point (iii) de Gödel-Rosser), par le théorème de correction. Si $T$ contient $\mathsf Q$, elle démontre tout ce que démontre $\mathsf Q$.

(iii) Par (ii), $\mathcal N \models \mathrm{Coh}_{\mathrm{Pr}}$ si et seulement si $T \nvdash \bot$. Si $T \vdash \bot$, comme $\vdash 0 = 0$ (Égalité démontrable, (i)), $T$ démontre une formule et sa négation ; si $T$ est incohérente, elle démontre toutes les formules (Cohérence, (i)), dont $\bot$.