Modal depth

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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.


Modal depth can be defined as follows. 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 \rightarrow \psi) = max(MD(\varphi), MD(\psi))
MD(\Box \varphi) = 1 + MD(\varphi)
MD(\Diamond \varphi) = 1 + MD(\varphi)


The following computation gives the modal depth of \Box ( \Box p \rightarrow p ):

MD(\Box ( \Box p \rightarrow p )) =
1 + MD( \Box p \rightarrow p) =
1 + max(MD(\Box p), MD(p)) =
1 + max(1 + MD(p), 0) =
1 + max(1 + 0, 0) =
1 + 1 =

Modal depth and semantics[edit]

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.