Window operator

In modal logic, the window operator formula_1 is a modal operator with the following semantic definition:
formula_2
for formula_3 a Kripke model and formula_4. 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 'formula_5', or its existential dual, often denoted by 'formula_6'). 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.