四值模态逻辑的免切割相继式演算与自然演绎

四值模态逻辑（${\cal TML}$）是 Font 和 Rius（\cite{FR2}）定义的两个逻辑之一（另一个是正规四值模态逻辑 ${\cal TML}^N$），与 Monteiro 的四值模态代数相关。这些逻辑是著名的 Belnap–Dunn 四值逻辑的扩展，结合了多值特征（四值性）与模态特征。事实上，$\cal TML$ 是关于四值模态代数保持真度的逻辑。正如 Font 和 Rius 所观察到的，逻辑 $\cal TML$ 与代数之间的联系不如在 ${\cal TML}^N$ 中那样良好，但作为补偿，它具有更好的证明论行为，因为它有一个强充分的 Gentzen 演算（见 \cite{FR2}）。在这项工作中，我们证明 Font 和 Rius 给出的相继式演算不具有切割消除性质。然后，利用 Avron、Ben-Naim 和 Konikowska（\cite{Avron02}）提出的一般方法，我们为 $\cal TML$ 提供了一个具有切割消除性质的相继式演算。最后，受后者的启发，我们提出了一个关于四值模态逻辑可靠且完备的自然演绎系统。