Window operator
In modal logic, the window operator is a modal operator with the following semantic definition:
for a Kripke model and
. Informally, it says that w "sees" every φ-world (or every φ-world is seen by w). This operator is not definable in the basic modal logic (i.e. some propositional non-modal language together with a single primitive "necessity" (universal) operator, often denoted by '
', or its existential dual, often denoted by '
'). Notice that its truth condition is the converse of the truth condition for the standard "necessity" operator.
For references to some of its applications, see the References section.
References
- Blackburn, P; de Rijke, M; Venema, Y (2002). Modal Logic. Cambridge University Press.
This article is issued from Wikipedia - version of the Monday, October 04, 2010. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.