Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: A proof of inner Löb's theorem, published by James Payor on February 21, 2023 on The AI Alignment Forum.

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: □P↔□(□PP)

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

Then, we can show that □L↔□P, i.e. they're equivalent! We do this by plugging □L into itself to get a twisty □P. We can then replace each □L with □P 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 L using quining, i.e. taking a modal fixed point:

⊢L↔(□LP) (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:

⊢□(L↔(□LP)) (from (1) by necessitation)

⊢□L↔□(□LP) (from (2) by box-distributivity in both directions)

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

⊢□L(□□L□P) (box-distributivity on (3))

⊢□L□□L (internal necessitation)

⊢□L□P (from (4) and (5))

The backward direction is equivalent to □P□(□LP), and is straightforward:

⊢P(□LP) (trivial)

⊢□P□(□LP) (necessitation and box-distributivity on (7))

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

⊢□L↔□P (from (6) and (8))

Now we'd like to finish by appealing to the following chain: □P↔□L↔□(□LP)↔□(□PP)

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

⊢(□LP)↔(□PP) (since □L and □P are equivalent by (9))

⊢□((□LP)↔(□PP)) (from (10) by necessitation)

⊢□(□LP)↔□(□PP) (from (11) by box-distributivity in both directions)

And that's everything we need:

⊢□P↔□(□PP) (from (3), (9), and (12))

Thanks for listening. To help us out with The Nonlinear Library or to learn more, please visit nonlinear.org.