In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly ◻ and ◊ ). Modal formulas without modal operators have a modal depth of zero.
Modal depth can be defined as follows. Let M D ( ϕ ) be a function that computes the modal depth for a modal formula ϕ :
M D ( p ) = 0 , where
p is an
atomic formula.
M D ( ⊤ ) = 0 M D ( ⊥ ) = 0 M D ( ¬ φ ) = M D ( φ ) M D ( φ ∧ ψ ) = m a x ( M D ( φ ) , M D ( ψ ) ) M D ( φ ∨ ψ ) = m a x ( M D ( φ ) , M D ( ψ ) ) M D ( φ → ψ ) = m a x ( M D ( φ ) , M D ( ψ ) ) M D ( ◻ φ ) = 1 + M D ( φ ) M D ( ◊ φ ) = 1 + M D ( φ ) The following computation gives the modal depth of ◻ ( ◻ p → p ) :
M D ( ◻ ( ◻ p → p ) ) = 1 + M D ( ◻ p → p ) = 1 + m a x ( M D ( ◻ p ) , M D ( p ) ) = 1 + m a x ( 1 + M D ( p ) , 0 ) = 1 + m a x ( 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 ⊨ ◊ ◊ φ , one needs to check whether there exists an accessible world v for which M , v ⊨ ◊ φ . If that is the case, one needs to check whether there is also a world u such that M , u ⊨ φ 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., ◻ φ holds for all φ in a world w when ∀ v ∈ W ( w , v ) ∉ R , where W is the set of worlds and R is the accessibility relation). To check whether M , w ⊨ ◻ ◻ φ , 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.
