This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources. Find sources: "Modal depth" – news · newspapers · books · scholar · JSTOR (November 2019)

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

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

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

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

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

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

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

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

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

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

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

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.