La vérité arithmétique n'est pas récursivement énumérable

(i) Par le point (iii) de Définissabilité, l'ensemble $K$ de l'arrêt est défini par une formule $\varphi_K$ dont la seule variable libre est $v$. Pour $n \in {\mathbb N}$, considérons l'énoncé $$\sigma_n = \forall v\, \big(v = \underline n \to \neg\varphi_K\big),$$ c'est-à-dire, en notation préfixée, le mot $\forall\, v \to {=}\, v\, \underline n\ \neg\, \varphi_K$.

Par la définition de la satisfaction et le lemme de coïncidence, $\mathcal N \models \sigma_n$ si et seulement si $\mathcal N \not\models \varphi_K\,[v \mapsto n]$, c'est-à-dire $n \notin K$.

Le code de $\sigma_n$ est $$\begin{aligned} g(n) = \mathrm{conc}\Big(&\mathrm{conc}\big(\ulcorner \forall v \to {=}\, v \urcorner, \ulcorner \underline n \urcorner\big), \\ &\ulcorner \neg\varphi_K \urcorner\Big), \end{aligned}$$ où le premier et le dernier codes sont fixes, et $\ulcorner \underline n \urcorner$ se calcule par récurrence primitive : $\ulcorner \underline 0 \urcorner = \langle 4 \rangle$ et $\ulcorner \underline{n + 1} \urcorner = \mathrm{conc}(\langle 5 \rangle, \ulcorner \underline n \urcorner)$. La fonction $g$ est primitive récursive (Codages).

Si l'ensemble $V$ des codes des énoncés vrais était récursivement énumérable, $\mathbb N \setminus K = g^{-1}(V)$ le serait aussi (Récursif, r.e., (iii)), contrairement au point (iii) de l'indécidabilité de l'arrêt.

(ii) Comme $\mathcal N$ est un modèle de $T$, le théorème de correction montre que tout énoncé démontrable dans $T$ est vrai dans $\mathcal N$. Si $T$ démontrait tous les énoncés vrais dans $\mathcal N$, l'ensemble $V$ serait celui des codes des énoncés démontrables dans $T$, récursivement énumérable par le point (iii) de Théorèmes r.e., ce que (i) exclut.

Il existe donc un énoncé $\sigma$ vrai dans $\mathcal N$ tel que $T \nvdash \sigma$. L'énoncé $\neg\sigma$ est faux dans $\mathcal N$ ; il n'est donc pas démontrable non plus.

(iii) Les axiomes de $\mathsf{PA}$ sont vrais dans $\mathcal N$. Les six premiers sont les axiomes de Peano et les égalités qui définissent les opérations. Pour un axiome de récurrence et une valuation $s$, l'ensemble des $n$ tels que $\mathcal N \models \varphi\,[s(x \mid n)]$ contient $0$ et est stable par successeur, par le lemme de substitution ; c'est donc $\mathbb N$ tout entier (Récurrence). On applique (ii).