Modal depth

In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly formula_1 and formula_2). Modal formulas without modal operators have a modal depth of zero.
Definition.
Modal depth can be defined as follows. Let formula_3 be a function that computes the modal depth for a modal formula formula_4:
Example.
The following computation gives the modal depth of formula_15:
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 formula_22, one needs to check whether there exists an accessible world formula_23 for which formula_24. If that is the case, one needs to check whether there is also a world formula_25 such that formula_26 and formula_25 is accessible from formula_23. We have made two steps from the world formula_29 (from formula_29 to formula_23 and from formula_23 to formula_25) 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., formula_34 holds for all formula_35 in a world formula_29 when formula_37, where formula_38 is the set of worlds and formula_39 is the accessibility relation). To check whether formula_40, 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 formula_29; the formula now trivially holds by the previous observation about the validity of formulas with a box as outer operator.