# Explanation of proof of Gödel's Second Incompleteness Theorem

I am looking for a simple explanation/outline of the proof of Gödel's Second Incompleteness Theorem, and I haven't yet been able to find anything that is within my grasp. I'm looking for something like: Kenny's Overview of Hofstadter's Explanation of Gödel's Theorem (for his first theorem) - i.e., not very mathematically rigorous, just giving an overview of the main ideas and the thought process behind the proof.

To me, it seems that the (main ideas of the) proof could be made quite simple:

1.) Gödel's first incompleteness theorem proves that "Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250)." (wikipedia).

2.) The proof works by asserting that in any "effectively generated theory capable of expressing elementary arithmetic", it is possible to formulate a "Gödel statement" which essential says: "This statement is not provable"; this must be a true statement, for if it were false, then it could be proven, and that would lead to contradictions. So we have a true statement which is not provable within the theory. QED.

3.) Now, IF we were able to prove the "Gödel statement", our theory would be inconsistent. Thus, a statement which asserts the consistency of our theory must prove/imply that we CANNOT prove the Gödel statement, or, in other words, it must prove the statement that the Gödel statement is not provable.

4.) BUT - the statement: "The Gödel statement is not provable" IS the Gödel statement. So, in proving its own consistency, a theory must prove the Gödel statement, implying that it is inconsistent.

Nothing that I have read has been anywhere near this simple. What am I missing? Is it really much more complicated that what I have put here?

DISCLAIMER: I am not a mathematician, and I haven't had much in the way of formal mathematics instruction. I am just an interested layperson.

The tricky bit is in step 3, and the distinction between "prove" and "imply". Let $T$ be our theory, and Con($T$) be the statement that $T$ is consistent. It is true that Con($T$) implies that we cannot prove the Gödel statement $G$. This does not immediately imply that the statement "Con($T$) implies $G$ is not provable in T" is provable in $T$. The point of the Second Incompleteness Theorem is to show that that statement is indeed provable in $T$.
Gödel's second incompleteness theorem states that any effectively generated theory $T$ capable of interpreting Peano arithmetic proves its own consistency if and only if $T$ is inconsistent. To be precise, when we say $T$ proves its own consistency, what we mean is that $T$ proves that there is no number $n$ which codes a proof of a contradiction from the axioms of $T$. Let us call this statement $\textrm{Con}(T)$ for short.
If $T$ is inconsistent, then $T$ proves any statement whatsoever, since ex falso quodlibet. So in particular, $T$ proves $\textrm{Con}(T)$. So this proves the easy half of the theorem. Now for the hard half. Let us write $\textrm{Prov}(\varphi)$ for the statement, ‘There is a number $n$ which codes the proof of the formula $\varphi$ from the axioms of $T$’. Löb's theorem shows that this provability predicate has the following property: if $T$ proves that $\textrm{Prov}(\varphi)$ implies $\varphi$, then $T$ proves $\varphi$; in symbols, $$T \vdash \textrm{Prov}(\varphi) \to \varphi \text{ implies } T \vdash \varphi$$ Let $\bot$ be an arbitrary contradiction. By definition, $\textrm{Con}(T)$ is equivalent to $\textrm{Prov}(\bot) \to \bot$, that is, if a contradiction is provable, then we have a contradiction. Therefore, by Löb's theorem, if $T$ proves $\textrm{Con}(T)$, then $T$ proves $\bot$, and therefore $T$ is inconsistent. This completes the proof of Gödel's second incompleteness theorem.
• This proof doesn't work as you've written it: it is not enough to observe that $Con(T)$ is equivalent to ${Prov}(\perp)\rightarrow \perp$. You must demonstrate at least that $T$ PROVES that $Con(T)\rightarrow (\mbox{Prov}(\perp)\rightarrow \perp)$ (call this $(\star)$). To avoid doing that work you could of course replace your current definition of $Con(T)$ with the universal "for all $n$ if $n$ codes a sentence and $Prov(n)$ then $n$". Then $T$ clearly proves $(\star)$ by instantiation of $\forall$, so your proof works but not with the usual definition of $Con(T)$. Jul 21, 2013 at 15:37