Philosophy:Modal depth

Short description: Modal logic term

Template:Singlesource In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly $◻$ and $◊$). Modal formulas without modal operators have a modal depth of zero.

Definition

Modal depth can be defined as follows. Let $\mathrm{MD}(\varphi )$ be a function that computes the modal depth for a modal formula $\varphi$:

$\mathrm{MD}(p)=0$, where $p$ is an atomic formula.

$\mathrm{MD}(\mathrm{\top })=0$

$\mathrm{MD}(\mathrm{\perp })=0$

$\mathrm{MD}(\mathrm{\neg }\phi )=\mathrm{MD}(\phi )$

$\mathrm{MD}(\phi \wedge \psi )=\max (\mathrm{MD}(\phi ),\mathrm{MD}(\psi ))$

$\mathrm{MD}(\phi \vee \psi )=\max (\mathrm{MD}(\phi ),\mathrm{MD}(\psi ))$

$\mathrm{MD}(\phi \to \psi )=\max (\mathrm{MD}(\phi ),\mathrm{MD}(\psi ))$

$\mathrm{MD}(◻\phi )=1+\mathrm{MD}(\phi )$

$\mathrm{MD}(◊\phi )=1+\mathrm{MD}(\phi )$

Example

The following computation gives the modal depth of $◻(◻p\to p)$:

$\mathrm{MD}(◻(◻p\to p))$

$=1+\mathrm{MD}(◻p\to p)$

$=1+\max (\mathrm{MD}(◻p),\mathrm{MD}(p))$

$=1+\max (1+\mathrm{MD}(p),0)$

$=1+\max (1+0,0)$

$=1+1$

$=2$

Modal depth and semantics

The modal depth of a formula indicates 'how far' one needs to look in a Kripke model when checking the validity of the formula. For each modal operator, one needs to transition from a world in the model to a world that is accessible through the accessibility relation. The modal depth indicates the longest 'chain' of transitions from a world to the next that is needed to verify the validity of a formula.

For example, to check whether $M,w\models ◊◊\phi$, one needs to check whether there exists an accessible world $v$ for which $M,v\models ◊\phi$. If that is the case, one needs to check whether there is also a world $u$ such that $M,u\models \phi$ and $u$ is accessible from $v$. We have made two steps from the world $w$ (from $w$ to $v$ and from $v$ to $u$) in the model to determine whether the formula holds; this is, by definition, the modal depth of that formula.

The modal depth is an upper bound (inclusive) on the number of transitions as for boxes, a modal formula is also true whenever a world has no accessible worlds (i.e., $◻\phi$ holds for all $\phi$ in a world $w$ when $\mathrm{\forall }v\in W(w,v)\in ̸R$, where $W$ is the set of worlds and $R$ is the accessibility relation). To check whether $M,w\models ◻◻\phi$, it may be needed to take two steps in the model but it could be less, depending on the structure of the model. Suppose no worlds are accessible in $w$; the formula now trivially holds by the previous observation about the validity of formulas with a box as outer operator.