We get today to Chapter 13, called ‘The Diagonalization Lemma, and Rosser’s Theorem’. Not that we actually prove Rosser’s theorem in detail, as this is fiddly. But I do establish the Lemma, show how it can be used to derive the syntactic version of the first theorem again, and I indicate the key construction for getting to Rosser’s theorem.

(Looking back at Chapter 12, though, I see that the section which actually proves the first theorem there had become rather oddly arranged: I’ve rearranged a bit, separating out the theorem from a couple of corollaries worth remarking. So I’ve included a revised Chapter 12 too.)

[*Link now removed*]

Rowsety MoidCh 13:

p 95, after the proof of Theorem 49, “see if you can work out why”.

Is it easy to say why? And does it matter that the fixed point is Π1? If so, I think you should just say, either here or in a footnote.

I think this is the first time there’s been a “see if you can work out”. Perhaps it’s not the first, but I can’t recall any other. It’s at least been quite rare. Yet this is the first chapter where I haven’t tried to follow all the proofs in detail. The density of formulas has sometimes been too great. We even diagonalised an α that was already a diagonalisation. So if anything I’d appreciate some help towards an intuitive understanding at about this point, rather than an exercise.

Perhaps that’s just me, or even just me today. Still, I think this is one of the points where there’s a level issue. A ways back in GWT, you weren’t even assuming the reader was familiar with mathematical induction.

Peter SmithI agree. A footnote is needed. That was me being lazy!

Rowsety MoidRe the revised Ch 12

p 89, proof of Theorem 40, “Given PA is ω-consistent” and “So given PA proves ¬G” —

Such use of “given” might be ok. However, to me “given” suggests something already established or accepted, rather than an assumption made in a proof. (Compare the two uses of “given” at the end of §12.1 on p 88.) Perhaps “if” would be better?

p 80, proof of Theorem 42, “But since G is unprovable” — unprovable in PA? Presumably not absolutely unprovable.

p 90, 1st par after Theorem 44 — “unless it stops ω-consistent” should be “unless it stops being ω-consistent”.

(This was something I also mentioned re the earlier version of Ch 12, though then the theorem was numbered 45 and was on p 91.)

p 91, bottom and top of p 92 — This paragraph is awkwardly worded (note the double ‘witch’ and the consequent use of long dashes), and without quite being told what Godel’s Theorem VI or VIII are, I’m not sure how helpful it is to be told they’re VI and VIII. Also, VIII is presumably later in the paper than VI, yet VI shows P has an undecidable sentence with its help? Then he generalises from VI alone.

I thought it might all make clear sense if I had Godel’s paper in front of me, but I’ve tried that (using more than one translation too), and I’m still not sure what VIII contributes to showing that P has an undecidable Π1 sentence. VIII also turns out to be after the generalisation, as well as after VI.

I also have doubts about the “Thus”. Still, here’s a stab at a fairly minimal rewording, with the “Thus” and VIII mention retained:

The part about VIII could be removed — or put in a footnote if you don’t want to say just Theorem VI.

Peter SmithTake the point about “given” — read instead “given our supposition”.

Agree that the para about Gödel and Theorem VI is awkward: I’ll simplify along the lines suggested.