窗口运算符

在模态逻辑中，窗口运算符△{displaystyle{triangle}是一个模态算子，其语义定义如下是一个模态算子，其语义定义如下。{displaystyleM=(W,R,f)}为Kripke模型。

一个克里普克模型和w,u∈W{displaystylew,u∈W}是一个Kripke模型，w,u∈W是一个Kripke模型。.非正式地，它说w看到了每个φ世界（或者每个φ世界都被w看到）。

这个算子在基本的模态逻辑中是无法定义的（即一些命题的非模态语言加上一个原始的必然性（普遍性）算子，通常用’◻{displaystyle/square}，或其存在的对等物，即”◻”。’，或者它的存在性对偶，通常表示为’◊{displaystyleDiamond}）。’).注意，它的真值条件是标准必然性算子的真值条件的反面。