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. This operator is not definable in the basic modal logic. 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.
