Here’s a simple Kripke frame proof of Payor’s lemma.
Let ⟨W,R,⊩⟩ be a Kripke frame over our language, i.e.W is a set of possible worlds, R is an accessibility relation, and ⊩ judges that a sentence holds in a world. Now, suppose for contradiction that W⊩x↔□(□x→x) but that W⊮x, i.e.x does not hold in some world u∈W.
A bit of De Morganing tells us that the hypothesis on x is equivalent to ¬x↔◊(□x∧¬x), so u⊩◊(□x∧¬x). So, there is some world v with uRv such that v⊩□x∧¬x. But again looking at our equivalent form for ¬x, we see that W⊩¬x→◊¬x, so v⊩□x∧◊¬x, a contradiction. □
Both this proof and the proof in the post are very simple, but at least for me I feel like this proof tells me a bit more about what’s going on, or at least tells me something about what’s going on that the other doesn’t. Though in a broader sense there’s a lot I don’t know about what’s going on in modal fixed points.
Kripke frame-style semantics are helpful for thinking about lots of modal logic things. In particular, there are cool inductiony interpretations of the Gödel/Löb theorems. These are more complicated, but I’d be happy to talk about them sometime.
Nice, I like this proof also. Maybe there’s a clearer way to say thing, but your “unrolling one step” corresponds to my going from u to v. We somehow need to “look two possible worlds deep”.
Here’s a simple Kripke frame proof of Payor’s lemma.
Let ⟨W,R,⊩⟩ be a Kripke frame over our language, i.e.W is a set of possible worlds, R is an accessibility relation, and ⊩ judges that a sentence holds in a world. Now, suppose for contradiction that W⊩x↔□(□x→x) but that W⊮x, i.e.x does not hold in some world u∈W.
A bit of De Morganing tells us that the hypothesis on x is equivalent to ¬x↔◊(□x∧¬x), so u⊩◊(□x∧¬x). So, there is some world v with uRv such that v⊩□x∧¬x. But again looking at our equivalent form for ¬x, we see that W⊩¬x→◊¬x, so v⊩□x∧◊¬x, a contradiction. □
Both this proof and the proof in the post are very simple, but at least for me I feel like this proof tells me a bit more about what’s going on, or at least tells me something about what’s going on that the other doesn’t. Though in a broader sense there’s a lot I don’t know about what’s going on in modal fixed points.
Kripke frame-style semantics are helpful for thinking about lots of modal logic things. In particular, there are cool inductiony interpretations of the Gödel/Löb theorems. These are more complicated, but I’d be happy to talk about them sometime.
Thanks! I also wrote up my proof in another comment, which should help triangulate intuition.
Nice, I like this proof also. Maybe there’s a clearer way to say thing, but your “unrolling one step” corresponds to my going from u to v. We somehow need to “look two possible worlds deep”.