Philosophy:Window operator

Short description: Operator in modal logic

In modal logic, the window operator $\mathrm{△}$ is a modal operator with the following semantic definition in the language of predicate logic:

$M,w\models \mathrm{△}\varphi ⟺\mathrm{\forall }u,M,u\models \varphi \Rightarrow Rwu$

for $M=(W,R,f)$( a Kripke model) and $w,u\in W$(The following can be read as "The satisfiability of the window operator delta applied to phi in a world w for Model m is only met if for all u, if phi is satisfied for a world u in model M, then w is related to u.)

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(which make sure cases satisfying phi are within accessible realms, which sets a possible upper bound for phi ) is the converse of the truth condition for the standard "necessity" operator because necessity operators are about making sure all accessible worlds satisfies phi, which secures phi as a minimum condition to be accessible.

For references to some of its applications, see the References section.

References

• Blackburn, P; de Rijke, M; Venema, Y (2002). Modal Logic. Cambridge University Press.