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?

  • 2
    $\begingroup$ The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency. $\endgroup$
    – Peter
    Dec 23, 2018 at 14:33
  • $\begingroup$ @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". $\endgroup$ Dec 23, 2018 at 14:41
  • $\begingroup$ 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. $\endgroup$
    – Peter
    Dec 23, 2018 at 14:45
  • $\begingroup$ Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency. $\endgroup$
    – Peter
    Dec 23, 2018 at 14:54
  • $\begingroup$ @Peter I still don't see at what point you tightened the reasoning compared to my argument. $\endgroup$ Dec 23, 2018 at 15:02

1 Answer 1


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

And all is well.

  • $\begingroup$ I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid. $\endgroup$ Dec 23, 2018 at 16:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.