Modal Depth

In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly $\Box$ and $\Diamond$). Modal formulas without modal operators have a modal depth of zero.

Definition

Modal depth can be defined as follows. Let $\operatorname(\phi)$ be a function that computes the modal depth for a modal formula $\phi$:

:$\operatorname(p) = 0$, where $p$ is an atomic formula.
:$\operatorname(\top) = 0$
:$\operatorname(\bot) = 0$
:$\operatorname(\neg \varphi) = \operatorname(\varphi)$
:$\operatorname(\varphi \wedge \psi) = \max(\operatorname(\varphi), \operatorname(\psi))$
:$\operatorname(\varphi \vee \psi) = \max(\operatorname(\varphi), \operatorname(\psi))$
:$\operatorname(\varphi \rightarrow \psi) = \max(\operatorname(\varphi), \operatorname(\psi))$
:$\operatorname(\Box \varphi) = 1 + \operatorname(\varphi)$
:$\operatorname(\Diamond \varphi) = 1 + \operatorname(\varphi)$

Example

The following computation gives the modal depth of $\Box ( \Box p \rightarrow p )$:

:$\operatorname(\Box ( \Box p \rightarrow p ))$
:$= 1 + \operatorname( \Box p \rightarrow p)$
:$= 1 + \max(\operatorname(\Box p), \operatorname(p))$
:$= 1 + \max(1 + \operatorname(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 \Diamond \Diamond \varphi$, one needs to check whether there exists an accessible world $v$ for which $M, v \models \Diamond \varphi$. If that is the case, one needs to check whether there is also a world $u$ such that $M, u \models \varphi$ 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., $\Box \varphi$ holds for all $\varphi$ in a world $w$ when $\forall v \in W \ (w, v) \not \in R$, where $W$ is the set of worlds and $R$ is the accessibility relation). To check whether $M, w \models \Box \Box \varphi$, 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.

References

{{ reflist

Depth