Diagonal lemma

For every one-variable arithmetical formula $\theta (x)$, a sufficiently strong theory of arithmetic has a sentence $\gamma$ satisfying $\gamma \leftrightarrow \theta (┌\gamma ┐)$.

For a computably enumerable first-order theory $T$ extending Robinson arithmetic, choose the standard arithmetic arithmetical provability predicate ${\mathrm{Prov}}_T$. The diagonal lemma, carried out in the weak base theory, gives a sentence $G$ withIf $T$ is consistent, $T$ cannot prove $G$: an actual finite proof would be verifiable in the weak base, so $T$ would prove both its provability and its unprovability. There is therefore no actual proof of $G$, and the displayed equivalence, true in the standard natural numbers, shows that this canonical $G$ is true there.

If $T$ is omega-consistent, it cannot prove $\neg G$ either. Such a proof would imply the existence of a proof code for $G$, while each standard numeral can be individually verified not to be such a code. Ordinary consistency suffices for unprovability of $G$; the original argument for unprovability of its negation uses the stronger hypothesis. Requiring the fixed-point equivalence in a sound weak base is important: an arbitrary equivalence provable only in an unsound extension need not yield a true sentence.

Assuming PA is consistent, the theory $S=\mathrm{PA}+\neg {\mathrm{Con}}_{\mathrm{PA}}$ is consistent by second incompleteness. Its false axiom $G=\neg {\mathrm{Con}}_{\mathrm{PA}}$ is provable, so the standard semantic biconditional $G\leftrightarrow \neg {\mathrm{Pr}}_S(┌G┐)$ is true with both sides false. Thus a true biconditional alone does not make an arbitrary sentence a true canonical Gödel sentence. A canonical Pi-1 construction adds the necessary syntactic or sound-base information. Truth, internal equivalence and canonical construction must be distinguished.

For a Gödel sentence $G\leftrightarrow \neg \square G$ with the Hilbert-Bernays-Löb derivability conditions, fix a refutable contradiction sentence $\perp$. Since $\perp \to G$ is provable, $\square \perp \to \square G$, giving $G\to \neg \square \perp$. For the reverse direction, $\square G$ implies both $\square \square G$ and $\square \neg \square G$, hence $\square \perp$. Contraposition gives $\neg \square \perp \to \neg \square G\to G$. This is an internal equivalence of sentences, not a rule asserting the theory's own consistency.

This diagonal sentence says that any proof of itself has a no-later proof of its negation. A proof of $R$ contradicts finite verification that no earlier opposite proof exists. A proof of its negation, together with finite verification that no earlier proof of $R$ exists, proves the displayed universal condition and hence $R$. Thus consistency alone excludes both proofs, strengthening the original omega-consistency form of incompleteness.

For disjoint sets numeralwise enumerated by $P,R$, finite-initial-segment and total-comparison axioms let $H$ separate the first set from the second in the theory. For a member of the first set use a positive $P$ stage and finitely many refutations of $R$. For a member of the second set use its positive $R$ stage: earlier proposed $P$ stages are all refuted by a finite bounded proof, while later stages lose to that known $R$ witness. This proves a separator without inferring arbitrary negative facts from the mere Sigma-1 form of the enumerators.

For the standard Gödel sentence and Rosser sentence, the formalized Rosser unprovability theorem and $G\leftrightarrow \mathrm{Con}(T)$ yield $T⊢G\to R$. If $T+\mathrm{Con}(T)$ is consistent, the converse is unprovable under the usual formalized incompleteness hypotheses. A proof of $R\to G$ would give $\square \neg G\to \square \neg R$. Formalized negative unprovability identifies $\neg \square \neg R$ with $\mathrm{Con}(T)$ and $\neg \square \neg G$ with $\mathrm{Con}(T+\mathrm{Con}(T))$. The strengthened theory would then prove its own consistency, contradicting the Gödel second incompleteness theorem. The consistency assumption belongs to this strictness conclusion.

The diagonal lemma can be carried out uniformly: from a one-variable formula code, compute a sentence code whose assertion is equivalent to the original formula applied to that sentence code. The effective substitution operation is what turns a semantic diagonal argument into a productive function.

Every consistent recursively axiomatized extension of elementary arithmetic is incomplete. If it were complete, its theorem set would be decidable; representing that decision procedure and diagonalizing against it yields a contradiction.