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?