In
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
, the modal depth of a formula is the deepest nesting of
modal operator
A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional in the following sen ...
s (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
Function or functionality may refer to:
Computing
* Function key, a type of key on computer keyboards
* Function model, a structured representation of processes in a system
* Function object or functor or functionoid, a concept of object-oriente ...
that computes the modal depth for a modal formula
:
:
, where
is an
atomic formula
In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
.
:
:
:
:
:
:
:
:
Example
The following computation gives the modal depth of
:
:
:
:
:
:
:
Modal depth and semantics
The modal depth of a formula indicates 'how far' one needs to look in a
Kripke model
Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...
when checking the
validity
Validity or Valid may refer to:
Science/mathematics/statistics:
* Validity (logic), a property of a logical argument
* Scientific:
** Internal validity, the validity of causal inferences within scientific studies, usually based on experiments
** ...
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
An accessibility relation is a relation which plays a key role in assigning truth values to sentences in the relational semantics for modal logic. In relational semantics, a modal formula's truth value at a ''possible world'' w can depend on w ...
. 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.
References
{{ reflist
Depth