Non-définissabilité de la vérité

(i) Soit $\tau$ une telle formule. Le lemme diagonal, appliqué à $\neg\tau$, donne un énoncé $G$ tel que $T \vdash G \leftrightarrow \neg\tau(\underline{\ulcorner G \urcorner})$, puisque $(\neg\tau)[\underline{\ulcorner G \urcorner}/v] = \neg\,\tau(\underline{\ulcorner G \urcorner})$. Avec $T \vdash G \leftrightarrow \tau(\underline{\ulcorner G \urcorner})$, les instances $(P \leftrightarrow \neg R) \to ((P \leftrightarrow R) \to P)$ et $(P \leftrightarrow \neg R) \to ((P \leftrightarrow R) \to \neg P)$ donnent $T \vdash G$ et $T \vdash \neg G$ : $T$ serait incohérente.

(ii) Supposons l'ensemble $V$ de ces codes défini par une formule $\tau$ et la variable $v$, qui contient alors ses variables libres. Soit $\sigma$ un énoncé de code $c$. Par le lemme de substitution, $\mathcal N \models \tau(\underline c)$ si et seulement si $\tau$ est satisfaite sous une valuation qui vaut $c$ en $v$, c'est-à-dire si et seulement si $c \in V$, ou encore $\mathcal N \models \sigma$. Par la table de $\leftrightarrow$ (Connecteurs), $\mathcal N \models \sigma \leftrightarrow \tau(\underline c)$.

Soit $T$ l'ensemble des énoncés vrais dans $\mathcal N$. C'est une théorie cohérente, puisque $\mathcal N$ en est un modèle : par le théorème de correction, une formule et sa négation ne peuvent pas y être démontrées toutes deux. Elle contient $\mathsf Q$, dont les axiomes sont vrais dans $\mathcal N$ (preuve du point (iii) de Gödel-Rosser). Elle a pour éléments tous les énoncés $\sigma \leftrightarrow \tau(\underline{\ulcorner \sigma \urcorner})$, et les démontre donc, ce que (i) exclut.