混合模态逻辑的有穷模型性研究

彭玉 林哲

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）来研究单模态逻辑的重要性质与混合多模态逻辑相应性质的关系。传递性定理是说如果一些重要的性质如完全性和有穷模型性等在某些单模态逻辑中成立，那么在基于这些单模态逻辑的混合模态逻辑中也成立。克拉赫特（M.Kracht）和沃尔特（F.Wolter）在[5]中通过代数的方法证明了在一些经典模态逻辑中传递性定理成立。遗憾的是没有已证的时态逻辑上的传递性定理的一般性结果。

除了上述的混合模态逻辑与混合时态逻辑外，时态逻辑与模态逻辑的混合也具有强烈的研究动机。一般单维时态逻辑被认为是复杂信息系统的表达和推理形式工具，而添加模态混合可以增强其表达力，使其可表达平行的论域、过程或代理，并且也让表示无限大小的系统成为可能。例如时态和模态逻辑的混合可以用来刻画知识或信仰如何随时间发生变化。从哲学的角度来看，时态和模态相结合的逻辑系统也是一个有趣的问题，因为这些逻辑在原始的哲学问题上有着广泛的应用领域，例如因果关系理论、行为理论等。这方面的研究始于托马斯（R.Thomason，[13]）。不同的时态和模态逻辑的混合逻辑被许多学者所关注，例如在[10]中莱夫（J.Reif）和希斯塔拉（A.Sista）提出了一种时态和空间模态混合的逻辑，而雷洛兹（M.Reynolds）在[11]中考虑了时态逻辑K4.3.t和模态逻辑S5的混合逻辑，并证明了这种混合逻辑虽然具有可判定性但却不具有穷模型性。本文考虑了雷洛兹的混合逻辑的基础逻辑即时态逻辑K4.t和模态逻辑S5的混合逻辑。与时态逻辑K4.3.t和模态逻辑S5的混合逻辑不同，本文证明了K4.t和模态逻辑S5的混合逻辑具有有穷模型性。鉴于时态逻辑也是模态逻辑的一种，同时本文对混合时态模态逻辑的研究方法同样也适用于时态逻辑与时态逻辑，或者模态逻辑与模态逻辑之间的混合。因此在本文中统一将这三种混合逻辑称为混合模态逻辑。

本文给出了一种适用于混合模态逻辑有穷模型性的一般性证明方法，并用该方法证明了时态逻辑K4.t和模态逻辑S5的混合逻辑具有有穷模型性。该逻辑是传递性基础时态逻辑K4.t和认知逻辑S5的混合逻辑，是重要的基础混合时态模态逻辑，同时也是雷洛兹考虑的混合逻辑的基础逻辑。该逻辑的有穷模型性是未知的，本文给出了肯定的回答。同时本文所采用的有穷模型性证明方法还可以被直接应用到混合模态逻辑M×M,M×N 和N×N 中。其中M 为基础时态逻辑K.t（[14]）的D,T,B,4 扩张，而N 为模态逻辑的D,T,B,4 扩张。本文证明有穷模型性的方法是一种代数证明论方法。该方法关键在于构造基于目标逻辑且满足内插引理的矢列。此条内插引理源于克拉格（Crag）的内插引理，由鲁达（D.Rooda）首次引入到兰贝克演算。这条性质被用来证明一些子结构逻辑的表达力等价于上下文无关文法语言。如彭图斯（M.Pentus，[9]）证明了兰贝克演算的表达力等价于上下文无关文法语法。该引理也被范拉列斯基（M.Farulewski，[2]）和布斯科沃夫斯基（W.Buszkowski，[1]）应用于证明非结合的兰贝克演算及其多种格上延伸的强有穷模型性和嵌入性。林哲（Z.Lin，[7,8]）修改此条性质并应用于证明不同的非经典模态逻辑的有穷模型性或强有穷模型性。本文证明方法源自[7,8]中的方法，并在此基础上做了拓展，简化并应用到经典时态与模态逻辑中。

本文结构安排如下：第2 节中引入K4.t×S5混合逻辑，同时给出了其对应的代数及矢列演算系统。第3 节中证明K4.t×S5混合逻辑具有有穷模型性，并讨论了该结论如何扩展到其他一般混合时态和模态逻辑中，第4 节总结了本文的工作并展望了进一步的研究前景。

2 混合逻辑的代数语义及矢列演算系统

定理1.矢列演算系统G对于K4.t×S5代数类是有效完全的。

对于有效性的证明，只需要逐条检验定义4中的(1) (10)在G中都成立即可。而完全性的证明可以由经典的塔斯基林登鲍姆构造证明，也可由下节有穷模型性的证明得到。

3 有穷模型性

本节证明矢列演算系统G具有代数有穷模型性。令S为一矢列演算，K(S)为其对应的完全有效的代数类。如S=G，则K(G)是K4.t×S5代数类。一个矢列演算系统S有代数有穷模型性指的是：如果对于S中的任意矢列Γ⇒β，/⊢SΓ⇒β，那么必然存在一个有穷代数A ∈K(S)，使得/|=AΓ⇒β。对任意公式α,令sub(α)表示其所有子公式组成的集合。令T为一个公式集合，定义s(T)。

定义6.令s(T)为满足下面所有条件的最小公式集：

则可得到混合逻辑KD4.t×S5，由于在上面有穷模型性的证明中D的证明类似于T的证明，因此易得到KD4.t×S5的有穷模型性。另在时态上考虑B的扩张，则有♢=♦，那么可以得到相应模态混合扩张的有穷模型性。如在K4.t×S5增加K4.t的B 性质及相关证明，那么可以得到K4×S5的有穷模型性证明。同样考虑两时态逻辑混合只需要重复时态部分的证明即可得到相应的混合逻辑的有穷模型性证明，如K4.t×K4.t。综上所述通过该方法我们可以得到当K1和K2是经典时态逻辑K.t或经典模态逻辑K上的D,T,B,4 组合扩张时，K1和K2的混合逻辑同样具有有穷模型性。

4 结论

本文证明了时态逻辑K4.t和模态逻辑S5的混合逻辑具有穷模型性，并且该结果可延伸为一般性的结果：当K1和K2是经典时态逻辑K.t或经典模态逻辑K上的D,T,B,4 组合扩张时，K1和K2的混合逻辑同样具有有穷模型性。

本文建立一种证明混合时态逻辑和混合模态逻辑的有穷模型性的一般证明方法。该方法也可以被用来证明常见的正规模态或时态逻辑的有穷模型性。本文的证明方法基于代数证明论，其关键是证明混合的两个单维时态或模态逻辑存在满足内插引理性质的矢列演算系统。在未来的研究中我们将尝试给出存在内插引理性质的矢列演算系统的时态或模态逻辑的代数条件，以期将本证明拓展为更一般的结果。