This is a short post that offers a slightly different take on the standard proof of Löb's theorem. It offers nothing else of any value :)

We seek to prove the "inner" version, which we write as:

The proof uses quining to build a related sentence , the "Löb sentence", which talks about its own source code. By construction has the property:

Then, we can show that , i.e. they're equivalent! We do this by plugging into itself to get a twisty . We can then replace each with and prove Löb's theorem.

The proof

This proof uses the same rules of box manipulation as on the wiki page. We start by creating using quining, i.e. taking a modal fixed point:

  1. (exists as a modal fixed point)

Yep, this is skipping the details of the most interesting part, but alas I don't understand them well enough to do more than wave my hands and say "quining".

We then stick it inside the box to get our first property:

  1. (from (1) by necessitation)
  2. (from (2) by box-distributivity in both directions)

We now want to show that . We can get the forward direction by feeding a copy of into itself:

  1. (box-distributivity on (3))
  2. (internal necessitation)
  3. (from (4) and (5))

The backward direction is equivalent to , and is straightforward:

  1. (trivial)
  2. (necessitation and box-distributivity on (7))

Taking those together, we've shown and are equivalent.

  1. (from (6) and (8))

Now we'd like to finish by appealing to the following chain:

We've proven all but the last part of the chain. Here are the steps that let us do the substitution:

  1. (since and are equivalent by (9))
  2. (from (10) by necessitation)
  3. (from (11) by box-distributivity in both directions)

And that's everything we need:

  1. (from (3), (9), and (12))
New Comment