In modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

, the modal depth of a formula is the deepest nesting of modal operator

Modal operator

In modal logic, a modal operator is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional, and is "intuitively" characterised by expressing a modal attitude about the proposition to which the operator is applied...

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 (mathematics)

In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...

 that computes the modal depth for a modal formula :
, where is an atomic formula

Atomic formula

In mathematical logic, an atomic 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 subformulas. Atoms are thus the simplest well-formed formulas of the logic...

.

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 when checking the validity

Validity

In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....

 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

Accessibility relation

In modal logic, an accessibility relation is a binary relation, written as R\,\! between possible worlds.-Description of terms:A statement in logic refers to a sentence that can be true or false...

. 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.