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 ┐)$.

A fixed point of the negated arithmetic provability predicate for a computably enumerable arithmetic theory $T$. Consistency excludes a proof of $G$, because a genuine proof is arithmetically verifiable and contradicts the fixed-point assertion. Omega-consistency excludes a proof of its negation. For a consistent theory extending Robinson arithmetic, this sentence is true in the standard natural numbers.

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.

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.