Models for Modal Logic

The fundamental insight of models for modal logic is that modal logic is for describing hypothetical worlds. In fact, hypothetical reasoning is itself a modality, though that's for a later time. For example, in the logic of time I described in my last post, if right now it is time t, I can use the eventually modality to describe all the worlds that might exist at later times. Or, in the logic of knowledge, I use the knows(a) modality to describe all the worlds that a thinks might be the real one.

Generally, a world is all the information needed to definitively decide whether a proposition is true or false. To give you an example, let's go back this axiom for describing the behavior of a computer system:

pressed(button) → halted

To decide whether this sentence is true or false, we'd need to know whether or not the button is pressed or not, and whether the computer is halted or now. So a world must contain a pair of button and computer state: (PRESSED, HALTED) is a world, as is (UNPRESSED, RUNNING). A model of this axioms is a set of such worlds where the implication above is true. For example, the set {(PRESSED, HALTED), (UNPRESSED, HALTED), (UNPRESSED, RUNNING)} is a model of that axiom.

Suppose we now want to reason instead about the behavior of this system over time, using the modal axiom:

pressed(button) → eventually halted

This proposition might true at some points in time and not others (“if the button were pressed right now, the computer will eventually halt”), so our possible worlds must include a timestamp of some sort. But to understand that eventually statement we must be able to think about what will happen at future times. That is, if a world is a triple of time, button state, and computer state, then at state (t, b, c) there are some states (s, b', c') that we might later find ourselves in. The axiom above describes a property of how those states are related to each other: that for any state (t, PRESSED, c), there is a state (t + k, b, HALTED) that you might later find yourself in.

We model eventually P as P being true in at least one of the worlds that might eventually follow your current one. This notion of one world following the next can be wrapped up in a relation (called the accessibility relation), so that the statement eventually P to be true at world w exactly when P is true at a world related to w.

So a model of a set of modal axioms is a collection of logical worlds and an accessibility relation between them.

We can always look at what propositions are true in a given model, and look at what models validate a given axiom.

How does one know if a proposition is true at a world? Non-modal propositions can be checked normally. A positive modality, like eventually P, means at least one accessible world has P true. A negative modality, like knows(a) P, demands that all accessible worlds have P true. For example, eventually P is true when there's at least one future time when P is true, and knows(a) P is true when all worlds that a things are possible have P true.

Which models validate a given axiom? One interesting case is those axioms that only involve modal operators, but no terms like pressed or halted that are specific to the system in question. Since these can't say much about individual worlds, these axioms necessarily describe a property of the accessibility relation. Often, the property described is natural and interesting on its own:

Theorem: Let M be a negative modality. Then ∀ p, M p → M M p if and only if all models of the modality M have transitive accessibility relations.

The core of the proof is that if M p true at a world w, then

∀ u, w ~ u → p(u)

Meanwhile, if M M p is true at w, then

∀ u v, w ~ u ∧ u ~ v → p(v)

Proof: Fix w, u and v where w ~ u and u ~ v. I must prove that w ~ v to prove that the accessibility relation is transitive. I'll do that by contradiction. I choose p to be true everywhere but v, and suppose w ~̸ v is not true. Then M p is true at w, since the one world where p is false isn't accessible from w. But M p is definitely false at u, since u ~ v; so M M p is false at w, since w ~ u. So we have M p but not M M p at w. This contradicts M p → M M p, so the hypothesis that w ~̸ v must be false.

For the reverse direction, we have w ~ u and u ~ v and ∀ u, w ~ u → p(u); yet since the relation is transitive we have w ~ v so p(v). ∎

Note that this theorem relies directly on the second-order nature of the axiom ∀ p, M p → M M p. In first-order logic, you'd only see the backward direction of this theorem.

This gives you two ways of thinking about modal axioms. You can write down a few modal axioms that seem reasonable, then think about the properties those axioms would have in a model. For example, I used the axioms ¬eventually p → ¬ p and eventually eventually p → eventually p to describe my logic of time. They correspond to a reflexive and transitive accessibility relation (note that eventually is positive, not negative, so the axiom is dual of that in the theorem above). I want any world to be able to access any world at a later time, which is in fact reflexive and transitive.

By reasoning through the properties you want to guarantee of your accessibility relation you can quickly axiomatize complicated modalities.