Philosophy:Modal depth

Short description: Modal logic term

In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly [math]\displaystyle{ \Box }[/math] and [math]\displaystyle{ \Diamond }[/math]). Modal formulas without modal operators have a modal depth of zero.

Definition

Modal depth can be defined as follows. Let [math]\displaystyle{ MD(\phi) }[/math] be a function that computes the modal depth for a modal formula [math]\displaystyle{ \phi }[/math]:

[math]\displaystyle{ MD(p) = 0 }[/math], where [math]\displaystyle{ p }[/math] is an atomic formula.

[math]\displaystyle{ MD(\top) = 0 }[/math]

[math]\displaystyle{ MD(\bot) = 0 }[/math]

[math]\displaystyle{ MD(\neg \varphi) = MD(\varphi) }[/math]

[math]\displaystyle{ MD(\varphi \wedge \psi) = max(MD(\varphi), MD(\psi)) }[/math]

[math]\displaystyle{ MD(\varphi \vee \psi) = max(MD(\varphi), MD(\psi)) }[/math]

[math]\displaystyle{ MD(\varphi \rightarrow \psi) = max(MD(\varphi), MD(\psi)) }[/math]

[math]\displaystyle{ MD(\Box \varphi) = 1 + MD(\varphi) }[/math]

[math]\displaystyle{ MD(\Diamond \varphi) = 1 + MD(\varphi) }[/math]

Example

The following computation gives the modal depth of [math]\displaystyle{ \Box ( \Box p \rightarrow p ) }[/math]:

[math]\displaystyle{ MD(\Box ( \Box p \rightarrow p )) = }[/math]

[math]\displaystyle{ 1 + MD( \Box p \rightarrow p) = }[/math]

[math]\displaystyle{ 1 + max(MD(\Box p), MD(p)) = }[/math]

[math]\displaystyle{ 1 + max(1 + MD(p), 0) = }[/math]

[math]\displaystyle{ 1 + max(1 + 0, 0) = }[/math]

[math]\displaystyle{ 1 + 1 =:2 }[/math]

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 [math]\displaystyle{ M, w \models \Diamond \Diamond \varphi }[/math], one needs to check whether there exists an accessible world [math]\displaystyle{ v }[/math] for which [math]\displaystyle{ M, v \models \Diamond \varphi }[/math]. If that is the case, one needs to check whether there is also a world [math]\displaystyle{ u }[/math] such that [math]\displaystyle{ M, u \models \varphi }[/math] and [math]\displaystyle{ u }[/math] is accessible from [math]\displaystyle{ v }[/math]. We have made two steps from the world [math]\displaystyle{ w }[/math] (from [math]\displaystyle{ w }[/math] to [math]\displaystyle{ v }[/math] and from [math]\displaystyle{ v }[/math] to [math]\displaystyle{ u }[/math]) 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., [math]\displaystyle{ \Box \varphi }[/math] holds for all [math]\displaystyle{ \varphi }[/math] in a world [math]\displaystyle{ w }[/math] when [math]\displaystyle{ \forall v \in W \ (w, v) \not \in R }[/math], where [math]\displaystyle{ W }[/math] is the set of worlds and [math]\displaystyle{ R }[/math] is the accessibility relation). To check whether [math]\displaystyle{ M, w \models \Box \Box \varphi }[/math], 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 [math]\displaystyle{ w }[/math]; the formula now trivially holds by the previous observation about the validity of formulas with a box as outer operator.