In modal logic, the window operator △ is a modal operator with the following semantic definition:
M , w ⊨ △ ϕ ⟺ ∀ u , M , u ⊨ ϕ ⇒ R w u
for M = ( W , R , f ) a Kripke model and w , u ∈ 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 ' ◻ ', 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.
