Logics containing K4. Part II
Logics containing K4. Part II
复制标题
包含 K4 的逻辑。
DOI：
10.2307/2274318
复制
发表时间：
1985
影响因子：
0.6
通讯作者：
K. Fine
中科院分区：
文献类型：
--
作者：
K. Fine
本文为 K4 领域内的逻辑建立了另一个非常普遍的完整性结果。对于每个有限传递框架 ℭ，我们可以关联一个公式 — Bℭ，它仅验证那些 ℑ 在某种意义上不可嵌入的框架 ℑ（确切地说，ℭ 不是 ℑ 的任何子框架的 p 形态图像。通过子框架逻辑，我们指的是将此类公式作为公理添加到 K4 的结果。一般结果是每个子框架逻辑都具有有限模型属性。有子帧逻辑的连续体，其中包括许多标准逻辑，例如 T、S4、S4.3、S5 和 G。事实证明，子帧逻辑正是在子帧下闭合的条件的逻辑（满足该条件的帧的任何子帧也满足该条件），因此，在子帧下闭合的条件的每个逻辑都具有有限模型属性。紧凑逻辑只是那些公理表达基本条件的测试，其目的是确定给定公理是否表达了基本条件，以及在它表达基本条件的情况下确定它是什么。在一方面，目前的一般完整性结果与文献中的大多数其他逻辑不同，其他逻辑通常要么是基于逻辑的，要么是基于公式的，或者是包含给定逻辑的所有逻辑都是完整的，或者是所有包含给定逻辑的逻辑都是完整的。相比之下，目前的结果是基于框架的，而要证明完整的逻辑公理是根据它们与某些框架的联系来最直接地描述的。
This paper establishes another very general completeness result for the logics within the field of K4. With each finite transitive frame ℭ we may associate a formula — Bℭ which validates just those frames ℑ in which ℭ is not in a certain sense embeddable (to be exact, ℭ is not the p-morphic image of any subframe of ℑ. By a subframe logic we mean the result of adding such formulas as axioms to K4. The general result is that each subframe logic has the finite model property. There are a continuum of subframe logics and they include many of the standard ones, such as T, S4, S4.3, S5 and G. It turns out that the subframe logics are exactly those complete for a condition that is closed under subframes (any subframe of a frame satisfying the condition also satisfies the condition). As a consequence, every logic complete for a condition closed under subframes has the finite model property. It is ascertained which of the subframe logics are compact. It turns out that the compact logics are just those whose axioms express an elementary condition. Tests are given for determining whether a given axiom expresses an elementary condition and for determining what it is in case it does. In one respect the present general completeness result differs from most of the others in the literature. The others have usually either been what one might call logic based or formula based. They have usually either been to the effect that all of the logics containing a given logic are complete or to the effect that all logics whose axioms come from a given syntactically characterized class of formulas are complete. The present result is, by contrast, what one might call frame based. The axioms of the logics to be proved complete are characterized most directly in terms of their connection with certain frames.