计算机科学家逻辑/模态逻辑/模态逻辑 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}}$

反映了传递性。