克里普克关系语义

美国逻辑学家S．A．克里普克(Kripke)建立的模态逻辑的一种集合论语义，也称可能世界语义。基本概念是克里普克标架和模型。一个克里普克标架(W，R)由一个集合W和W上的一个二元关系R组成，通常称W中元素为可能世界，称R为可能世界之间的可达关系。要想在克里普克标架(W，R)上解释模态命题，首先必须弄清原子命题在各个可能世界w中的真假情况，也就是要指定哪些原子命题是为可能世界w所接受的，哪些不是为w所接受的。这样的指派称为赋值，以V表示，然后按照下面的要求把V扩张到所有的模态命题：①任一个可能世界w所接受的全部模态命题必须保持通常有关命题联结词的真值条件(例如，w接受A∨B当且仅当w接受A或者w接受B；w接受A当且仅当w不接受A)，而且还必须对分离规则封闭，即，如果w接受A和AB那么w也接受B。②可能世界w接受模态命题□A当且仅当w可达的可能世界都接受A，也就是说，w接受□A当且仅当任一个满足wRw′的w′都接受A。给定对原子命题的赋值V后，满足这两个要求的赋值V的扩张是唯一的，通常以归纳定义的形式出现。所得到的关系就是可能世界在赋值下接受哪些命题的关系，以“wvA”表示“可能世界w在赋值w下接受命题A”，简言之“w在V下接受A”。一个克里普克模型(W，R，V)由一个克里普克标架(W，R)和一个赋值V组成。如果对于W中的任一个可能世界w而言关系wvA都成立，则称命题A在克里普克模型(W，R，V)中为真，记成(W，R，V)A。如果命题A对于任一个赋值V都有(W，R，V)A，则称A在克里普克标架(W，R)上有效，记成(W，R)A。如果命题A在某个克里普克标架类C中的任一个克里普克标架上有效，则称A在这个类C中有效，记成CA。

在古典命题逻辑的语言中加进模态词□和◇就得到模态命题逻辑的语言，这语言中的合式公式就表示模态命题。所谓一个模态逻辑或模态系统L，就是包含所有重言式并且对于分离规则和代入规则都封闭的一个模态命题类；类中的命题被称为L的定理，A∈L也记为┝A或L┝A。如果一个模态逻辑或模态系统含有命题□(pq)(□p□q)并且还对必然概括规则(从A推出□A)封闭，则称之为一个正规模态逻辑或正规模态系统。最小的正规模态逻辑是系统K。在系统K中附加若干模态命题就可形成各种正规模态系统，例如附加□pp得系统T，再附加□p□□p就得系统S4，进一步再附加p□◇p还可得到系统S5。称一个克里普克标架类C决定了一个模态逻辑L，当且仅当，任一个命题A为L的定理等价于它在C中有效。例如，系统K就是由全体克里普克标架决定的。正规模态逻辑的完全性问题，就是确定一个正规模态系统是否由一类克里普克标架决定的问题。不同的正规模态系统反映了对可达关系的不同要求，例如系统T由全体具有自返的可达关系的克里普克标架所决定，系统S4由全体具有自返的、传递的可达关系的克里普克标架所决定，系统S5则由全体具有自返的、传递的、反对称的可达关系的克里普克标架所决定。克里普克关系语义理论提出以后，很快解决了一大批模态系统的完全性问题，也发展了多种证明完全性的方法。克里普克本人用的是语义图方法，这种方法复杂繁琐而又不充分，现在基本上没有人使用。20世纪60年代中期由E．J．雷蒙(Lem mon，1930～1966)和D．S．司各脱(Scott)等人建立起了典范模型方法。这是极其有力而又灵活的证明方法，60年代以来使用范围很广。雷蒙和司各脱用这方法在他们的合著中建立了正规模态系统KG′的完全性结果；这里，G′表示公理◇□p□◇p，m、n、e、k都是非负整数。系统KG′就是把G′作为公理附加进系统K而得的正规模态系统，或者说是包含K和G′的最小正规模态系统。诸如D、T、B、S4、S5等常见的系统都是G′中的m、n、e、k取具体数字时的情形，因此他们的结果是相当一般的，统一处理了一大类系统的完全性。雷蒙和司各脱还作了一个推广性的猜测，概括了更大一类正规模态系统的完全性。1973年H．塞奎斯特(Sahlgvist)证实了这一猜测，得到了更一般性的结果。他提出的模式是

这里，A是任一个由原子命题及其否定利用模态算子□、◇和联结词∧、∨构成的命题，但不允许◇、∧或∨出现在任一个□的辖域内；而B则是由原子命题利用□、◇、∧和∨构成的命题，不允许利用否定联结词。相应于模式Sahl的语义条件当然是十分复杂的，但把它的任意多个实例加进系统K所得的正规模态系统却仍是完全的。70年代出现了一些不完全性结果，也就是一些不为任何一类克里普克标架类决定的正规模态系统。这些不完全性结果的出现表明，尽管克里普克关系语义功绩卓著，但它作为研究模态系统的工具还是不充分的。