# 6

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