The Second Incompleteness Theorem

The first incompleteness theorem produced a true sentence a consistent recursive theory cannot prove. The second one turns the same argument on the theory's own consistency: a sufficiently strong recursively axiomatized theory cannot prove that it is consistent, unless it is not. The consistency statement is an ordinary arithmetic sentence, and the proof is the argument of the first theorem carried out inside the theory. Throughout, $T$ is a recursively axiomatizable theory given by a recursive axiom set $A$ (that is, $\#A$ is recursive), and $┌\sigma ┐=S^{\#\sigma }0$ names a Gödel number.¹

The provability predicate

From item 20 of the arithmetization, a sentence $\sigma$ is a theorem of $T$ iff some number codes a deduction of it,

The bracketed binary relation between $\#\sigma$ and $d$ is recursive; choose a formula $\pi (v_1,v_2)$ that numeralwise represents it in $A_E$. Existentially quantifying the proof gives a formula that expresses provability.

The construction uses the recursiveness of $A$, so the subscript is really the axiom set. The predicate reflects the theory's own proofs back into arithmetic.

Reflection is one-directional. Whenever the theory proves $\sigma$, it proves that it proves $\sigma$, but it does not prove the conditional $\sigma \to {\mathrm{Prb}}_T\sigma$. If $\sigma$ is true yet unprovable from $A_E$, then $\sigma \to {\mathrm{Prb}}_{A_E}\sigma$ is actually false in $\mathfrak{N}$.

The Gödel sentence, formalized

Apply the fixed-point lemma to $\neg {\mathrm{Prb}}_T$ to obtain a sentence asserting its own unprovability,

Half of the first incompleteness theorem is now a two-line consequence of reflection.

The proof of the unprovability of the Gödel sentence is short and uses only reflection. A short proof about $T$ might be reproducible inside $T$, if $T$ can formalize the steps

Carrying this out yields $T⊢\mathrm{Cons}T$ only when $T$ is inconsistent.

The derivability conditions

What the internalization needs is that $T$ prove the reflection and modus-ponens facts about its own provability predicate, not merely obey them in the metatheory.

Consistency itself is expressible. Take $0=S0$ as a fixed sentence refutable from $A_E$, and define

read as $T$ does not prove $0=S0$, that is, $T$ is consistent.

The second incompleteness theorem

Formalizing the unprovability of the Gödel sentence inside a sufficiently strong theory gives the key conditional: consistency would imply the Gödel sentence is unprovable.

An inconsistent theory proves everything, including its own (false) consistency statement; the theorem says this is the only way a sufficiently strong theory can prove its consistency.

Löb's theorem

The same formalized argument, with the fixed refutable sentence $0=S0$ replaced by an arbitrary $\tau$, gives a companion result. Build $\sigma$ to say if I am provable, then $\tau$.

Its formalization runs exactly as the formalized unprovability lemma: from $T⊢(\sigma \to ({\mathrm{Prb}}_T\sigma \to \tau ))$, reflection and two applications of formalized modus ponens give $T⊢({\mathrm{Prb}}_T\sigma \to {\mathrm{Prb}}_T\tau )$.

Since $T⊢\tau$ trivially yields $T⊢({\mathrm{Prb}}_T\tau \to \tau )$, Löb's theorem is the equivalence $T⊢({\mathrm{Prb}}_T\tau \to \tau )\iff T⊢\tau$: a theory proves "if I prove $\tau$ then $\tau$" only when it already proves $\tau$. Taking $\tau$ to be $0=S0$ recovers the second incompleteness theorem, since $\mathrm{Cons}T=\neg {\mathrm{Prb}}_T(0=S0)$ is exactly ${\mathrm{Prb}}_T(0=S0)\to 0=S0$ up to sentential logic.

Which theories are sufficiently strong

The finite subtheory $A_E$ is not sufficiently strong; conditions 2 and 3 require proving general facts about provability, which needs induction. Two theories that do satisfy all three are worth naming.

