Canonical formulas for K4. Part I: Basic results
Canonical formulas for K4. Part I: Basic results
复制标题
K4 的规范公式。
DOI：
10.2307/2275372
复制
发表时间：
1992
影响因子：
0.6
通讯作者：
M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
M. Zakharyaschev
本文提出了一种处理具有传递框架的模态逻辑的新技术，即模态系统K4的扩展。实际上，该技术基于以下基本结果，将在§3中得到。给定一个公式φ，我们可以有效地构造有限坐标系1，…，n，它们完全表征反驳φ的所有传递一般坐标系的集合。更确切地说，一个任意的一般坐标系反驳φ iff包含一个（不一定生成的）子坐标系，使得(1)i，对于某些i λ{1，…，n}，是（在Fine[1985]之后，我们说它是可约于i的）的p-态象，(2)在上是协定的，(3)不在上的每一个点都不能进入在i中由φ唯一确定的“闭域”。事实证明，这一纯粹的技术结果产生了意想不到的深远影响。例如，如果φ决定与其相关的坐标系1，…，n中没有闭域，则由φ生成的K4的法向扩展具有有限模型性质，因此是可决定的。而且，任何可由这类公式的任意（甚至无限）集合公理化的正规逻辑φ也具有有限模型性质。如果不是因为这类逻辑包含了K4领域内几乎所有的标准系统（至少是Segerberg[1971]或Bull和Segerberg[1984]提到的所有标准系统），包含S4.3的所有逻辑，Fine[1985]的所有子框架逻辑，以及其他逻辑的连续体，这个观察结果可能不值得任何特别注意。
This paper presents a new technique for handling modal logics with transitive frames, i.e. extensions of the modal system K4. In effect, the technique is based on the following fundamental result, to be obtained below in §3. Given a formula φ, we can effectively construct finite frames 1, …, n which completely characterize the set of all transitive general frames refuting φ. More exactly, an arbitrary general frame refutes φ iff contains a (not necessarily generated) subframe such that (1) i, for some i ϵ {1, …, n}, is a p-morphic image of (after Fine [1985] we say is subreducible to i), (2) is cofinal in , and (3) every point in that is not in does not get into “closed domains” which are uniquely determined in i, by φ. This purely technical result has, as it turns out, rather unexpected and profound consequences. For instance, it follows at once that if φ determines no closed domains in the frames 1, …, n associated with it, then the normal extension of K4 generated by φ has the finite model property and so is decidable. Moreover, every normal logic axiomatizable by any (even infinite) set of such formulas φ also has the finite model property. This observation would not possibly merit any special attention, were it not for the fact that the class of such logics contains almost all the standard systems within the field of K4 (at least all those mentioned by Segerberg [1971] or Bull and Segerberg [1984]), all logics containing S4.3, all subframe logics of Fine [1985], and a continuum of other logics as well.