計算機科學家邏輯/模態邏輯/翻譯方法

翻譯方法

有幾種方法旨在將命題模態邏輯翻譯成一階謂詞邏輯。這個想法是，將可達性的語義條件轉化為邏輯公式：語義定義的一條規則是

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}$ 的一個片段。