• Peano arithmetic (PA). The axioms of $A_E$ together with every induction axiom, the universal closure of $(\phi (0)\wedge \forall x(\phi (x)\to \phi (Sx)))\to \forall x\phi (x)$ for each formula $\phi$. Induction is what lets one prove commutativity of addition, and formalized reflection and modus ponens, inside the theory.
• Set theory (ST). The number-theoretic sentences provable in an axiomatic set theory such as Zermelo–Fraenkel, via the standard interpretation of arithmetic in sets.

PA is consistent because it is true in $\mathfrak{N}$; the second theorem then says PA cannot prove $\mathrm{Cons}(\text{PA})$. We know PA is consistent by an argument carried out in informal mathematics, or in set theory — so set theory has higher consistency strength, proving $\mathrm{Cons}(\text{PA})$ where PA cannot. But the grounds for believing set theory consistent are thinner: there is no evident "standard model of set theory" to point to, the way $\mathfrak{N}$ underwrites PA.

Set theory and Hilbert's program

Set theory gets a separate incompleteness argument because it yields the undecidability results for its own language. Arithmetic embeds in set theory: take $0=\varnothing$ and $n+1=n\cup \{n\}$, so each number is the set of smaller numbers, and let $\omega$ be the collection of these number-sets. Translating the symbols of $A_E$ into set-theoretic formulas — ${\pi }_{\forall }$ from "$v_1\in \omega$," ${\pi }_0$ from "$v_1=\varnothing$," ${\pi }_S$ from "$v_2=v_1\cup \{v_1\}$," and ${\pi }_{+},{\pi }_{\cdot },{\pi }_E$ from the recursion equations — gives an interpretation $\pi$ of $\text{Cn }{A}_E$ into ST. Verifying it makes seventeen demands on ST, each an everyday fact about $\omega$ (that $\varnothing$ is unique and lies in $\omega$, that addition is well defined by recursion on $\omega$, and so on), so a finite $\Delta \subseteq \mathrm{ST}$ already interprets $\text{Cn }{A}_E$.²

The proof transfers nonrecursiveness backward along the interpretation. The preimage ${\pi }^{-1}[\Theta ]$ of $\Theta =\text{Cn }(T\cup \Delta )$ is a consistent number-theoretic theory containing $A_E$, hence nonrecursive by strong undecidability of $\text{Cn }{A}_E$; and the translation $\sigma \mapsto \#({\sigma }^{\pi })$ is recursive, so $\Theta$ cannot be recursive without making its preimage recursive.³ Two consequences follow.

• Incompleteness of set theory. If set theory is consistent, it is not complete: its axioms are recursive, so completeness would make it recursive.
• Church's theorem, minimal vocabulary. In the language with equality and one two-place predicate symbol, the set of valid sentences is not recursive. This is Church's theorem at its sharpest lower bound on the vocabulary.

The whole development can itself be carried out inside ST, since essentially all of mathematics can. Then the informal implication if ST is consistent, then ${\sigma }^{\pi }$ is not a theorem of ST becomes a deduction within ST of a formal sentence $(\mathrm{Cons}(\mathrm{ST})\to {\sigma }^{\pi })$, where ${\sigma }^{\pi }$ is itself the set-theoretic sentence asserting its own unprovability.

This closes Hilbert's program in its original form. Before Gödel, one could hope to prove $\mathrm{Cons}(\mathrm{ST})$ from assumptions weaker than the axioms of set theory — ideally assumptions already known to be consistent, securing the foundations from below. The second theorem shows $\mathrm{Cons}(\mathrm{ST})$ is not provable in any subtheory of ST, so no such self-certification exists. A consistent, recursively axiomatized, sufficiently strong theory can neither decide every sentence in its language nor prove its own consistency. What remains is to add axioms, judged by whether they both strengthen the theory and match our informal understanding of the objects they describe.