Friday, June 26, 2009

Rosser's Theorem

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!!!


Richard Zach said...

I'm missing something obvious I'm sure. Isn't RProv a Sigma_1 predicate (there is a g.n. x of a proof such that for every g.n. y < x ....)? And so a fixed point R of ~RProv is provably equivalent to a Pi_1 sentence (viz., ~RProv('R')). And if R is undecidable so is ~RProv('R').

Robbie Williams said...

"do please me know if you spot errors"?

Peter Smith said...

Duh! Thanks Robbie!

Richard: RProv(x) is usually defined as (Ev)(Prf(v,x) & (Aw < v)not-Prf(w, not(x))), where as things are typically set up, e.g. as in my book, Prf is already Sigma_1. So there's a negated Sigma_1 wff buried inside RProv(x), and so the whole thing isn't [or at least, isn't trivially] Sigma_1. No??

Aatu Koskensilta said...

"x is a proof of y" is not only Sigma-1 but also primitive recursive, so Rprov(y) = (Ex)(x is a proof of y & (z < x)(z is not a proof of y)) is Sigma-1, given that the class of primitive recursive predicates is closed under bounded quantification. Spelling out the details depends of course on how exactly one sets up things...

Peter Smith said...

Sure Aatu. We know that the property "x numbers a proof of y and no number less than x numbers a proof of the negation of y" is p.r., so there will be some quantifiers-at-the-front Sigma_1 wff RPrf*(x, y) that represents that. Quantify that, and we get a new Sigma_1 predicate RProv*(v) = (Ev)RPrf*(v, x).

So sure, we know that the Rosserized property has a Sigma_1 wff that expresses it. But now we don't know yet how a proof will go that a fixed point for RProv*(x) is undecidable, do we? I mean, we won't get that result out of the usual proof that fixed points for the usual RProv(x) are undecidable, for that relies on the way that RProv is built up from two occurrences of Prf. (But that way of building up on the face of it gives us something Sigma_2 since one occurrence is negated, so isn't RProv*.)

So we still need to do something more to do. Either a new proof that RProv* has undecidable fixed point(???), or a proof that RProv can be massaged into RProv*(???), or -- simplest! -- the sort of thing I do in the new version.