If that’s how it works, it doesn’t lead to a simplified cartoon guide for readers who’ll notice missing steps or circular premises; they’d have to first walk through Lob’s Theorem in order to follow this “simplified” proof of Lob’s Theorem.
Yes to Alex that (I think) you can use an already-in-hand proof of Löb to make the self-referential proof work, and
Yes to Eliezer that that would be cheating wouldn’t actually ground out all of the intuitions, because then the “santa clause”-like sentence is still in use in already-in-hand proof of Löb.
(I’ll write a separate comment on Eliezer’s original question.)
If that’s how it works, it doesn’t lead to a simplified cartoon guide for readers who’ll notice missing steps or circular premises; they’d have to first walk through Lob’s Theorem in order to follow this “simplified” proof of Lob’s Theorem.
Yes to both of you on these points:
Yes to Alex that (I think) you can use an already-in-hand proof of Löb to make the self-referential proof work, and
Yes to Eliezer that that would be cheating wouldn’t actually ground out all of the intuitions, because then the “santa clause”-like sentence is still in use in already-in-hand proof of Löb.
(I’ll write a separate comment on Eliezer’s original question.)