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↔□(□P→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:
□L↔□(□L→P)
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↔(□L→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:
⊢□(L↔(□L→P)) (from (1) by necessitation)
⊢□L↔□(□L→P) (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→□(□L→P), and is straightforward:
⊢P→(□L→P) (trivial)
⊢□P→□(□L→P) (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↔□(□L→P)↔□(□P→P)
We've proven all but the last part of the chain. Here are the steps that let us do the substitution:
⊢(□L→P)↔(□P→P) (since □L and □P are equivalent by (9))
⊢□((□L→P)↔(□P→P)) (from (10) by necessitation)
⊢□(□L→P)↔□(□P→P) (from (11) by box-distributivity in both directions)
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↔□(□P→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: □L↔□(□L→P)
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:
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:
We now want to show that □L↔□P. We can get the forward direction by feeding a copy of □L into itself:
The backward direction is equivalent to □P→□(□L→P), and is straightforward:
Taking those together, we've shown □L and □P are equivalent.
Now we'd like to finish by appealing to the following chain: □P↔□L↔□(□L→P)↔□(□P→P)
We've proven all but the last part of the chain. Here are the steps that let us do the substitution:
And that's everything we need: