公式分层的谓词模态逻辑  

Formula-Layered Predicate Modal Logic

作　　者：孙梅莹 邓少波[1,2] 陈博[1,2] 曹存根[1] 眭跃飞[1] 

机构地区：[1]中国科学院计算技术研究所智能信息处理重点实验室,北京100190 [2]中国科学院大学,北京100049

出　　处：《软件学报》2014年第5期1014-1024,共11页Journal of Software

基　　金：国家自然科学基金(60573064;91224006;61203284;61173063)

摘　　要：由于必然模态词的引入,谓词模态逻辑的公式在一个可能世界中的真假值可能依赖于其可达的可能世界.在谓词模态逻辑中存在个体跨可能世界相等问题.针对这一问题,Lewis提出了对应物理论,并且在对应物理论中用对应物关系来表示个体跨可能世界相等.但是,当一个对象具有一个以上的对应物时,谓词模态逻辑中的跨可能世界相等关系无法与对应物关系建立一一对应.通过限制谓词模态逻辑中全称量词?的范围,给出了一种公式分层的谓词模态逻辑.它是谓词模态逻辑的一个子逻辑,并且其语言与谓词模态逻辑的语言是相同的.但其公式是分层定义的,使得?可以出现在的范围内,并且不能出现在?的范围内.由于任意形如?x?(x)的表达式都不是该逻辑的公式,以量词开头的公式在一个可能世界w中的真假值只依赖于w,该逻辑避免了个体跨可能世界相等问题.给出了该逻辑的语言、语法和语义,并证明了该逻辑是可靠的和完备的.As an introduction to the necessary modality □, the truth values of formulas of the predicate modal logic in a possible world may rely on its alternative worlds. So there is a problem of the transworld identity of individuals in the predicate modal logic. According to this problem, Lewis proposed the counterpart theory and used the counterpart relation to represent the transworld identity of individuals in the counterpart theory. When an object has more than one counterpart, the transworld identity cannot have a one-to-one correspondence with the counterpart relation. By limiting the scope of the universal quantifier Ⅴ in the predicate modal logic, this paper gives a formula- layered predicate modal logic, which is a sublogic of the predicate modal logic, and which language is the same as that of the predicate modal logic. But the definition of its formulas is decomposed into layers such that Ⅴ may occur in the scope of o, and □ cannot occur in the scope of Ⅴ. Since any expression in the form of Ⅴχ□φ（χ） is not a formula of this logic, the truth value of any formula which begins with a quantifier in a possible world w only relies on w, and this logic avoids the problem of the transworld identity of individuals. This paper gives the language, the syntax and the semantics of this logic, and proves that this logic is sound and complete.

关 键 词：跨可能世界相等 谓词模态逻辑 可变论域语义 Ⅴ-性质 可靠性 完备性 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]