Gödel's incompleteness theorems

Remarks

Proof idea for 1: by the diagonal lemma there is a sentence $G$ with $T \vdash G \leftrightarrow \neg \mathrm{Prov}_T(\ulcorner G \urcorner)$. If $T \vdash G$, then $T \vdash \mathrm{Prov}_T(\ulcorner G \urcorner)$, and $T$ is inconsistent. Gödel's argument that $T \nvdash \neg G$ used $\omega$-consistency; Rosser's variant of the sentence needs only consistency, which gives the form stated here. Proof idea for 2: the argument for "if $T$ is consistent then $T \nvdash G$" can be carried out inside $T$, so $T \vdash \mathrm{Con}(T) \to G$; thus $T \vdash \mathrm{Con}(T)$ would give $T \vdash G$.

The hypotheses matter. The theory of the true sentences of $\N$ is complete and consistent, but its axioms are not computably enumerable. Presburger arithmetic, with addition but no multiplication, is consistent, computably axiomatized and complete.

Going deeper

For a student

The proofs turn statements about proofs into statements about numbers by a Gödel numbering, and then use the diagonal lemma to build a self-referential sentence. The first theorem implies that every consistent computably axiomatized extension of $\mathsf{Q}$ is incomplete, and with more work that such theories are undecidable. The second theorem ended the hope of Hilbert's program to prove the consistency of mathematics by finitary means within mathematics itself. Concrete true statements unprovable in $\mathsf{PA}$ include Goodstein's theorem and the Paris–Harrington theorem.