So I was reading this article: https://www.scottaaronson.com/blog/?p=710 and I had an issue with the way he described Rosser's Theorem.
He starts by describing Gödel's Incompleteness Theorems, and mentioning that it doesn't actually prove that a system can't be both complete and consistent, but it does prove that a system can't be both complete and sound.
To quote:
This is the thing that, given a formal system F, constructs a sentence G(F) that’s a mathematical encoding of
“This sentence is not provable in F.”
If F proves G(F), then F proves both that F proves G(F) and that F doesn’t prove G(F), so F is inconsistent (and hence also unsound). Meanwhile, if F proves Not(G(F)), then it “believes” there’s a proof of G(F). So either that proof exists (in which case it would render F inconsistent, by the previous argument), or else it doesn’t exist (in which case F is unsound). The conclusion is that, assuming F is powerful enough to express sentences like G(F) in the first place, it can’t be both sound and complete (that is, it can’t prove all and only the true arithmetical statements).
This all makes perfect sense to me. By assuming $F$ is complete, either we show $F$ is inconsistent, or we show that $F$ can prove it has a proof that it actually doesn't, meaning it is unsound.
To contrast, he brings up Rosser's Theorem, which does show that a system can't be both complete and consistent.
To quote:
In Rosser’s proof, we replace G(F) by a new sentence R(F), which is a mathematical encoding of the following:
“For every proof of this sentence in F, there’s a shorter disproof.”
If F proves R(F), then it also proves that there’s a disproof of R(F) that’s shorter than the proof of R(F) whose existence we just assumed. So we can look for that disproof (since there are only finitely many strings of symbols to check), and either we’ll find it or we won’t—but in either case, we’ll have revealed F to be inconsistent. Meanwhile, if F proves Not(R(F)), then it proves that there is a proof of R(F) with no shorter disproof. So in particular, it proves that there’s a proof of R(F) that’s no longer than the proof of Not(R(F)) whose existence we just assumed. But once again, we can look for that proof (there are only finitely many strings to check), and either we’ll find it or we won’t, and in either case, F is revealed to be inconsistent.
But I have an issue with this. Take the first case. Say $F$ proves $R(F)$. Then that proves that there is a disproof of $R(F)$, specifically one that is shorter than the proof we used to prove $R(F)$. Since we were actually able to prove $R(F)$, the proof we used was finite. So we have a finite amount of symbols to check. So we can see whether or not there is a disproof of $R(F)$ that is shorter. If there is, then we've certainly shown that $F$ is not consistent, since there exists both a proof and a disproof for $R(F)$. However, in the case where there is no disproof for $R(F)$, how does that show $F$ is inconsistent? It definitely shows that $F$ is unsound, since we proved there is a disproof, but there isn't actually one.
But I feel like this is the exact same situation we had for Gödel's Theorem. We could show that there was a proof for something, but that proof might not actually exist, meaning our system is unsound. But in that case, we couldn't show that our system was inconsistent. So why can we show our system is inconsistent here? It doesn't feel like anything is different.
The point is that in this case, $F$ proves there is no shorter disproof of R(F) (since by assumption, $F$ has the requisite strength to examine the finite number of shorter proofs and establish that none are a disproof of the Rosser sentence). Thus it disproves the Rosser sentence, which says just the opposite of that. Therefore it is inconsistent, since the premise was that it proves the Rosser sentence.