[FOM] Kreisel, Löb, and G2

[Craig Smorynski]

Aatu Koskensilta quoted me on the issue of who first realised that Löb's Theorem for a theory T is equivalent to the Second Incompleteness Theorem for all finite extensions of T to the effect that I side with Boolos in crediting Kripke. That is not quite true:

I accidentally rediscovered the proof at the conference in Kiel in 1974(?) and asked around. Dana Scott told me it was old and had been discovered by Kreisel a couple of decades earlier. That would be right about the time give or take a couple of years of Löb's paper. When I wrote to Kreisel to ask about the proofs provenance, he denied ever having seen it. Perhaps Scott meant Kripke, not Kreisel. In any event, there was Boolos's crediting Kripke, which I wrote to him about, feeling it smacked more of hero-worship than scholarship. As usual I stated things poorly and Kripke got upset and informed me of his 1967 discovery. This is the earliest discovery of the proof that I am aware of. This does not mean that I side with Boolos; I take an agnostic stand. It is quite possible that someone, perhaps a later forgetful Kreisel, discovered it in the 1950s.

Certainly half of the equivalence, that Löb's Theorem implies the Second Incompleteness Theorem, was stated frequently by Kreisel.

I fear my statement was more suggestive than I intended.
Craig



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20120517/8ce35293/attachment.html>