Armlängen

Löb’s Theorem

A lesser known elementary theorem in basic proof theory is Löb’s Theorem. Even though I know it and know the basic idea of a proof for it, I cannot remember where I know this from, in the logic lectures I took it wasnt mentioned iirc, and in the introducting books I have read I cant remember it, too. And actually, I never needed it so far for anything, so I forgot about it.

The Löb Theorem basically states: If PA⊧ (^⌈PA⊧A^⌉→A) then PA⊧A.

Well, in the comments of this Blogpost I found a nice illustration of the proof.

Which reminds me of an old xkcd-comic.