计算机科学家逻辑/模态逻辑/公理化

公理化

最简单的模态逻辑称为 $K$，由以下公理给出

• 所有经典重言式（及其替换）
• 模态公理：所有形式为 $\square (X\to Y)\to (\square X\to \square Y)$ 的公式

以及推理规则

• 肯定前件规则：从 $X$ 和 $X\to Y$ 推导出 $Y$
• 必然性规则：从 $X$ 推导出 $\square X$

从公式集 $S$ 推导出 $X$ 的 $K$ 推导是一个公式序列，以 $X$ 结束，其中每个公式都是 $K$ 的公理、$S$ 的成员，或者通过应用推理规则从前面的项推导出来。\defined{$K$ 证明} $X$ 是一个从 $\emptyset$ 推导出 $X$ 的 $K$ 推导。

举个例子，考虑 $K$ 对 $(\square P\land \square Q)\to \square (P\land Q)$ 的证明

${\begin{matrix}&{\mbox{Tautology: }}&P\to (Q\to (P\land Q))\\&{\mbox{Necessitation: }}&\square (P\to (Q\to (P\land Q)))\\&{\mbox{Modal axiom:}}&\square (P\to (Q\to (P\land Q)))\to (\square P\to \square (Q\to (P\land Q)))\\&{\mbox{Modus ponens: }}&\square P\to \square (Q\to (P\land Q))\\&{\mbox{Modal axiom:}}&\square (Q\to (P\land Q))\to (\square Q\to \square (P\land Q))\\&{\mbox{Classical arg: }}&\square P\to (\square Q\to \square (P\land Q))\\&{\mbox{Classical arg: }}&(\square P\land \square Q)\to \square (P\land Q)\\\end{matrix}}$

这个蕴含的逆命题也有类似的证明；因此在 $K$ 中我们有

$\square (P\land Q)\leftrightarrow (\square P\land \square Q)$

注意，对析取的分配律不成立！（为什么？）

K 的扩展

从模态逻辑 $K$ 开始，我们可以添加额外的公理，从而得到不同的逻辑。我们列出以下基本公理
$K$ : $\square (X\to Y)\to (\square X\to \square Y)$

$T$ : $\square A\to A$

$D$ : $\square A\to \diamond A$

$4$ : $\square A\to \square \square A$

$5$ : $\diamond A\to \square \diamond A$

$B$ : $A\to \square \diamond A$

传统上，如果在逻辑 $K$ 中添加公理 $A_{1},\cdots ,A_{n}$，我们称得到的逻辑为 $KA_{1}\cdots A_{n}$。然而，有时这个逻辑非常有名，以至于被另一个名字称呼；例如 $KT4$ 被称为 $S4$。

这些逻辑也可以用某些框架类来刻画，因为已知特定的公理对应于可达性关系 $R$ 上的特定限制。如果 $\langle W,R\rangle$ 是一个框架，那么某个公理在 $\langle W,R\rangle$ 上有效，当且仅当 $R$ 满足某个限制。一些限制可以通过一阶逻辑公式来表达，其中二元谓词 $R(x,y)$ 表示可达性关系

${\begin{matrix}T:&{\mbox{Reflexive}}&\forall w{\text{:}}R(w,w)\\D:&{\mbox{Serial}}&\forall w\exists w':R(w,w')\\4:&{\mbox{Transitive}}&\forall s,t,u:(R(s,t)\land R(t,u))\to R(s,u)\\5:&{\mbox{Euclidean}}&\forall s,t,u:(R(s,t)\land R(s,u))\to R(t,u)\\B:&{\mbox{Symmetric}}&\forall w,w':R(w,w')\to R(w',w)\end{matrix}}$