Modal Logic Playground

Number of propositional variables:
No state selected
p:
q:
r:
s:
t:
  • Click in the open space to add a state
  • Drag between states to add a transition
  • Ctrl-drag a state to move graph layout
  • Click a state or a transition to select it
  • When a state is selected:
    • R toggles reflexivity
    • Delete removes the state
  • When a transition is selected:
    • L(eft), R(ight), B(oth) change direction
    • Delete removes the transition
Enter a formula:
  • When entering a formula:
    • use ~A for $\lnot{}A$
    • use []A for $\Box{}A$
    • use <>A for $\Diamond{}A$
    • use (A & B) for $(A\land{}B)$
    • use (A | B) for $(A\lor{}B)$
    • use (A -> B) for $(A\rightarrow{}B)$
    • use (A <-> B) for $(A\leftrightarrow{}B)$

So what's modal logic, anyway?

Modal logic is a type of symbolic logic for capturing inferences about necessity and possibility. As with other logical systems, the theory lies at the intersection of mathematics and philosophy, while important applications are found within computer science and linguistics.

This app is a graphical semantic calculator for a specific kind of modal logic, modal propositional logic, which extends propositional logic but lacks quantifiers (∀ and ∃). Let's take a whirlwind tour.

From propositional logic...

To start out, let's briefly recall the language and semantics of propositional logic, i.e., connectives and truth tables.[1]
The usual connectives are the following:

SymbolRead asOperationNatural language example[2]
$\lnot$'not'negationIt is not raining.
$\land$'and'conjunctionIt is snowing and it is cold.
$\lor$'or'disjunctionIt is raining or it is cold.
$\rightarrow$'if...(then)'implicationIf it is snowing, (then) it is cold.
$\leftrightarrow$'iff'equivalence3 × 2 = 6 if and only if 3 + 3 = 6.

A typical (long-form) truth table would look something like this (using 0 for false and 1 for true):

$p$$q$$(q\rightarrow{}p)$$(p\rightarrow{}(q\rightarrow{}p))$
0011
0101
1011
1111

So once we've fixed a truth value for each of the propositional variables, the truth value of any formula using those variables is deterministic.

...to modal propositional logic

Now, in modal logic, we add two new unary connectives to our familiar language:

SymbolRead asOperationNatural language example[2]
$\Box$'box'necessityIt must be cold outside.
$\Diamond$'diamond'possibilityIt may be snowing.

Semantically, these modal connectives are interpreted with respect to possible worlds. We can conceive of possible worlds in various ways, depending on what we're interested in modelling. On the one hand, possible worlds might be hypothetical 'alternate universes': there is the 'actual world', the way things really are at the present moment, as well as an infinity of other 'worlds' which differ in ways both subtle (such as a world where my pen is simply on the opposite side of my desk) and dramatic (such as a world in which dinosaurs still roam Earth in 2013 CE). Alternatively, possible worlds might be the various states of a computer, a computer program, or another system which evolves over time.

Regardless, if we have a proposition $p$ and current world $w$:

  • $\Box{}p$ holds ($p$ is necessary) just when $p$ is true in all worlds accessible from $w$
  • $\Diamond{}p$ holds ($p$ is possible) just when $p$ is true in at least one world accessible from $w$

What does it mean for a world to be 'accessible'? The clearest example is surely that of a computer: an 'accessible' state is simply a successor state, one that is immediately reachable from the current state. As such, the set of all possible worlds isn't just an unstructured mess, but is ordered by an accessibility relation that says which worlds we can get to from which others.

Let's illustrate this further with an example from linguistics. When one speaks of what may or must be so, we can view this as talking about what is true in some or all possible worlds. Yet we're seldom concerned with every single possible world at once: when conversing about the current weather, things like pens and dinosaurs are typically far from one's mind. Rather, we're only concerned with a relevant subset of these possibilities—just those worlds which are accessible from the actual world via some implicit relation.

The English sentences below show three kinds of accessibility relations at work:

Example sentenceModality typeAccessible worlds
It must have rained overnight.epistemicworlds consistent with one's knowledge
You must arrive before noon.deonticworlds consistent with one's obligations
A triangle must have three vertices.alethicworlds consistent with logic (= all worlds)

These sentences might be represented as $\Box{}p$, $\Box{}q$, and $\Box{}r$, but the box operator has a noticeably different interpretation in each case.

In the first case, we can imagine someone who, upon leaving their house in the morning, notices that the sidewalk is wet. Based on this observation, they conclude that it has rained overnight. Here, the worlds under consideration are just those which are consistent with the speaker's knowledge, in particular, their observation of the sidewalk. Thus the box means something like, 'Given what is known, it must be the case that...'. This 'knowledge-based' interpretation of the modal operators is known as epistemic modality.

The second sentence might be uttered by airport staff to inform a passenger of the time that their flight boards. In this case, the relevant worlds are those consistent with the passenger's obligations, namely, to get to their airplane punctually. The box here means, 'Given what is obligated, it must be the case that...'. This 'obligation-based' interpretation of the modal operators is known as deontic modality.

Finally, suppose that we remove all restrictions and let the modal operators range over every single possible world at once. But we've talked about the infinity of possible worlds—what could they possibly all have in common? One thing only: logical consistency. Under this so-called alethic modality, the box now means, 'It is logically necessary that...'. This interpretation may not be commonplace in daily conversation, but is useful for discussing mathematics, as in the third sentence: by definition, a triangle has three vertices, otherwise it wouldn't be a triangle!

Conveniently, we can view possible world semantics as an extension of truth tables. In propositional logic, we only had to fix a truth value for each propositional variable once, but in modal logic, each propositional variable can take a different truth value at each possible world. Even when two worlds have the same truth assignment, formulas with $\Box$ or $\Diamond$ might have a different truth value in each world, since the worlds accessible from each may not be the same. Thus we might say that each possible world "has its own truth table". A complete assignment of truth values to each variable at each world is known as a valuation.

Altogether, a set of possible worlds, an accessibility relation, and a valuation form a semantic model for modal logic, known as a Kripke model. A Kripke model can be visualized as a directed graph, where nodes represent worlds, the set of edges represents the accessibility relation, and the valuation is indicated by annotating each node with its truth assignment.

As a culminating example, let's take a look at the following graph, which happens to be the initial model for the app:

0 ¬p, ¬q 1 p, ¬q 2 ¬p, q

Using the computer program metaphor, imagine a scenario where $p$ stands for 'the program is running' and $q$ stands for 'the program has terminated'. Then state 0 of our model represents the state where the program is about to launch (neither running nor terminated), state 1 is the running (and non-terminated) state, and state 2 is the terminated (and no longer running) state. As for the accessibility relation: from the ready-to-launch state, the only option is to transition to the running state; at the running state, the program can either continue to run (the reflexive edge is indicated by a bold circle) or terminate; and the terminated state is the end of the line, so to speak.

We can then evaluate formulas based on this model. For instance, $\Diamond(p\land\lnot{}q)$ says 'there is a transition to a running-and-not-terminated state (i.e., to state 1)', or more naturally, that the program is able to run (or keep running). This formula is true at states 0 and 1 but false at state 2, which can be expressed in the following notation (the 'double turnstile' $\models$ can be read as 'satisfies' or 'makes...true'):

$w_0\models\Diamond(p\land\lnot{}q)$
$w_1\models\Diamond(p\land\lnot{}q)$
$w_2\not\models\Diamond(p\land\lnot{}q)$

To see this in action, try using the app to evaluate <>(p & ~q) at each state!

Hungry for more?

This whirlwind tour has only scratched the surface of modal logic—if you're curious to learn more, here are a few useful resources: