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.
