计算机科学家逻辑/模态逻辑/语法

语法

我们假设上述章节中使用的经典命题逻辑的语法。此外，我们还有以下两条规则：如果 $A$ 是一个公式

${\begin{matrix}&&\diamond A{\mbox{ and}}\\&&\square A\end{matrix}}$

是公式。

符号 $\diamond$ 和 $\Box$ 传统上代表可能性和必要性；在时态逻辑的语境中，它们代表总是和最终，因此 $\diamond A$ 代表$A$ 最终为真，而 $\Box A$ 代表$A$ 总是为真。