Modal depth explained

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.^[1] Let

MD(\phi) be a function that computes the modal depth for a modal formula \phi :MD(p) = 0 , where p is an atomic formula.MD(\top) = 0 MD(\bot) = 0 MD(\neg \varphi) = MD(\varphi) MD(\varphi \wedge \psi) = max(MD(\varphi), MD(\psi)) MD(\varphi \vee \psi) = max(MD(\varphi), MD(\psi)) MD(\varphi → \psi) = max(MD(\varphi), MD(\psi)) MD(\Box \varphi) = 1 + MD(\varphi) MD(\Diamond \varphi) = 1 + MD(\varphi)

Example

The following computation gives the modal depth of

\Box ( \Box p → p ) :MD(\Box ( \Box p → p )) = 1 + MD( \Box p → p) = 1 + max(MD(\Box p), MD(p)) = 1 + max( 1 + MD(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.

Notes and References

1. Web site: Constructing the Least Models for Positive Modal Logic Programs. Nguyen. Linh Anh. January 26, 2019. January 26, 2019. https://web.archive.org/web/20190126163820/https://www.mimuw.edu.pl/~nguyen/least.pdf. 32. English.