# Models for Modal Logic

In a previous post, I introduced modal logic as a common way of adding an operation from propositions to propositions to ordinary logic. In that post, I noted that you want to add the operator, and then axiomatize some properties of it.

Now I want to examine the model of modal logic, to shed more light on what the axioms mean. The particular type of model used for modal logic is called a Kripke structure.1 Before I describe those, let's talk about hypothetical worlds.

## Hypothetical worlds

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.

## Modalities move between worlds

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.

## Axioms to models and back

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.

## Using models

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.

1
More precisely, only “normal” modal logics have a Kripke structure as their semantics. I know nothing, and plan to say nothing, about non-normal modal logics.

By on . Share it—it's CC-BY-SA licensed.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.