Gödel's incompleteness theorems

By the diagonal lemma (a formal cousin of Cantor's diagonal argument), arithmetic can construct a sentence $G_F$ satisfying $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ — a sentence asserting its own unprovability in $F$. If $F \vdash G_F$, then $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ holds, so $F \vdash \neg G_F$, contradicting consistency. Hence $F \nvdash G_F$ — which is exactly what $G_F$ claims, making $G_F$ true in $\mathbb{N}$. (Rosser later removed the $\omega$-consistency hypothesis.)

Step 1 (arithmetization of syntax). Fix a computable coding scheme assigning to every symbol, formula, and finite sequence of formulas of $F$'s language a unique natural number, its Gödel number. Because $F$ is effectively axiomatized, the relation $\mathrm{Prf}_F(p, n)$ — "$p$ is the code of a proof of the formula with code $n$" — is expressible by an arithmetic formula using only $+$, $\times$, and quantifiers, since checking a proof line by line is a finite mechanical procedure. Define $\mathrm{Prov}_F(n) := \exists p\, \mathrm{Prf}_F(p, n)$.

Step 2 (the diagonal lemma). For any arithmetic formula $\psi(x)$ with one free variable, the diagonal lemma produces a sentence $D$ such that $F \vdash D \leftrightarrow \psi(\ulcorner D \urcorner)$ — $D$ asserts of its own code that $\psi(x)$ holds of it. Apply this to $\psi(x) := \neg\mathrm{Prov}_F(x)$: we obtain a sentence $G_F$ with $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$. Informally, $G_F$ says "I am not provable in $F$."

Step 3 ($F \nvdash G_F$). Suppose toward contradiction that $F \vdash G_F$. Since $F$ is effectively axiomatized, this proof itself has a code $p_0$, so $\mathrm{Prf}_F(p_0, \ulcorner G_F \urcorner)$ is true, hence $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ (provable arithmetic facts about concrete numbers are themselves provable in $F$). But the diagonal equivalence together with $F \vdash G_F$ gives $F \vdash \neg \mathrm{Prov}_F(\ulcorner G_F \urcorner)$. So $F$ proves both a statement and its negation, contradicting consistency. Hence $F \nvdash G_F$.

Step 4 ($G_F$ is true, and — assuming $\omega$-consistency — $F \nvdash \neg G_F$). Since $F \nvdash G_F$, no number codes a proof of $G_F$, so $\neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$ holds in $\mathbb{N}$; by the diagonal equivalence this is exactly what $G_F$ asserts, so $G_F$ is true. If $F$ also proved the negation of $G_F$, i.e. $F \vdash \neg G_F$, then combining this with the diagonal equivalence would give $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ — "some $p$ codes a proof of $G_F$" — without that ever being witnessed by an actual proof, exactly the situation $\omega$-consistency rules out. So under $\omega$-consistency $F \nvdash \neg G_F$ as well, and $F$ is incomplete.

The proof of the first theorem — "if $F$ is consistent, then $F$ does not prove $G_F$" — can itself be formalized inside $F$, yielding $F \vdash \mathrm{Con}(F) \to G_F$. If $F$ could prove $\mathrm{Con}(F)$, modus ponens would give $F \vdash G_F$, contradicting the first theorem.

Step 1 (the provability predicate is formalizable, not just definable). Because $\mathrm{Prov}_F$ is built from the mechanical, checkable relation $\mathrm{Prf}_F(p,n)$, three "derivability conditions" are themselves provable inside $F$ (this is where the argument needs $F$ to extend Peano arithmetic, not just be consistent): ($P_1$) if $F$ proves $\varphi$ then $F$ proves $\mathrm{Prov}_F(\ulcorner\varphi\urcorner)$; ($P_2$) $F$ proves $\mathrm{Prov}_F(\ulcorner\varphi\to\psi\urcorner) \to (\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_F(\ulcorner\psi\urcorner))$; ($P_3$) $F$ proves $\mathrm{Prov}_F(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_F(\ulcorner\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\urcorner)$.

Step 2 (formalizing Theorem 1's own argument). By the diagonal equivalence, $F \vdash \neg G_F \to \mathrm{Prov}_F(\ulcorner G_F \urcorner)$. The informal argument of Theorem 1 — "if $G_F$ were provable, its own proof would witness $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$, and the diagonal equivalence would then hand us a proof of $\neg G_F$ too" — uses nothing beyond mechanical symbol manipulation covered by ($P_1$)–($P_3$), so it can be mirrored step by step as a formal deduction inside $F$ itself, yielding $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \mathrm{Prov}_F(\ulcorner \neg G_F \urcorner)$. Since proving both $G_F$ and its negation lets $F$ derive $0 = 1$ by ex falso quodlibet, this gives $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \neg\mathrm{Con}(F)$, i.e. $F \vdash \mathrm{Con}(F) \to G_F$.

Step 3 (conclusion). Suppose toward contradiction that $F \vdash \mathrm{Con}(F)$. Combined with $F \vdash \mathrm{Con}(F) \to G_F$ via modus ponens, $F$ would prove $G_F$. But Theorem 1 already showed $F \nvdash G_F$ for consistent $F$ — a contradiction. Hence $F$ cannot prove $\mathrm{Con}(F)$, exactly as claimed.

Proved by Gödel in 1929 (his doctoral thesis), this says the inference rules of first-order logic are complete: they miss no logical consequence. Incompleteness (1931) does not contradict this: $G_F$ is unprovable because $F$ has non-standard models in which $G_F$ is false, even though $G_F$ is true in the intended model $\mathbb{N}$.

Step 1 (soundness — the easy direction, $T \vdash \varphi$ implies $T \models \varphi$). Argue by induction on the length of a formal proof of $\varphi$ from $T$. Every axiom of $T$ is true in any model $M$ of $T$ by definition; every purely logical axiom (e.g. $\varphi \to (\psi \to \varphi)$) is valid, true under every interpretation whatsoever. And each inference rule preserves truth in $M$: for modus ponens, if $M \models \theta$ and $M \models \theta \to \varphi$ then automatically $M \models \varphi$. So every line of the proof is true in $M$, and in particular the last line, $\varphi$, is; since $M$ was an arbitrary model of $T$, $T \models \varphi$.

Step 2 (completeness — the hard direction, by contraposition: $T \nvdash \varphi$ implies $T \not\models \varphi$). Suppose $T \nvdash \varphi$. Then the set $T \cup \{\neg\varphi\}$ is consistent (if it proved a contradiction, $T$ would prove $\varphi$ by reductio). Using Henkin's method, extend it to a maximal consistent set $\Sigma$ with witnesses: whenever $\exists x\, \psi(x)$ is in $\Sigma$, some constant $c$ is added with $\psi(c)$ also in $\Sigma$. Build the term model $M_\Sigma$ whose elements are closed terms of the extended language identified up to provable equality in $\Sigma$, with relations and functions interpreted directly from $\Sigma$. A term-length induction (the "truth lemma") then shows $M_\Sigma \models \theta \iff \theta \in \Sigma$ for every sentence $\theta$.

Step 3 (assembling the model, and conclusion). Since $\neg\varphi \in \Sigma$, the truth lemma gives $M_\Sigma \models \neg\varphi$, and since every axiom of $T$ lies in $\Sigma$, also $M_\Sigma \models T$. So $M_\Sigma$ is an actual model of $T$ in which $\varphi$ fails, i.e. $T \not\models \varphi$. This proves the contrapositive of Step 2, and combined with Step 1, $T \vdash \varphi$ exactly when $T \models \varphi$ — this is Gödel's 1929 doctoral thesis result, later streamlined by Leon Henkin (1949) into the term-model construction used here.

Suppose $H(P, x)$ decided halting. Build a machine $D(P)$ that runs $H(P, P)$ and then loops forever if $H$ says "halts", and halts if $H$ says "loops". Feeding $D$ its own code: $D(D)$ halts iff $H(D, D)$ says it loops — a contradiction. This is the exact computational twin of Gödel's diagonal sentence.

Step 1 (assume a halting decider exists). Suppose toward contradiction that there is an algorithm $H$ such that $H(P, x)$ always terminates and correctly outputs "halts" if the program with code $P$ halts on input $x$, and "loops" otherwise.

Step 2 (build a diagonal machine from $H$). Define a new algorithm $D(P)$ that, on input a program code $P$, first computes $H(P, P)$ — running $H$ with $P$ fed in as both the program and the input. If $H(P, P)$ says "halts", then $D$ deliberately enters an infinite loop; if $H(P, P)$ says "loops", then $D$ halts immediately (say, by returning $0$).

Step 3 (feed $D$ its own code). Since $D$ is itself an algorithm, it has a code, and nothing stops us from running $D$ on that very code: consider $D(D)$. Two cases, both impossible: if $D(D)$ halts, then by construction this happens exactly when $H(D, D)$ said "loops" — meaning $H$ incorrectly reported that $D$ on $D$ does not halt, even though it just did. If instead $D(D)$ runs forever, this happens exactly when $H(D, D)$ said "halts" — meaning $H$ incorrectly reported that it halts, even though it loops forever.

Step 4 (conclusion). Either way $H$ gives a wrong answer on the input $(D, D)$, contradicting the assumption that $H$ is always correct. So no such algorithm $H$ can exist: the halting problem is undecidable.