Today’s chapter is optimistically entitled ‘Proving the Second Incompleteness Theorem’. Of course we don’t actually do that! But we do say something more about what it takes to prove it (stating the so-called derivability conditions, and saying what it takes to prove them).
As an extra, we say how it can be that there are consistent theories which ‘prove’ their own inconsistency.
[Link now removed]
I apologize for not having read along (life with surrounding pandemic, and other complications, proves (or is it demonstrates?) time-consuming in weird spasms) until now. But, as you know, the Second always catches my eye. So, this comment:
you say “This is perhaps a bit naughty, as the new notation hides away some Gödel-numbering.” It also hides away some *numeraling*. I don’t know if you earlier made an appropriately fussy remark about the range of the ⌜ ⌝ mapping, but it becomes relevant in the context of Second. Seems worth a remark, en passant, about the additional naughtiness.
I’ll cut down on the scare-quoted ‘knows’ (T “knows” p just mean T can prove p). The box does is not being read as knows, it is being read as “is provable (in T)” — thought that was clear from the definition but I’ll make it explicit.
I only mention “fixed points” to introduce standard jargon in the context. I wouldn’t want to rest anything on that. It isn’t supposed to be especially enlightening!
A nice chapter.
p 116: What does ‘knows’ in the explanation of Defn 58 amount to, though, and how is □ being read?
Most of the time, it looks like □ is being read as ‘knows’; not in footnote 2, though, or in the explanation of (3) where ‘it can code up’ re-enters the picture. When coding up was mentioned for (1), it seemed to be about getting from something without the □ to something with; it’s not clear how that fits with what’s said for (3).
p 119, “Con (like G) is also a fixed point” — I think it would be helpful to have something somewhere in GWT (not necessarily in this chapter) that would give the reader a more intuitive feel for fixed points.
I’ve found in other contexts in the past that when told, or shown, that something was a fixed point, some people seemed to find that enlightening in itself. It helped them to see … something. It hasn’t worked that way for me, though, and I don’t think I’m alone there.