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

Question

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.

Answer 1

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

Answer 2

There's actually a pretty simple statement of how the proof of G2 goes. Basically, the point is that the proof of G1 can itself be formalized in Peano Arithmetic (say). If you look at the proof itself, it's pretty easy to convince yourself that this is true. The reasoning is quite elementary. It uses induction, but nothing more powerful than that.

Actually, all you really need here is half of the proof of G1: The part where you prove that, if T is consistent, then T does not prove G (the Goedel sentence). When you formalize this, you get a proof, in T, of: $$Con(T) \to G$$ And then you reason (outside T!) as follows: We already know that T does not prove G (if it is consistent). But if it prove Con(T), then it would prove G, by modus ponens. So it can't prove Con(T).

This, by the way, is basically all that Goedel himself says about the matter in the 1931 paper. It seems everyone just said, "Yeah, pretty clearly", so he never published the sequel.

That said, there are details that are not trivial to get right. The hard part is the formalization of the proof of $\Sigma_1$ completeness (which yields the third derivability condition).

Let me also add that it's now known that we can formalize this proof in very weak systems, so nothing so strong as PA is needed.

Answer 3

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.

Here is a slightly different proof of the theorem, which does not make overt use of the Gödel sentence.

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.