計算機科學家邏輯/模態邏輯/模態邏輯 tableaux

模態邏輯 tableaux

在經典命題邏輯中，我們為邏輯 $L$ 引入了一個 tableaux 演算（定義），它是一個有限分支樹，其節點來自 $L$ 的公式。給定一個來自 $L$ 的公式集 $\Phi$，$\Phi$ 的 tableaux 是透過對 tableaux 規則模式進行（可能無限）的序列應用來構建的

$\rho {\frac {\psi }{D_{1}\mid D_{2}\mid \cdots \mid D_{n}}}$

前提是 $\psi$ 以及分母 $D_{1},\cdots ,D_{n}$ 都是公式集；$\rho$ 是規則的名稱。我們使用以下規則引入 $K$-tableaux

$(\land ){\frac {X;P\land Q}{X;P;Q}}$           $(\lor ){\frac {X;\lnot (P\land Q)}{X;\lnot P;\mid X;\lnot Q}}$

$(\bot ){\frac {X;P;\lnot P}{\bot }}$           $(\lnot ){\frac {X;\lnot \lnot P}{X;P}}$

$(\theta ){\frac {X;Y}{X}}$                       $(K){\frac {\square X;\lnot \square P}{X;\lnot P}}$

一組公式的 tableau $X$ 是一個有限樹，其根節點為 $X$，節點包含有限的公式集。擴充套件 tableau 的規則如下：

• 選擇一個葉節點 $n$，其標籤為 $Y$，其中 $n$ 不是終端節點，並選擇一個規則 $\rho$，該規則適用於 $n$；
• 如果 $\rho$ 有 $k$ 個分母，則為 $n$ 建立 $k$ 個後繼節點，後繼節點 $i$ 攜帶相應的分母例項 $D_{i}$；
• 如果一個後繼節點 $s$ 攜帶一個集合 $Z$ 且 $Z$ 已經在從根節點到 $s$ 的分支上出現過，則 $s$ 是一個終端節點。

如果一個分支的終端節點攜帶 ${\bot }$，則該分支稱為閉合分支，否則稱為開放分支。

與經典情況類似，公式 $A$ 是模態邏輯 $K$ 中的一個定理，當且僅當集合 $\lnot A$ 存在一個封閉的 $K$-tableau。

例如，取公式 $\square (p\to q)\to (\square p\to \square q)$：它的否定顯然不可滿足，因為該公式是我們之前給出的 $K$-公理的一個例項。

有一些需要說明的

• $\theta$-規則，稱為弱化規則，是構建 $K$-規則應用的前提所必需的。
• 兩者可以結合成一個新規則

$(K\theta ){\frac {Y;\square X;\lnot \square P}{X;\lnot P}}$

• 為了獲得其他提到的演算（如 $T$ 或 $K4$）的 tableau 演算，必須引入額外的規則

$(T){\frac {X;\lnot \square P}{X;\square P;P}}$

這顯然反映了可達性關係的自反性，或者

$(K4){\frac {\square X;\lnot \square P}{X;\square X;\lnot P}}$

反映了傳遞性。