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.
Definition
Modal depth can be defined as follows. Let
be a function that computes the modal depth for a modal formula
:
, where
is an atomic formula.
![{\displaystyle MD(\top )=0}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3ef0ea07a0b4729acc48ca57e5fd15c707e70a50)
![{\displaystyle MD(\bot )=0}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ce38c16d7895a1cc05d2c215fa56a1a29566093f)
![{\displaystyle MD(\neg \varphi )=MD(\varphi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3dc69a8b304f875e171af7a9f9724c111f7337f6)
![{\displaystyle MD(\varphi \wedge \psi )=max(MD(\varphi ),MD(\psi ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84540dfc3d15e7cb4415b88ecef1b67cf0e1b898)
![{\displaystyle MD(\varphi \vee \psi )=max(MD(\varphi ),MD(\psi ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d83f24dc016dcafe6fae8f9dfe8d7ba6d1ceeaf2)
![{\displaystyle MD(\varphi \rightarrow \psi )=max(MD(\varphi ),MD(\psi ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c7fe963a5ff3da36e621150ec935d47faa20513e)
![{\displaystyle MD(\Box \varphi )=1+MD(\varphi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f29c3c3b03d56e9c9390e6af70e374554e64e9a)
![{\displaystyle MD(\Diamond \varphi )=1+MD(\varphi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9cd58195eed4d45daab98683cc3818f58c765302)
Example
The following computation gives the modal depth of
:
![{\displaystyle MD(\Box (\Box p\rightarrow p))=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8e8cac267a3d5420a27645167d9396891f06922a)
![{\displaystyle 1+MD(\Box p\rightarrow p)=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/38e02fa2f28591d5bb62d1206c38b5212d9157b2)
![{\displaystyle 1+max(MD(\Box p),MD(p))=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/90707f6102d3db274e0caaf7a3816c2d28127e21)
![{\displaystyle 1+max(1+MD(p),0)=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/abc38381a7cb406d600a198f60dc1ed36d44e36e)
![{\displaystyle 1+max(1+0,0)=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a55096d9f3b401351c566b3639ad580e8bfdf420)
![{\displaystyle 1+1=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/58ad5a3978466f6e4ec43ca6f31d6fe978202c17)
- 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
, one needs to check whether there exists an accessible world
for which
. If that is the case, one needs to check whether there is also a world
such that
and
is accessible from
. We have made two steps from the world
(from
to
and from
to
) 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
when
, where
is the set of worlds and
is the accessibility relation). To check whether
, 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
; the formula now trivially holds by the previous observation about the validity of formulas with a box as outer operator.