In modal logic, the window operator <math>\triangle</math> is a modal operator with the following semantic definition: <math>M,w\models\triangle\phi \iff \forall u, M,u\models\phi\Rightarrow Rwu</math> for <math>M=(W,R,f)</math> a model and <math>w,u\in W</math>. 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.

PropertyValue
dbpprop:abstract
  • In modal logic, the window operator <math>\triangle</math> is a modal operator with the following semantic definition: <math>M,w\models\triangle\phi \iff \forall u, M,u\models\phi\Rightarrow Rwu</math> for <math>M=(W,R,f)</math> a model and <math>w,u\in W</math>. 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" operator, often denoted by '<math>\square</math>', or its existential dual, often denoted by '<math>\Diamond</math>'). 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.
rdfs:comment
  • In modal logic, the window operator <math>\triangle</math> is a modal operator with the following semantic definition: <math>M,w\models\triangle\phi \iff \forall u, M,u\models\phi\Rightarrow Rwu</math> for <math>M=(W,R,f)</math> a model and <math>w,u\in W</math>. 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.
rdfs:label
  • Window operator
owl:sameAs
skos:subject
foaf:page