Window operator

In modal logic, the window operator \triangle is a modal operator with the following semantic definition in the language of predicate logic: M,w\models\triangle\phi \iff \forall u, M,u\models\phi\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 ' \square ', or its existential dual, often denoted by ' \Diamond '). 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 satisfy phi, which secures phi as a minimum condition to be accessible. For references to some of its applications, see the References section.

In modal logic, the window operator \triangle is a modal operator with the following semantic definition in the language of predicate logic: M,w\models\triangle\phi \iff \forall u, M,u\models\phi\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 ' \square ', or its existential dual, often denoted by ' \Diamond '). 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 satisfy phi, which secures phi as a minimum condition to be accessible. For references to some of its applications, see the References section.

Text derived from https://en.wikipedia.org/w/index.php?oldid=1378066600 under CC BY-SA 4.0; modifications have been made.