# What was the exact form of Gödel's original Second Incompleteness Theorem?

Gödel's second incompleteness theorem is usually stated as:

Any consistent formal system $$F$$ capable of elementary arithmetic can't prove its own consistency.

I'm having trouble deducing this statement using just the pieces Gödel had available in 1931. As I understand it those were:

• Suppose $$G$$ is provable. Then this can be converted into a proof of $$\neg G$$. Hence, $$F$$ is inconsistent.

• Suppose $$\neg G$$ is provable. Then $$F$$ "believes" that $$G$$ can be proven. This doesn't necessarily have to be true. But at the very least $$F$$ is unsound.

The best I'm able to deduce from this is this:

Any sound formal system $$F$$ capable of elementary arithmetic can't prove its own consistency.

Take the contrapositive of the first of the previous deductions. Because consistency is a syntactic property this can be fully formalized in $$F$$ as "$$F$$ is consistent $$\implies$$ $$\neg G$$ is provable". Moreover, there really isn't anything stopping us from actually proving this theorem in $$F$$. But then, provided $$F$$ is sound, $$F$$ can't prove its own consistency. If it could, then using modus ponens it could prove $$\neg G$$. However, that would make $$F$$ unsound. $$\square$$

This is a decidedly weaker version of the second incompleteness theorem. And I don't see how to plug the hole without invoking Rosser's Theorem. Is this all that Gödel had in 1931?

• The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency. Dec 23, 2018 at 14:33
• @Peter This only shows "$F$ is inconsistent $\implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $\implies$ $F$ is inconsistent". Dec 23, 2018 at 14:41
• This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not\ G"$ cannot be both deduced. This leads to the contradiction you mentioned. Dec 23, 2018 at 14:45
• Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency. Dec 23, 2018 at 14:54
• @Peter I still don't see at what point you tightened the reasoning compared to my argument. Dec 23, 2018 at 15:02

The negation of "$$G$$ is provable" isn't "$$\neg G$$ is provable". It's "$$G$$ isn't provable" = $$G$$. The contrapositive of the first deduction is thus "$$F$$ is consistent $$\implies$$ $$G$$". Now suppose $$F$$ is consistent and can prove its own consistency. Then $$F$$ can prove $$G$$, rendering it inconsistent. ⚡