Modal Logic

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$ .

因此有一些反直觉：例如对于没有可达世界的 $x$ , $x\vdash\Box\bot$ . 但是仔细想还是能理解，因为任意 $y$ 都满足 $\neg R(x,y)$ .

Equivalence

要求对任何模型中的任何世界 $x$ , 如果 $(\forall\phi\in\Gamma,\;x\vdash\phi)\implies x\vdash\psi$ , 那么定义 $\Gamma\vdash\psi$ .

等价的意思是 $\{\phi\}\vdash\psi$ 且 $\{\psi\}\vdash\phi$ . $\{\}$ 可以去掉.

考虑分配律和 De Moegan 律， $\Box\Diamond$ 和 $\forall\exists$ 很相像，这里省略.

回到上面说的边界情况，我们得到 $\Box\phi\not\equiv\Diamond\phi$ . 然而我们有 $\Box\top\equiv\top$ 和 $\Diamond\bot\equiv\bot$ . 前者很显然，而后者有点费解，稍微证明一下.

Pf. of $\Diamond\bot\equiv\bot$ :

首先没有 $x$ 满足 $\bot$ , 有 $\bot\vdash\Diamond\bot$ . 反过来如果 $x\vdash\Diamond\bot$ , 那么存在一个 $x$ 的可达世界 $y\vdash\bot$ , 没有这样的 $x$ , 就算 $x$ 没有后继也不存在. 双向奔赴了属于是. $\blacksquare$

还有一个有趣的等价 $\Diamond\top\equiv\Box\phi\to\Diamond\phi$ , 证明显然，对任意 $\phi$ 成立.

类似一阶逻辑，模态逻辑也有 validity，定义为对任意模型、任意世界都成立，记作 $\vdash\phi$ .

$\vdash\neg\Box\phi\leftrightarrow\Diamond\neg\phi$ $\vdash\neg\Diamond\phi\leftrightarrow\Box\neg\phi$

还有一个有趣的有效公式 $K:\Box(\phi\to\psi)\to(\Box\phi\to\Box\psi)$ .

Logic engineering

逻辑工程的部分工作是确定什么样的公式模式一共有效，并且勾勒出恰好使这些公式为有效的逻辑.

Validity

上面我们全部的表述都是基本模态逻辑的框架，为了适应之前所说的复杂情况，需要 re-engineer 这些基本模态逻辑. 书上的表述为

As modal logic automatically gives us the connective $\Diamond$ ,which is equivalent to $\neg\Box\neg$ , we can find out what the corresponding readings of in our system will be.

说实话，我不知道怎么就 automatically 了；不如接受这个约定，带入自然语言：

“未来总是真”对应右边“并非未来总是假”，也就是“未来存在真”；“理应为真”其实是“不允许为假”，那么就对应右边“允许为真”（这里反着绕了一下）；“相信 $\phi$ 为真”对应右边“不相信 $\phi$ 为假”，假设 Q 有一个“信念”的集合，那么 $\neg\phi$ 不在这个集合中，也就是说， $\phi$ 不和 Q 的信念矛盾，即 consistent；“知道为真”对应“不知道为假”，也就是说， $\phi$ 不和 Q 的知识矛盾，但是 Q 可能知道 $\phi$ , 也可能知道 $\neg\phi$ .

p.s. 写这一段的时候想到了情态动词（modal verb）；看看标题！

除了最后三列都和基本模态逻辑相同，其他都需要讨论一下（另外发现 $\Box$ 和 $\Diamond$ 在45°排版中互换）。不过有些很费解就是了。

Accessibility Relation and Correspondence

这一部分，我们从 $\Box\Diamond$ 的自然语言语义出发，重新回顾 $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$ 这两个形式化定义。

首先重新为 $R$ 建模.

我们发现上面两个形式化定义与 $R$ 的性质非常相关。例如，如果 $\Box$ 表示“未来总是真”，根据 Table5.7 我们有一个合理的建模，其中 $\Box\phi\to\Box\Box\phi$ . 注意到这个逻辑仅仅添加了一条 valid 公式模式（ $\Box\phi\to\Box\Box\phi$ ）. 同时观察到根据 Table 5.8, 这时候的 $R$ 具有了传递性.

一个直觉：对 $\Box$ 的不同解读, 有不同的 validity 公式模式， $R$ 也有不同的性质（我们最开始认为 $R$ 是一个普通的二元关系）.

这里我们为了考察 $R$ 的性质，定义标架 $\mathcal{F}=(W,R,AP)$ （注意之前我们定义“有效”的时候，用的是“任意模型的任何世界”，这里我们将自由度减少，固定了模型中的前两个参数 $W,R$ ）, 称 $\mathcal{F}\vdash\phi$ 当且仅当 $\forall w\in W, L:W\mapsto\mathcal{P}(AP)$ , $\mathcal{M}=(W,R,AP,L),w\vdash\phi$ 成立.

定理. 给定 $\mathcal{F}=(W,R,AP)$ , $R$ 是自反的当且仅当 $\mathcal{F}$ 使 $\Box\phi\to\phi$ 有效.

证明. 如果对任意 $w\in W$ , $R(w,w)$ , 假设 $x\vdash\Box\phi$ , 那么对任意可达世界 $y$ , $y\vdash\phi$ , 其中也包括 $w$ ; 如果 $\vdash_{\mathcal{F}}\Box\phi\to\phi$ , 反设存在 $x\in W$ such that $\neg R(x,x)$ . 那么存在一个标识函数 $L$ 使得 $\phi\not\in L(x)$ ，且对任意其他的 $y$ , $\phi\in L(y)$ . 由于除了 $x$ 其他都满足 $\phi$ , 因此 $x\vdash\Box\phi$ ; 矛盾. $\blacksquare$

