Modal depth

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

${\displaystyle \operatorname {MD} (\Box (\Box p\rightarrow p))}$

${\displaystyle =1+\operatorname {MD} (\Box p\rightarrow p)}$

${\displaystyle =1+\max(\operatorname {MD} (\Box p),\operatorname {MD} (p))}$

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

${\displaystyle =1+\max(1+0,0)}$

${\displaystyle =1+1}$

${\displaystyle =2}$

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 ${\displaystyle M,w\models \Diamond \Diamond \varphi }$, one needs to check whether there exists an accessible world ${\displaystyle v}$ for which ${\displaystyle M,v\models \Diamond \varphi }$. If that is the case, one needs to check whether there is also a world ${\displaystyle u}$ such that ${\displaystyle M,u\models \varphi }$ and ${\displaystyle u}$ is accessible from ${\displaystyle v}$. We have made two steps from the world ${\displaystyle w}$ (from ${\displaystyle w}$ to ${\displaystyle v}$ and from ${\displaystyle v}$ to ${\displaystyle 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., ${\displaystyle \Box \varphi }$ holds for all ${\displaystyle \varphi }$ in a world ${\displaystyle w}$ when ${\displaystyle \forall v\in W\ (w,v)\not \in R}$, where ${\displaystyle W}$ is the set of worlds and ${\displaystyle R}$ is the accessibility relation). To check whether ${\displaystyle 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 ${\displaystyle w}$; the formula now trivially holds by the previous observation about the validity of formulas with a box as outer operator.