$$

Introduction to Modal Logic

(draft) … (up)

Motivation

Superficially, modal logic adds to the propositional connectives

$\wedge$ (and),

$\vee$ (or),

$\mathrm{\neg }$ (not) two new connectives that allow us to take any formula

$\varphi$ and form two new formulas

$$◻\varphi ◊\varphi .$$

One of the reasons modal logic has been so important is that there are so many possible interpretations for these connectives. For example,

• $◻\varphi$ means necessarily
  $\varphi$ and
  $◊\varphi$ means possibly
  $\varphi$,
• $◻\varphi$ means always
  $\varphi$ and
  $◊\varphi$ means sometimes
  $\varphi$,
• ${◻}_i\varphi$ means agent
  $i$ knows
  $\varphi$ and
  ${◊}_i\varphi$ means agent
  $i$ thinks
  $\varphi$ is possible.

(Temporal and Epistemic Logic) Each of these interpretations created their own field of research. The first one dominated modal logic in the first half of the 20th century. The second one is known as temporal logic and has been playing an important role in computer science (verificiation, model checking) since the 1980ies. The third one is known as epistemic logic and continues to be cutting edge in philosophy, economics, software engineering, AI and other areas.

Besides temporal logic and epistemic logic there is also … (insert more examples) …

(Fragments of First-Order Logic) Another reason modal logic has been important is as a fragment of first-order logic. As we can see from the examples above,

$◻\varphi$ is a universal quantifier (eg always) and

$◊\varphi$ is an existential quantifier (eg sometimes). Consequently, modal logic is a fragment of first-order logic. In fact, modal logic is a fragment of first-order logic in at least two different but interesting ways:

• Modal logic is a decidable fragment of first-order logic.
• Modal logic is the bisimulation invariant fragment of first-order logic.

The first point has given rise to various generalisations of modal logic, in particular in the area of automated theorem proving. Search for guarded fragment for references.

In the second point bisimulation refers to a relation of observational or behavioural equivalence of dynamic systems, which are themselves considered as "black boxes". In fact, bisimulation is the natural notion of behavioural equivalence for non-determinstic transition systems in which the states themselves are not observable but choices are. This leads us to the next item.

(Possible Worlds Semantics) The idea that something is necessarily true if it is true in all possible worlds is an old one. The turning point for modal logic was the mathematical formalisation of possible world semantics by Kripke:

• Saul Kripke: A Completeness Theorem in Modal Logic. 1959.
• Saul Kripke: Semantical Analysis of Modal Logic I. 1963. I recommend Section 2.1, which also contains the solution to one of the exercises below.
• Saul Kripke: Semantical Analysis of Modal Logic II. 1965.

There is a lot to say here, but to present the main ideas as quickly as possible I would proceed as follows (see Chapters 3.1 and 3.2 of the book referenced below).

Definition: Let

$Prop$ be a set of 'propositional variables'. The language of modal logic is the smallest set of 'formulas' containing

$Prop$ and closed under

$\wedge$ ,

$\vee$,

$\mathrm{\neg }$,

$◻$,

$◊$.

Definition: Let

$W$ be a set of 'worlds' and

$R\subseteq W\times W$. Let

$[[-]]:Prop\to 2^W$ be a function assigning sets of worlds to each atomic proposition. Define

$$\begin{array}{rl}[[\varphi \wedge {\varphi }^{\prime }]]& =[[\varphi ]]\cap [[{\varphi }^{\prime }]]\\ [[\varphi \vee {\varphi }^{\prime }]]& =[[\varphi ]]\cup [[{\varphi }^{\prime }]]\\ [[\mathrm{\neg }\varphi ]]& =W\setminus [[\varphi ]]\\ [[◻\varphi ]]& =\{w\in W\mid \mathrm{\forall }v\in W.v\in [[\varphi ]]\}\\ [[◊\varphi ]]& =\{w\in W\mid \mathrm{\exists }v\in W.v\in [[\varphi ]]\}\end{array}$$
and

$$(W,R)\models \varphi$$

iff

$[[\varphi ]]=W$ for all choices of

$[[-]]:Prop\to 2^W$.

It is convenient to write

$$w⊩\varphi \stackrel{\mathrm{d}\mathrm{e}\mathrm{f}}{⟺}w\in [[\varphi ]].$$

The following exercise is a straightforward unvraveling of definitions:

Exercise: If

$R$ is reflexive, then

$(W,R)\models ◻p\to p$.

A crucial observation that lets us glimpse the power of Kripke's approach is that the converse is also true.

Prop: If

$(W,R)\models ◻p\to p$, then

$R$ is reflexive.

The proof is short once you know the trick. Try to find it for yourself before looking at the footnote.^[1]

The proof can be generalised to a method applying to all so-called Sahlqvist formulas and the area of modal logic is known as correspondence theory. We just look at one other basic example:

Exercise:

$(W,R)\models ◻p\to ◻◻p$ iff

$R$ is transitive.

Remark: In the early 20th century modal logics where developed by philosophers from a syntactic and proof theoretic point of view. Axioms such as

$◻p\to p$ and

$◻\varphi \to ◻◻\varphi$ where discovered by reading them as "necessarily p implies p" and "necessarily p implies necessarily necessarily p" and modal logics where characterised by axioms and proof rules. As far as I know the history, it came as a surprise that these axioms had such a neat semantic characterisation.

Exercise: Interpret

$◻p\to p$ and

$◻p\to ◻◻p$ from the point of view of temporal and epistemic logic.

Further Reading

The paper

• Halpern, Vardi: Model Checking v. Theorem Proving: A Manifesto. 1991.

illustrates many of the themes that make modal logic so important for computer science applications.

The Basic Theory of Modal Logic

We have seen that modal logic comprises several independent areas (temporal logic, epistemic logic, etc) and has important overlaps with others (concurrency, multi-agent systems, automated reasoning, game theory, etc). My intention here is only to sketch out the basic theory that is important in all these fields.

Actually, instead of writing this out myself, I refer to the book "Modal Logic" by Blackburn, de Rijke, Venema.(The book treats also

$n$-ary relations (the "general case", as opposed to binary relations). This generalisation is interesting for some applications but should be skipped on a first reading.)

Here is what I would consider essential for a first run through the basics of modal logic.

• 1.2: Modal Languages
• 1.3: Models and Frames
• 1.5: Semantic Consequence
• 1.6: Normal Modal Logics
• 2.1: Invariance Results (Def 2.10 and Prop 2.14)
• 2.2: Bisimulations (up to Thm 2.20)
• 2.3: Finite Models (can be skipped on first reading)
• 2.4: The Standard Translation (up to Prop 2.47)
• 3.1: Frame Definability (Exle 3.6)
• 3.2: Frame Definability and Second-Order Logic (Exle 3.11)

References

Blackburn, de Rijke, Venema: "Modal Logic".

---

1. Proof: Let

   $w\in W$. Let
   $[[p]]=\{v\mid wRv\}$. We know
   $w⊩◻p$ by definition of
   $[[◻p]]$ and
   $w⊩◻p\to p$ by assumption. It follows
   $w⊩p$, which implies
   $wRw$ by definition of
   $[[p]]$. ↩︎