Intuition

Modes of Truth: 命题逻辑和谓词逻辑不允许真/假之外的可能性，然而自然语言允许。例如“永远为真”“知道为真”“相信为真”。LTL 和 CTL 就是这样的，它们是 Modal Logic 的特例。又例如对于交互式的 agent 来说，模态逻辑是一种帮助我们形式化的方法。

Our main case study will be the logic of knowledge in a multi-agent system.

Syntax

简单将谓词逻辑（即 First-Order Logic）的存在/任意，替换成 box $\Box$ 和 diamond $\Diamond$。

Semantics

模态逻辑的模型为一个 4-tuple $\mathcal{M}=(W,R,AP,L)$：

• 集合 $W$, 其中元素称为“世界”（这个称呼很怪，不知道是不是翻译问题，第一反应“一花一世界”）（如果称呼 $W$ 为宇宙 universe 或许说得通，事实上 Ebbinghaus 的一阶逻辑中就是这么做的）
• $R\subset W\times W$ 可达关系
• $AP$ 原子命题
• $L:W\mapsto \mathcal{P}(AP)$ 标识函数

这里 $R$ 只是一个普通的子集，因此只能看作有向图，如果 $R(x,y)$ 那么称 $y$ 为一个可达世界.

可满足性的定义：$\mathcal{M}=(W,R,L)$, $x\in W$

• $x\vdash \top$
• $x\not\vdash \bot$
• $x\vdash p\iff p\in L(x)$
• not and or imply iff 和 FO 一样
• $x\vdash p\iff p\in L(x)$
• $x\vdash \Box\psi\iff\text{for all } y\in W,\;\neg R(x,y)\text{ or } y\vdash\psi$
• $x\vdash \Diamond\psi\iff\text{there exists } y\in W,\;R(x,y)\text{ and } y\vdash\psi$

一些边界情况

如果 $x$ 没有可达世界，那么 $\forall\phi,\; x\vdash\Box\phi$ 且 $x\not\vdash\Diamond\phi$. 这里的 $\phi$ 也包括 $\top$ 和 $\bot$.