name	formula scheme	property of R	definition
K	$\Box\phi\land\Box(\phi\to\psi)$ $\to\Box\psi$	none
T	$\Box \phi \rightarrow \phi$	reflexive	$\forall x \in W,$ $\;R(x,x)$
B	$\phi \rightarrow \Box \Diamond \phi$	symmetric	$\forall x, y \in W,$ $\;R(x,y)\implies R(y,x)$
D	$\Diamond\top\equiv\Box \phi \rightarrow \Diamond \phi$	serial	$\forall x,\;\exists y$ $\;\text{s.t. }R(x,y)$
4	$\Box \phi \rightarrow \Box \Box \phi$	transitive	$\forall x, y, z \in W$ , $R(x,y)\land R(y,z)$ $\implies R(x,z)$
5	$\Diamond \phi \rightarrow \Box \Diamond \phi$	Euclidean	$\forall x, y, z \in W,$ $\;R(x,y)\land R(x,z)$ $\implies R(y,z)$
	$\Box \phi \leftrightarrow \Box \phi$	functional	$\forall x,\;\exists! y\;R(x,y)$
	$\Box(\phi \land \Box \phi \rightarrow \psi) \lor$ $\Box(\psi \land \Box \psi \rightarrow \phi)$	linear	$\forall x, y, z \in W$ , $R(x,y)\land R(y,z)\implies$ $R(y,z)\lor y=z\lor R(z,y)$

p.s. 以上 scheme 和 property 都是当且仅当关系，而且有 Euclidean $\to$ linear

KT45 logic: $\mathbb{L}=\{$ T,4,5 $\}$

最开始我们介绍的就是 K logic: $\mathbb{L}=\varnothing$

KT45 逻辑经常用来建模知识推理，这与 Table 5.7 相呼应；这里 4 代表如果 Q 知道某为真，那么知道自己知道它为真；5 代表如果 Q 不知道某为假，那么知道自己不知道它为假. 称为正反省和负反省（实际上没人能做到，理想化建模；后面我们可以看到这种建模对应的是逻辑游戏中“所有人都拥有足够智慧”的假设）.

然而注意到，“knows”这一行其实除了 T,4,5 还有 D. 事实上 $D$ 可以直接由 $T$ 推出：前提是 $\Box\phi$ , 反设 $\Box\neg\phi$ , 根据 T，直接推出 $\phi$ 和 $\neg\phi$ , 矛盾. 因此有 $\neg\Box\neg\phi=\Diamond\phi$ .

如果放在二元关系这里，更简单：如果 $R(x,x)$ , 那么每个 $x$ 一定存在自己的可达世界，就是自己.

注意到从 KT45 也可以推出 B, 直观上说，如果 $\phi$ 为真，那么我可以知道我不知道 $\neg\phi$ . 反设 $\Box\neg\phi$ , 由 T 得 $\neg \phi$ , 矛盾. 因此 $\Diamond\phi$ . 由 5 得 $\Box\Diamond\phi$ .

因此 KT45 对应的二元关系应该也是对称的，因为 $R(x,y)\land R(x,x)$ 可以推出 $R(y,x)$ .

总之 KT45 对应的二元关系就变成等价关系了. 书上说（待证明，而且我感觉很奇怪，比如一长串 $\Box$ 怎么等价？）

KT4 Logic: $\mathbb{L}=\{$ T,4 $\}$

这个逻辑和程序语义、直觉主义逻辑有一些联系，不细说了.

Natural Deduction

Going into a dashed box means reasoning in an arbitrary accessible world.

Wherever $\phi$ occurs in a proof, $\phi$ may be put into a subsequent dashed box. Wherever $\psi$ occurs at the end of a dashed box, $\psi$ may be put after that dashed box.

KT45$^n$

对 KT45 做推广，扔掉 $\Diamond$ , 改写 $\Box$ , 得到 KT45$^n$. 其中 $K_i\phi$ 表示 agent $Q_i$ 知道 $\phi$ .

KT45$^n$ 的一个模型是一个四元组 $\mathcal{M}=(W,(R_i)_{i\in\mathcal{A}},AP,L)$ ：

根据 $K_i$ 可以扩展定义.

$x\vdash E_G\phi$ 当且仅当 $\forall i\in G$ , $x\vdash K_i\phi$ .
$x\vdash C_G\phi$ 当且仅当 $\forall k\geq1$ , $x\vdash E_G^k\phi$ .
$x\vdash D_G\phi$ 当且仅当 $\forall y,$ $(\forall i\in G,R_i(x,y))\implies y\vdash\phi$ .

后面大概率用不到 $D$ , 因此略过.

Some valid formulas

modus ponens

redefinition of relations

注意为什么 $R_{E_G}$ 用 for some 定义？因为这个 relation 适用于 $x\vdash E_G\phi\iff \forall i,\;\forall y\text{ s.t. }R_i(x,y),\;y\vdash\phi\iff\forall y\text{ s.t. }R_{E_G}(x,y),\;y\vdash\phi$ . 这样 $R_{E_G}$ 的确要包括所有的 $i$ . $R_{D_G}$ 同理.