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: $$\square P\leftrightarrow \square (\square P\to P)$$

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: $$\square L\leftrightarrow \square (\square L\to P)$$

Then, we can show that $\square L\leftrightarrow \square P$, i.e. they're equivalent! We do this by plugging $\square L$ into itself to get a twisty $\square P$. We can then replace each $\square L$ with $\square 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:

1. $⊢L\leftrightarrow (\square L\to P)$ (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:

2. $⊢\square (L\leftrightarrow (\square L\to P\left)\right)$ (from (1) by necessitation)
3. $⊢\square L\leftrightarrow \square (\square L\to P)$ (from (2) by box-distributivity in both directions)

We now want to show that $\square L\leftrightarrow \square P$. We can get the forward direction by feeding a copy of $\square L$ into itself:

4. $⊢\square L\to (\square \square L\to \square P)$ (box-distributivity on (3))
5. $⊢\square L\to \square \square L$ (internal necessitation)
6. $⊢\square L\to \square P$ (from (4) and (5))

The backward direction is equivalent to $\square P\to \square (\square L\to P)$, and is straightforward:

7. $⊢P\to (\square L\to P)$ (trivial)
8. $⊢\square P\to \square (\square L\to P)$ (necessitation and box-distributivity on (7))

Taking those together, we've shown $\square L$ and $\square P$ are equivalent.

9. $⊢\square L\leftrightarrow \square P$ (from (6) and (8))

Now we'd like to finish by appealing to the following chain: $$\square P\leftrightarrow \square L\leftrightarrow \square (\square L\to P)\leftrightarrow \square (\square P\to P)$$

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

10. $⊢(\square L\to P)\leftrightarrow (\square P\to P)$ (since $\square L$ and $\square P$ are equivalent by (9))
11. $⊢\square \left(\right(\square L\to P)\leftrightarrow (\square P\to P\left)\right)$ (from (10) by necessitation)
12. $⊢\square (\square L\to P)\leftrightarrow \square (\square P\to P)$ (from (11) by box-distributivity in both directions)

And that's everything we need:

13. $⊢\square P\leftrightarrow \square (\square P\to P)$ (from (3), (9), and (12))