2
$\begingroup$

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?

$\endgroup$
7
  • 2
    $\begingroup$ The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency. $\endgroup$
    – Peter
    Commented 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$
    – Sebastian Oberhoff
    Commented 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
    Commented Dec 23, 2018 at 14:45
  • $\begingroup$ Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency. $\endgroup$
    – Peter
    Commented 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$
    – Sebastian Oberhoff
    Commented Dec 23, 2018 at 15:02

1 Answer 1

Reset to default
2
$\begingroup$

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.

$\endgroup$
1
  • $\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$
    – Noah Schweber
    Commented Dec 23, 2018 at 16:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .