Wolfgang Rautenberg’s very nice A Concise Introduction to Mathematical Logic states Gödel’s first theorem in the usual sort of way. Roughly: given a suitably axiomatized omega-consistent theory T containing enough arithmetic, there’s a Pi_1 undecidable sentence. He proves this by appeal to the diagonalization lemma applied to the predicate not-Prov (where Prov suitably expresses provability in T). A fixed point G for this is neither provable nor disprovable. And being equivalent to not-Prov(‘G’) that’s undecidable too. But not-Prov by construction is Pi_1, so that gives us a Pi_1 undecidable sentence.
So far, so very familiar! He then goes on to say (p. 195) that the assumption of omega-consistency in Gödel’s theorem can be weakened to that of consistency. And he gives the usual Rosser construction. Define a Rosser proof-predicate RProv (defined from the usual Sigma_1 proof-relation Prf, so it is satisfied by the Gödel number for a wff if the wff has a proof, and there is no “smaller” proof of its negation). Then, just on the assumption of consistency, a fixed point R for not-RProv is neither provable nor disprovable. Great.
But oops, that isn’t quite enough to prove the weakening of Gödel’s theorem as stated. For Rautenberg hasn’t checked that there’s a Pi_1 undecidable sentence that you can get in this way. And note that not-RProv (as he defines it from the Sigma_1 Prf) isn’t explicitly Pi_1, so the argument from before doesn’t carry over. So there’s a gap in the proof here: some more work needs to be done.
There’s the same gap it seems in Per Lindström’s Aspects of Incompleteness (p. 26). He just cheerfully starts off, in effect, “Let R be a Pi_1 fixed point of not-RProv.” Why should there be one? He doesn’t explain.
At least one book, though, does worse. That is to say, it notes the need for an argument that there is a Pi_1 undecidable sentence that you can get from Rosser’s kind of construction. But then it proceeds to give a bad argument, claiming not-RProv can be manipulated into an equivalent Pi_1 formula, but giving an evidently hopeless “proof” for that claim. Oh dear.
And the culprit was me. So I’m very grateful to Adil Sanaulla for alerting me to the fact that something is badly amiss in An Introduction to Gödel’s Theorems at the foot of p. 178. So I’ve needed to go back to the drawing board.
In fact, sorting out things out took just a bit of thought. To recap, the sort of argument that I use in the book (and that e.g. Rautenberg uses) to get an undecidable sentence just assuming consistency relies on proving that a fixed point for not-RProv is undecidable. But that doesn’t immediately give us the result that there’s a Pi_1 undecidable sentence. On the other hand, e.g. Raymond Smullyan in Chap. VI of his wonderful Gödel’s Incompleteness Theorems uses a slightly different construction that does get us a Pi_1 undecidable sentence: it is perhaps closer to Rosser’s original, but it doesn’t use the now standard Rosserized proof predicate. The two arguments are evidently very closely related, however. But exactly how?
Well, this is hardly a deep expository problem! But I confess it did take me a while, after a false start, to make the obvious connection. The result is here: an updated section for the book (which will appear in the next revised printing). It still gives much the same original version which shows that a fixed point for not-RProv is undecidable, and then I hope smoothly segues into showing how to give what is in essence the original Rosser/Smullyan version that yields a Pi_1 undecidable sentence. Obvious when you see how, and I kick myself that this wasn’t in the previous printings of the book.
Do please let me know if you still spot some errors!!!