Window operator

In modal logic, the window operator $riangle$ is a modal operator with the following semantic definition:

$M,wmodels\; rianglephi\; iff\; forall\; u,\; M,umodelsphiRightarrow\; Rwu$

for $M=(W,R,f)$ a model and $w,uin\; W$. 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 '$square$', or its existential dual, often denoted by '$Diamond$'). 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. "Modal Logic". Cambridge University Press, 2002.