Modal depth

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.

Definition

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 )}$

Example

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}$

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 ${\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.

References

1. Nguyen, Linh Anh. "Constructing the Least Models for Positive Modal Logic Programs" (PDF). p. 32. Archived from the original (PDF) on January 26, 2019. Retrieved January 26, 2019.