Modal Logic

Read the intro of First-order Logic for a more abstract view of how Formal Systems and Logics are defined and characterized.

Modal Logic is a class of Formal (Logic) Systems.

In general, a Modal Language is the language of Propositional Logic extended with new unary connectives – modalities. They express the notion of “possibility”.

Then, the Rules of Inference of a modal language may vary across different compositions of axioms, or conditions on frames (name for modal-structures).

This document discusses Standard/Normal Modal Logic (“K”), which defines two modalities – $\lozenge$ (possibly) and $\square$ (necessarily) – and its extensions.

As a Logic, Modal Logic is considered non-classical, whereas Propositional and First-order Logics are classical.

Syntax

Alphabet

Nothing remarkable;

• everything from Propositional Logic
• Modalities – new unary connectives
  • $\square$
  • $\lozenge$

Well-Formed Formulas

Still nothing remarkable. Read that of Propositional Logic, then add two more unary connectives, the modalities, analogous to $\lnot$'s rules. (They also the highest precedence alongside $\lnot$.)

Semantics

Specifically, we’re discussing Kripke semantics (aka. relational semantics or frame semnatics).

Modal Structures

An $\mathcal{L}$-structure, aka. Modal / Kripke Frame, is a pair $M = \braket{W, R}$:

• $W$ – the Universe
  a (possibly empty) set of worlds
• $R$ – Accessibility Relation
  a binary relation on $W$
  for $w_1, w_2 \in W$, $\ (w_1, w_2) \in R \space$ iff $\ w_2$ is accessible from $w_1$ ¹

In Graph Theory, $M$ is a directed graph with vertices $W$ and edges $R$.
Intuitively, it is a map of worlds and how they’re interconnected.

Formulas are interpreted with respect to (“in”) a given world. A world represents a state of truth – i.e., the trueness of a proposition is dependent on the world it’s in.
The “neighbors” of a world (as given by $R$) are the possibilities as seen from said world. This is how “necessity” and “possibility” are formally treated.

Valuations

As an $\mathcal{L}$-structure can have multiple worlds, a valuation does not directly assign propositions truth values – rather, specifies which propositions are true in which worlds.

A valuation in an $\mathcal{L}$-structure $\braket{W^M, R^M}$ is a mapping
$$\rho : W^M \times \mathcal{P} \mapsto \{ \top, \bot \}$$

where $\rho(w, P) = \top \space$ iff $\ P$ is true in world $w$.

Some instead have $\rho : \mathcal{P} \mapsto W^M$ – i.e., $\rho(P)$ is the set of worlds where $P$ is true.

Combined, we get an interpretation / relational model $\mathfrak{M} = \braket{W, R, \rho}$.

Then, the evaluation of a formula at a world $w$ in a model $\mathfrak{M}$ is defined inductively.
For $P \in \mathcal{P}$; $\varphi, \psi \in \mathcal{L}$; and binary connective $\text{op}$,
$$\begin{align*} \mathfrak{M}, w \models P &\iff \rho(w, P) \\ \mathfrak{M}, w \models \lnot \varphi &\iff w \not \models \varphi \\ \mathfrak{M}, w \models (\varphi \;\text{op}\; \psi) &\iff (w \models \varphi) \;\text{op}\; (w \models \psi) \\ \mathfrak{M}, w \models \square \varphi &\iff \forall u \in W^\mathfrak{M} : w R^\mathfrak{M} u \rightarrow u \models \varphi \\ \mathfrak{M}, w \models \lozenge \varphi &\iff \exists u \in W^\mathfrak{M} : w R^\mathfrak{M} u \land u \models \varphi \\ \end{align*}$$

Alternative notation for $\mathfrak{M}, w \models \varphi$ (specifying both a structure and a valuation) includes $M, w \models_\rho \varphi$, which is more explicit about the valuation.

The intuitive implications are clear:

• a statement is necessary (from world $w$) if it holds in every world accessible from $w$;
• a statement is possible (from world $w$) if it holds in at least one world accessible from $w$.

Satisfaction Relation (Validity & Satisfiability)

A definition of $\models$ as used above. It is called a satisfaction relation as it denotes the satisfaction (trueful-evaluation) of a formula under an interpretation.

Some authors use $\Vdash$, defined within $\mathfrak{M}$ as an equivalent replacement for $\rho$, instead of the meta-language symbol $\models$.²
We use subscript notation, $\models_\rho$, to achieve the same effect.

For valuation $\rho$ for frame $M = \braket{W, R}$ and $w \in W$,

“$\varphi$ is true (under $\rho$) at $w$ (in $M$)”
$\iff M, w \models_\rho \varphi$

