BK的模态公理化

《Journal of Logic and Computation》：A Modal Axiomatization of BK

当移除模态逻辑中的(K)公理和必然规则后，系统与巴西非一致逻辑BK相关，通过3值非确定性语义矩阵及精细化方法，证明其与T、S4模态逻辑的联系，为非经典逻辑研究提供新视角。

　　

摘要

如果我们从模态逻辑的常规公理化表述中去掉公理(K)和必要性规则，会发生什么？这个系统最初由Ivlev（1988年，《Bull. Sect. Log.》，17，114–121）提出。我们证明这种逻辑是著名的“paraconsistent logic”（也称为“mbCciw”）的一种语法变体，而“paraconsistent logic”属于一个称为“Logics of Formal Inconsistency”（LFIs）的大型逻辑家族。我们的方法是语义学的，因为“paraconsistent logic”可以通过一个三值非确定性矩阵（Nmatrix）来表征；我们还证明这个Nmatrix可以用更简洁的公理在模态词汇表中重新公理化。这一结果将这类paraconsistent逻辑与另一条研究方向联系起来，后者旨在描述不依赖于可能世界的模态逻辑，这一研究方向由Kearns（1981年，《J. Symb. Log.》，46，77–86）和Ivlev（1988年，《Bull. Sect. Log.》，17，114–121）的工作开启。我们将看到，“T”逻辑及其去掉必要性规则后的版本，以及“S4”逻辑，都可以借助这个单一Nmatrix的简单“细化”（refinements）来表征。所有这些表明，这种逻辑既可以作为模态逻辑的基础，也可以作为LFIs的基础。