词条 | Modal depth |
释义 |
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. DefinitionModal depth can be defined as follows.[1] Let be a function that computes the modal depth for a modal formula : , where is an atomic formula. ExampleThe following computation gives the modal depth of : Modal depth and semanticsThe 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. References{{ reflist }} 1 : Modal logic |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。