Modal depth

Modal depth can be defined as follows.[1] Let ${\displaystyle MD(\phi )}$ be a function that computes the modal depth for a modal formula ${\displaystyle \phi }$:

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

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

${\displaystyle MD(\bot )=0}$

${\displaystyle MD(\neg \varphi )=MD(\varphi )}$

${\displaystyle MD(\varphi \wedge \psi )=max(MD(\varphi ),MD(\psi ))}$

${\displaystyle MD(\varphi \vee \psi )=max(MD(\varphi ),MD(\psi ))}$

${\displaystyle MD(\varphi \rightarrow \psi )=max(MD(\varphi ),MD(\psi ))}$

${\displaystyle MD(\Box \varphi )=1+MD(\varphi )}$

${\displaystyle MD(\Diamond \varphi )=1+MD(\varphi )}$

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

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

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

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

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

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

${\displaystyle 1+1=: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.