模型论视角下对正规多元模态逻辑的阐述（英文）

本文对正规多元模态逻辑做了模型论视角的整体阐述。正规多元模态逻辑(PML)是对一元模态逻辑系统K,在n 元算子上的推广。而多元模态逻辑的研究相对于一元逻辑较为匮乏。文献中的一系列有关PML 的结果也被看作是有关K的结论的直接推广,而缺少部分完整证明,且已有证明多为代数证明。PML 对于K 的推广在某些方面是非平凡的,忽略这一点导致了一些教材及文章中甚至存在各种错误。从证明的角度上讲,对于PML 的证明有时也需要不同的方法。基于以上几点考虑,我们认为有必要从模型论视角对PML 做一个细致的考察,并给出一些模型论版本的证明,来简化以往的代数证明,从而给研究者提供一个统一的参考。本文从两个模态逻辑常用的模型构造方法(滤子和超滤扩张)出发,以经典教材中的定义为准,补全一些重要定理在多元语言下的模型论方法的详细证明。然后我们对van-Benthem 刻画定理的多元版本证明做了一个澄清,考察了多元语言和一元语言下证明的具体区别。最后我们用模型论方法证明了PML 具有插值性,而该定理在文献中往往是被当作一些代数事实的推论。

Model Theoretical Aspects of Normal Polyadic Modal Logic: An Exposition

In this paper, we give an exposition on the model theoretical aspects of normal polyadic modal logic (PML), which is a modal logic with n-ary modalities generalizing the basic normal modal logic K. Compared to the basic normal modal logic K, PML is much less studied. Basic results about PML scattered in the literature are often stated without proofs, except in certain algebraic setting, as they are considered as straightforward generalizations of the results of K. Besides the missing details, the very limited available expositions are errorprone even in well-known textbooks and papers, since the generalization to the polyadic setting from the monadic one is sometimes non-trivial, which requires different techniques. Therefore, we think there is a need for a detailed exposition of the basic model theoretical results of PML proved in the modal logic setting, to provide a unified reference for further studies of PML, and this is the goal of the paper. In this paper, we review the definition of filtration and ultrafilter extension for polyadic language and give proofs for some basic theorems including the saturation theorem of ultrafilter extension in a purely model theoretical way other than algebraic one. Then we give a clarification on proving van-Benthem characterization theorem of PML in order to exhibit differences in the proof from the monadic cases. Finally, we also give a model theoretical proof for the Craig Interpolation Theorem of PML while the theorem was treated as a corollary of some algebraic results in the literature.