彭玉 林哲

1 引言

所谓一个逻辑具有有穷模型性是指如果一公式在该逻辑系统中不可证，那么它在该逻辑系统的一有穷模型中不成立。有穷模型性是逻辑研究中重要的基础性质之一，此概念不仅本身具有重要意义，并且有广泛应用。一个有穷可公理化且具有有穷模型性的逻辑是可判定的。长久以来，一逻辑是否具有有穷模型性是证明其是否可判定的重要方式。关于模态逻辑的有穷模型性有着广泛的研究。模态逻辑的有穷模型性的一般证明方法是滤子方法（见[6]）。盖比（D.M.Gabby，[4]）给出了滤子方法在模态逻辑上的一般化方案，证明了如K、T、B、S4、S4.1、S4.2、S5等熟知的经典模态逻辑具有有穷模型性。扎哈拉斯基夫(M.Zakharyaschev)在[15,16]中修改这种方法并用典范公式证明了K4以上的所有经典模态逻辑具有有穷模型性。时态逻辑的有穷模型性问题也备受研究者们的关注，有部分时态逻辑被证明具有有穷模型性，也有部分被证明并不满足有穷模型性，具体可参照赛格博格(K.Segerberg)的研究（[12]）。沃尔特（F.Wolter，[14]）考虑了时态逻辑有穷模型性的一般化结论，他将扎哈拉斯基夫在模态逻辑上的结论延伸到经典时态逻辑中，证明了K4以上满足一定典范框架条件的所有经典时态逻辑具有有穷模型性。

模态逻辑和时态逻辑有着广泛的应用场景，如认知、人工智能、逻辑程序、知识表达等，因此单模态不足以驾驭如此多的应用。许多逻辑学家早已敏锐地察觉到混合模态逻辑研究的重要性。范恩（K.Fine）和舒尔茨（G.Schurz）在[3]中提出了传递性定理（transfer theorem）来研究单模态逻辑的重要性质与混合多模态逻辑相应性质的关系。……