Window operator explained
In modal logic, the window operator
is a
modal operator with the following
semantic definition:
M,w\models\triangle\phi\iff\forallu,M,u\models\phi ⇒ Rwu
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
- Book: Blackburn. P. de Rijke. M. Venema. Y. Modal Logic. Cambridge University Press. 2002.
