Modal depth

In modal logic, the modal depth of a formula is the deepest nesting of modal operators (commonly $\Box$ and $\Diamond$). Modal formulas without modal operators have a modal depth of zero.

Definition

Modal depth can be defined as follows. Let MD(ϕ) be a function that computes the modal depth for a modal formula ϕ:

MD(p) = 0, where p is an atomic formula.

$MD(\top) = 0$

$MD(\bot) = 0$

$MD(\neg \varphi) = MD(\varphi)$

$MD(\varphi \wedge \psi) = max(MD(\varphi), MD(\psi))$

$MD(\varphi \vee \psi) = max(MD(\varphi), MD(\psi))$

$MD(\varphi \rightarrow \psi) = max(MD(\varphi), MD(\psi))$

$MD(\Box \varphi) = 1 + MD(\varphi)$

$MD(\Diamond \varphi) = 1 + MD(\varphi)$

Example

The following computation gives the modal depth of $\Box ( \Box p \rightarrow p )$:

$MD(\Box ( \Box p \rightarrow p )) =$

$1 + MD( \Box p \rightarrow p) =$

$1 + max(MD(\Box p), MD(p)) =$

1 + max(1 + MD(p),0) =

1 + max(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 \models \Diamond \Diamond \varphi$, one needs to check whether there exists an accessible world v for which $M, v \models \Diamond \varphi$. If that is the case, one needs to check whether there is also a world u such that $M, u \models \varphi$ 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., $\Box \varphi$ holds for all φ in a world w when $\forall v \in W \ (w, v) \not \in R$, where W is the set of worlds and R is the accessibility relation). To check whether $M, w \models \Box \Box \varphi$, 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.

This logic-related article is a stub. You can help Wikipedia by expanding it.v · Categories: Logic stubs Modal logic Wikimedia Foundation. 2010. Игры ⚽ Поможем написать реферат Modal Soul Classics II Modal fictionalism Look at other dictionaries: Modal companion — In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic which interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate… …   Wikipedia Method of analytic tableaux — A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau (or truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulas of first order logic. The… …   Wikipedia Natural deduction — In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the natural way of reasoning. This contrasts with the axiomatic systems which instead use… …   Wikipedia Existential graph — An existential graph is a type of diagrammatic or visual notation for logical expressions, proposed by Charles Sanders Peirce, who wrote his first paper on graphical logic in 1882 and continued to develop the method until his death in 1914.The… …   Wikipedia igneous rock — Any of various crystalline or glassy, noncrystalline rocks formed by the cooling and solidification of molten earth material (magma). Igneous rocks comprise one of the three principal classes of rocks, the others being metamorphic and sedimentary …   Universalium Singing — Sings and Vocals redirect here. For other uses, see Sings (disambiguation) and Vocals (disambiguation). Singer redirects here. For other uses, see Singer (disambiguation). Harry Belafonte 1954 Singing is the act of producing musical sounds with… …   Wikipedia railroad — /rayl rohd /, n. 1. a permanent road laid with rails, commonly in one or more pairs of continuous lines forming a track or tracks, on which locomotives and cars are run for the transportation of passengers, freight, and mail. 2. an entire system… …   Universalium jazz — jazzer, n. /jaz/, n. 1. music originating in New Orleans around the beginning of the 20th century and subsequently developing through various increasingly complex styles, generally marked by intricate, propulsive rhythms, polyphonic ensemble… …   Universalium Islamic arts — Visual, literary, and performing arts of the populations that adopted Islam from the 7th century. Islamic visual arts are decorative, colourful, and, in religious art, nonrepresentational; the characteristic Islamic decoration is the arabesque.… …   Universalium Preclinical imaging — is the visualization of animals for research purposes, such as drug development. Imaging modalities have long been crucial to the researcher in observing changes, either at the organ, tissue, cell, or molecular level, in animals responding to… …   Wikipedia 18+ © Academic, 2000-2024 Contact us: Technical Support, Advertising Dictionaries export, created on PHP, Joomla, Drupal, WordPress, MODx. Mark and share Search through all dictionaries Translate… Search Internet Share the article and excerpts Direct link … Do a right-click on the link above and select “Copy Link”