计算机科学家逻辑/模态逻辑/翻译方法

翻译方法

有几种方法旨在将命题模态逻辑翻译成一阶谓词逻辑。这个想法是，将可达性的语义条件转化为逻辑公式：语义定义的一条规则是

w\models \Box A\;\;{\mbox{ iff }}{\mbox{for all }}v\in W,(w,v)\not \in R{\mbox{ or }}v\models A

这可以通过用一阶公式 $\forall yR(x,y)\to P'(y)$ 替换模态公式 $\square P$ 来编译成公式。因此，我们可以通过引入一阶翻译来消除所有模态运算符。这种翻译的结果是一个经典的一阶公式，可以用我们之前看到的方法来处理。

对于一个模态公式 $F$ ，我们定义它的翻译 $F^{*}$

$P^{*}=P(x)$ ，如果 $P$ 是一个命题常量
$(\lnot F)^{*}=\lnot (F)$
$(F\land G)^{*}=(F^{*}\land G^{*})$
$(\square F)^{*}=(\forall y(R(x,y)\to F^{*}(x/y)))$ ，其中 $y$ 是一个在 $F^{*}$ 中不出现的新的变量，而 $F^{*}(x/y)$ 是用 $y$ 替换 $F^{*}$ 中所有 $x$ 的自由出现的结果。

因此，我们有

F 是 $K$ 中的一个有效的模态公式，当且仅当 $F^{*}$ 是一个有效的的一阶公式。

结合这样一个观察：在模态逻辑 $K$ 中（像许多其他模态逻辑一样）有效性是可判定的，我们因此得到一个可判定的经典一阶谓词逻辑的子逻辑！模态逻辑可以被视为二元一阶逻辑 $FO^{2}$ 的一个片段。