Window operator

From Wikipedia, the free encyclopedia

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

$M,w\models\triangle\phi \iff \forall u, M,u\models\phi\Rightarrow Rwu$

for $M = (W, R, f)$ a model and $w,u\in 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.