“$\varphi$ is valid in $M$”
$\iff M \models \varphi$
$\iff \forall \rho\, \forall w : M, w \models_\rho \varphi$

“$\varphi$ is valid”
$\iff \,\models \varphi$
$\iff \forall M : M \models \varphi$

“$\varphi$ is satisfiable in $M$”
$\iff M \not \models \lnot \varphi$
$\iff \exists \rho\, \exists w : M, w \models_\rho \varphi$

“$\varphi$ is satisfiable”
$\iff \,\not \models \lnot \varphi$
$\iff \exists M : (\exists \rho\, \exists w : M, w \models_\rho \varphi)$
I.e., “$\varphi$ is satisfiable in some frame”.

As usual, validity and satisfiability are duals.

Validity $\implies$ Validity (in a frame) $\implies$ Satisfiability (in that frame) $\implies$ Satisfiability.

Rules of Inference

Multiple deductive systems are commonly used with modal logic (unlike propositional- or first-order- logics, where one “common” system prevails.)
They’re called modal systems.

One way axioms can be defined for modalities, unique to Kripke semantics, is via frame conditions (properties on $R$).

Observe from above how inference (implication) between modalities is defined in terms of $R$.

Base Axioms

Recall we’re discussing normal modal logics; here N and K (collectively called just K) are the two primitive axioms.
(They also aren’t definable as frame conditions.)

N – Necessitation
$$(\models \varphi) \implies (\models \square \varphi)$$

I.e., if $\varphi$ is a tautology, then so is $\square \varphi$.

K – Distribution
$$\square (\varphi \rightarrow \psi) \implies (\square \varphi \rightarrow \square \psi)$$

Or, equivalently, $\square \big[(\varphi \rightarrow \psi) \land \varphi \big] \implies \square \psi$, establishing Modus Ponens in modal logic.

Frame Conditions

Combinations of frame conditions (and any other forms of axioms) form modal systems.

Common frame conditions (their code names in bold) and equivalent axioms:

• T: Reflexivity – $\forall w : w R w$
  $\quad \varphi \rightarrow \lozenge \varphi \space$ (and so $\square \varphi \rightarrow \varphi$)
• B: Symmetry – $\forall w, u : w R u \rightarrow u R w$
  $\quad \varphi \rightarrow \square\lozenge \varphi \space$ (and so $\lozenge\square \varphi \rightarrow \varphi$)
• 4: Transitivity – $\forall w, u, q : w R u \land u R q \rightarrow w R q$
  $\quad \square \varphi \rightarrow \square \square \varphi$
• D: Serial-ness – $\forall w\, \exists u : w R u$
  $\quad \square \varphi \rightarrow \lozenge \varphi$
• 5: Euclidean-ness – $\forall w, u, q : w R u \land w R q \rightarrow u R q$
  $\quad \lozenge \varphi \rightarrow \square\lozenge \varphi$

(where the domain for the quantifiers is, of course, $W$.)

Graph theory again:

• Reflexivity = all vertices have self-loops
• Symmetry = undirected graph / all edges are bidirectional
• Transitivity = a vertex’s “neighbors” is its transitive closure
• Serial-ness = all outdegree > 0
• Euclidean-ness = bruh.

For a B frame, 5 $\Leftrightarrow$ 4.
T + 5 $\implies$ B + 4, and
B + 4 + D $\implies$ T + 5; or
for a T frame, 5 $\Leftrightarrow$ B + 4.

There are other possible formulations and names for various types of frames – see table on Wikipedia.

Common modal systems, their frame conditions and code names:

• K: normal – (N, K), implied in all these below:
• T: reflexive – T
• K4: transitive – 4
• S4: preorder – T + 4 $\space$
• S5: equivalent – T + 5 $\space$ $R$ is an equivalence relation here

Equivalences

Derived identities (from the above axioms).

Duality

$\lozenge$ and $\square$ are duals (as observable from their definitions in Valuations above). I.e,
$$\begin{align*} \square \varphi &\equiv \lnot\mkern1mu\lozenge\mkern1mu\lnot \varphi \\ \lozenge \varphi &\equiv \lnot\square\lnot \varphi \\ \end{align*}$$

Others

xD

---

1. (as usual with binary relations), $R$ is usually used in infix or prefix notation; i.e., $(w_1, w_2) \in R$ can be written $w_1 R w_2$ or $R w_1 w_2$. ↩︎

2. okay, there’s more to this; $\Vdash$ means “forces” and is a model-theoretic symbol… It is technically more accurate to use this “forces” instead of “models”… but whatever im lazy to figure out the specifics rn ↩︎