Canonical formulas for K4. Part II: Cofinal subframe logics
Canonical formulas for K4. Part II: Cofinal subframe logics
复制标题
K4 的规范公式。
DOI：
10.2307/2275669
复制
发表时间：
1996
影响因子：
0.6
通讯作者：
M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
M. Zakharyaschev
本文是Zakharyaschev [25]的继续，在[25]中得到了关于具有传递框架的模态逻辑的下列基本结果：·对于每个有限根传递框架和两个公式α（，）中的每个反链集（称为闭域），α（，）是相关联的。我们分别称它们为规范公式和否定自由规范公式，并证明了用次约化（又称部分p-态射）、共尾性条件和闭域条件刻画它们的反驳一般框架的构造的可反驳性准则。·我们还证明了规范公式的完备性定理，为我们提供了一种算法，该算法给定模态公式φ，返回规范公式α（i，i），（i = 1，...，n），使得如果φ是否定自由的，则该算法而不是α（i，i，α）可以使用否定自由的规范公式α（i，i）。因此，每一个包含K4的正规模态逻辑都可以用一组规范公式公理化。在这一部分中，我们应用规范公式的工具，在K_4域中建立了模态逻辑的可判定性、有限模型性质、元素性和其他一些性质的一些结果。我们的注意力将集中在一类逻辑，可以公理化的规范公式没有封闭的领域，即，根据Fine [11]的术语，我们称它们为共尾子帧逻辑，并将这类逻辑表示为。正如第一部分所示，几乎所有的标准模态逻辑都在。
This paper is a continuation of Zakharyaschev [25], where the following basic results on modal logics with transitive frames were obtained: • With every finite rooted transitive frame and every set of antichains (which were called closed domains) in two formulas α (, , ⊥) and α(, ) were associated. We called them the canonical and negation free canonical formulas, respectively, and proved the Refutability Criterion characterizing the constitution of their refutation general frames in terms of subreduction (alias partial p-morphism), the cofinality condition and the closed domain condition. • We proved also the Completeness Theorem for the canonical formulas providing us with an algorithm which, given a modal formula φ, returns canonical formulas α(i, i), ⊥), for i = 1,…, n, such that if φ is negation free then the algorithm instead of α(i, i, ⊥) can use the negation free canonical formulas α(i, i). Thus, every normal modal logic containing K4 can be axiomatized by a set of canonical formulas. In this Part we apply the apparatus of the canonical formulas for establishing a number of results on the decidability, finite model property, elementarity and some other properties of modal logics within the field of K4. Our attention will be focused on the class of logics which can be axiomatized by canonical formulas without closed domains, i.e., on the logics of the form Adapting the terminology of Fine [11], we call them the cofinal subframe logics and denote this class by . As was shown in Part I, almost all standard modal logics are in .