一阶模态逻辑的语义问题
江峰，眭跃飞，曹存根
摘要一阶模态逻辑最初是被当成非经典逻辑的一个分支而逐步发展起来的。通过在经典的命题逻辑和谓词逻辑（一阶逻辑）的基础上增加两个模态算子：必然算子□和可能算子◇，我们可以分别得到命题模态逻辑以及一阶模态逻辑。目前，命题模态逻辑已经被广泛用于人工智能以及计算机科学的其他领域。但是一阶模态逻辑却很少有人愿意涉及，这是因为对于一阶模态逻辑语义的研究还存在很多的争议和问题。从表面上看，一阶模态逻辑不过是在命题模态逻辑中添加量词而得到的。然而事情并非这么简单，似乎正是这些新添加的量词给我们的语义解释带来许多的问题和麻烦。本文主要从当前一阶模态逻辑语义研究中所面临的主要问题、目前已经提出的一阶模态逻辑语义以及这些语义的不足之处这三个方面来展开讨论。
关键词命题模态逻辑；一阶模态逻辑；可能世界语义
1模态逻辑介绍
模态逻辑是逻辑学中的一个重要的分支，它主要研究由模态词构成的模态命题（公式）以及这些命题（公式）之间的逻辑关系。在汉语中，“模态”是英语形容词“modal”的音译，指事物对象或认识的必然性、偶然性和可能性等这类性质。模态在思维中的反映表现为一定的认识或观念，即模态概念。对应于不同的模态就有不同的模态概念。例如，必然、可能、允许信念等等。模态词就是语言中用以表示模态或者模态概念的词语或符号。模态词是模态命题中的逻辑常项。含有模态词的命题是模态命题，以模态命题为前提或结论的推理，即含有模态词的推理，是模态推理。模态逻辑所研究的模态命题“□A”和“◇A”（其中A是一个命题，□和◇是两个模态词，“□A”代表必然A，“◇A”代表可能A）与通常命题逻辑中的命题不同。后者是真值函项，前者不是。因为，当 A 为真时，“□A”既可以是真也可以是假；当 A 为假时，“◇A”既可以是真也可以是假 [51]。
模态逻辑具有悠久的历史。早在约公元前300 年，古希腊哲学家亚里士多德 (Aristotle) 就已经对模态逻辑进行过系统的研究。他对必然性, 可能性和偶然性等模态词做了深刻细致的分析，并提出了一个模态三段论。亚里士多德的学生泰奥弗拉斯托斯(Theophrastus) 也创造了一个不同的模态三段论系统。稍后，麦加拉－斯多阿学派 (Megaric-stoics School) 对必然与可能这些模态概念进行了深入的探讨。在公元9～12 世纪，阿拉伯逻辑学家吸取了古希腊有关模态逻辑的思想并有所发展。伊本·西那 (Ibn Sina) 把模态概念和命题的时间结合起来，创造了一个新的模态三段论系统。12～15 世纪的欧洲经院逻辑学家区分了命题模态与事物模态合的意义下的模态与分的意义下的模态。邓斯·司各特 (Duns Scotus) 还构造了一个在合的意义下的模态三段论系统和一个在分的意义下的模态三段论系统。奥康的威廉(William of Occam) 则构造了一个这样的模态三段论系统：其中一个前提是在合的意义下的模态命题，而另一个前提是在分的意义下的模态命题。此外，经院逻辑学家还研究了知道、怀疑、愿意等主观模态概念和应当、许可等道义概念的逻辑性质[53]。
以上所论述的模态逻辑通常被称为传统模态逻辑。德国哲学家莱布尼茨 (Lebniz) 是现代逻辑的创始人，对现代模态逻辑的创立也做出了卓越的贡献。他提出了可能世界理论，成为现代模态逻辑语义理论的基本内容。现代模态逻辑的创始人是美国逻辑学家刘易斯(C. I. Lewis)。他在 1912 年发表的《蕴涵和逻辑代数》中提出了不同于实质蕴涵的严格蕴涵，并构造了一系列严格蕴涵系统。1914 年他又发表了《严格蕴涵的运算》和《蕴涵的矩阵代数》这两篇论文，提出了严格蕴涵的命题演算。1932 年他同兰福德 (C. H. Langford) 合著《符号逻辑》，提出模态命题演算 S1 和 S2，后来又建立了 S3，S4 和 S5 系统 [51]。
下面，我们来讨论模态逻辑的语义问题。直观地说，一个逻辑系统的语义就是对该逻辑系统中
所使用到的符号和符号序列进行解释 [48]。模态逻辑的基本体系包括命题模态逻辑和一阶模态逻辑。其中命题模态逻辑是在经典的命题逻辑的基础上加入一个必然算子□和一个可能算子◇得到的；而一阶模态逻辑则是在经典的一阶逻辑的基础上增加□和◇而形成的扩张。因此，我们在
考虑模态逻辑的语义时，关键的问题就是如何解释这两个算子。为了解决模态逻辑的语义解释问题，克里普克 (S. A. Kripke) 等人提出了可能世界语义。可能世界语义实际上是由坎格尔 (S. Kanger)、
欣蒂卡 (J. Hintikka) 和克里普克 (S. A. Kripke) 等逻辑学家在上世纪五十年代同时提出的。由于克
里普克最为明确地指出他的语义来自于莱布尼茨的思想，并且用他的语义证明了一系列模态逻辑系
统的完全性，所以影响最大。可能世界语义的基本出发点来自于莱布尼茨关于必然性和可能世界的
思想：一个命题是必然的，当且仅当，它不仅在现实世界中为真，而且在所有可能世界中都为真 [51]。
可能世界语义的基本思想是：给定一个框架F=
指派，对常量和谓词符号进行解释。从而我们就可以规定模态公式的真值和有效性，定义逻辑真、
逻辑推导以及证明模态逻辑系统的可靠性和完备性。在可能世界语义中，对必然算子□和可能算
子◇的解释可以分别表示为：
1．对必然算子 □ 的解释：一个公式在某一可能世界中是必然为真的，当且仅当它在由 该可能世界可达的所有可能世界中都是真的。
2．对可能算子 ◇ 的解释：一个公式在某一可能世界中是可能为真的，当且仅当它在由该可能世界可达的某个可能世界中是真的。
可能世界语义的提出具有重要的意义。它不仅解决了现代模态逻辑中模态概念不清楚并且没有
分析工具这一极其重要的问题，而且为模态逻辑的发展提供了新的理论和方法。它为分析各类必然
性1提供了有力的技术手段，使得必然性这种几乎无从下手分析的性质得到了严格的刻画，分清了
不同的必然性的强弱层次。今天，可能世界语义已在逻辑学中占有非常重要的地位。经典逻辑的语
义也可以被看作可能世界语义的特例[52]。
自上世纪 50 年代以来，模态逻辑在语法、代数、模型论等研究方向以及道义、可证性、多值、直觉主义、认知等等领域发展迅速。对于人工智能和计算机科学中的许多应用领域，经典谓词逻辑
的表达能力是不够的，不容易恰当地表达知识，这样的应用系统大多数具有状态和状态转换这种基
本现象。模态逻辑及其各种扩展，如时态逻辑[43]、认知逻辑[28]、道义逻辑[2]、动态逻辑 [26]、可
证性逻辑 [8] 已经成为更适合应用于这类问题相关领域的逻辑系统。时态逻辑、认知逻辑、道义逻辑、动态逻辑、可证性逻辑等这样一些模态逻辑分支在人工智能 [9] [16]、形式化验证及模型检测 [41] [42]、
硬件验证[5] [47]、数据库理论[13] [14]、分布式计算[10] [25]、网络协议制定与安全性验证[10] [15]等等
领域都日渐显示出其不可替代的作用。如今，模态逻辑已经发展成为一个庞大的逻辑分支，其中比
较典型的命题模态逻辑系统包括：K 系统、T 系统、B 系统、S4 和 S5 系统等等。
2一阶模态逻辑介绍
早在古希腊，亚里斯多德就研究了主谓形式的模态命题和由它们所构成的模态三段论。在现代，对一阶模态逻辑(通常又称谓词模态逻辑) 的研究开始于巴肯 (R. C. Barcan) 和卡尔纳普 (R. Carnap) [4] [12]。由于在直观的理解上以及语义解释上遇到种种困难，因而一阶模态逻辑的发展较为
缓慢。跟命题模态逻辑相比，它还有待进一步的完善。
1必然性有两种使用：一种是必然模态词，二种指一般的模态词。在后种意义下，自然就有“各类必然性”一说。
一阶模态逻辑是在经典的一阶逻辑基础上增加两个模态算子：必然算子□和可能算子◇而形成的扩张。如果对命题模态逻辑作量化扩张, 则也会形成一阶模态逻辑[52]。由于一阶模态逻辑不仅研究命题之间的形式结构，还要研究命题内部的形式结构，所以较命题模态逻辑产生了更多的问题。
在一阶模态逻辑中，引入了变量、常量符号、谓词符号、函数符号和量词来扩展命题模态逻辑。模态算子作用在谓词和公式上，其真值依赖于自变元的取值。一阶模态逻辑的语义仍然是可能世界语义。与经典的一阶逻辑不同的是，由于在可能世界语义的一个框架 F=
∈中，我们都要对变量进行指派，对常量来自 W 中的多个可能世界，因此在每个可能世界w W
和谓词符号进行解释，并且在每个可能世界中的指派和解释都是经典一阶逻辑意义下的。这样就产生一个问题，即变量在这些不同可能世界中的指派是否可以不同？另外，常量和谓词符号在不同可能世界中的解释是否可以不同？对于这些问题，目前普遍接受的观点是常量和谓词符号在不同可能世界中的解释可以不同。但是，对于变量的赋值是否可以随可能世界变化而变化，则一直存在着很多的争议。在最早提出的克里普克的一阶模态逻辑语义中 [32]，变量在每个可能世界中的取值都必须相同，不随可能世界的变化而变化，即变量是严格的 (rigid)。然而，变量的严格指派会导致很多的问题，例如著名的晨星、昏星问题2[18]。
实际上，并没有理由要求变量一定得是严格的。如果我们在不同的可能世界中对变量指派不同的值并不会导致任何的不一致性。很多学者提出放宽对变量的严格指派，强调应该允许变量在不同的可能世界中取不同的值。比如在休斯（Hughes）等人所提出的偶然相等 CI 系统中 [30]，变量就是非严格的。另外，在阿洛尼（Aloni）提出的概念覆盖语义[1]、刘易斯的对应物（Counterpart）语义[35]、希尔肯（B. P. Hilken）的层模型[27] 以及费廷（M. C. Fitting）的一阶内涵逻辑中[18]，变量都被认为是非严格的。但是，如果一个变量可以在不同可能世界中被指派为不同的对象，这些不同的对象之间会有什么联系，如何刻画这种联系呢? 则又是当前的一阶模态逻辑语义研究中所面临的一个主要问题。
另外，在一阶逻辑中，我们只需要给定一个对象的论域。然而在可能世界语义中，由于我们要考虑多个可能世界，因此我们必须为每个可能世界都给定一个特定的论域。这样就产生一个问题，即不同的可能世界所对应的论域是否可以不同？这些不同的论域之间具有什么关系？在目前的一阶模态逻辑语义中主要采取下面三种方式来给定论域：不变论域 (constant domain)、递增论域和可
∈，都有D(w) = D(w′)，其变论域 (varying domain) [17]。不变论域是指对任意的可能世界 w, w′W
∈，若 wRw′，则 D(w)□D(w′)，中 D(w) 表示可能世界 w 的论域；递增论域是指对任意的 w, w′W
∈，其中R是W上的一个二元关系，wRw′表示从可能世界w可达w′；而可变论域则是指存在 w, w′W
使得 D(w)≠D(w′)。
3当前一阶模态逻辑语义所面临的问题
目前，一阶模态逻辑的语义研究中所面临的问题主要包括[52]：
（1） 模态词和相等符号的组合产生了必然相等与偶然相等 (contingent identity) 的问题以及模态词和个体项 (singular term) 的组合所产生的指称隐晦性 (referential opaque) 问题。
必然等同与偶然等同问题来自一个著名的难题：晨星和昏星问题。当我们在带相等符号的一阶逻辑上进行模态扩张时，就会得到定理 LI：x = y →□(x = y)。这个定理表示：对任意两个对象，只要它们相等，那么它们就必然相等。但实际情况并非如此，相等也可以是偶然的。比如说在晨星
2见下节（1）
和昏星问题中，我们把早晨在天空中出现的最亮的那颗星称为晨星，把黄昏时在天空中出现的最亮的那颗星称为昏星。如果我们把□解释成“古巴比伦人知道”，用 a 和 b 分别表示“晨星”和“昏星”，那么 a = b →□(a = b) 就是定理 LI 的一个实例。由于事实上晨星和昏星是同一个天体，因而 a = b 成立，再由MP 规则（即如果公式?成立，并且公式?→ψ也成立，那么我们可以推出公式ψ是成立的），我们可以得到□(a = b)，即古巴比伦人知道晨星和昏星是同一个天体，但实际上，古巴比伦人并不知道这是同一颗星，这就导致了一个矛盾。
一个个体项的指称即该个体项所表示或指示的事物或对象。通常认为，个体项除了具有指称之外还有含义 (sense)。在一个表达式中，一个个体项如果仅仅表示它的指称而不涉及到其含义，则称个体项在此处的出现为纯指称性出现，否则称为非纯指性称出现。我们把个体项在其中非纯指称性出现的语境(简称语境 context) 称为指称隐晦的语境 (referentially opaque context)，反之，称为指称透明的语境(referentially transparent context)。
一个表达式中如果含有模态词，那么该表达式中受模态词影响的部分(其辖域) 可称作模态语境。在一阶模态逻辑中，由于模态词的作用，会使得原来指称透明的语境变成指称隐晦的模态语境，我们称这类问题为指称隐晦性问题。指称隐晦性问题所带来的后果是使得一些常见的逻辑规律以及相应的推理失效。比如在模态语境中相等替换规则和存在推广规则 (existential generalization) 都不成立。
（2） 模态词和量词的顺序不同会形成意义不同的公式，由此产生了巴肯（Barcan） 公式及其逆公式的有效性问题。
在一阶模态逻辑中，模态词和量词的前后顺序不同会产生意义不同的公式，例如
□x◇P(x)的含义是：存在某个对象，它可能是P；
◇□x P(x)的含义是：“存在某个对象，它是P”是可能的。
由以上两式可以得到下面两个公式：
(a)□x P(x) → □x◇P(x)
(b)□x◇P(x) →◇□x P(x)
它们分别被称为巴肯公式 Bf和逆巴肯公式 Bfc[3][4]。在可能世界语义中，巴肯公式及其逆公式的有效性条件分别是：
(a)对任意可能世界w，Bf在 w 中为真，当且仅当 w 的任意可达世界w′中的所有对象
都在 w 中，即 D(w′)□D(w)，其中 D(w) 表示 w 中的所有对象的集合；
(b)对任意可能世界w，Bfc在 w 中为真，当且仅当 w 中的所有对象都在 w 的任意可达
世界w′中，即 D(w)□D(w′)。
（3） 模态词和一阶公式组合所产生的从物模态 (de re) 与从言模态 (de dicto) 问题。
从物模态与从言模态的差异可以通过这样的一个例子来看出，我们可以把公式 □(9 > 7) 解释成下面两种不同的形式：
(a)9 必然大于 7；和
(b)“9 大于 7”是必然的。
从物模态和从言模态分别属于事物和语言两个不同的层次，是两种不同的模态。由于这一不同，
在形式表达式中，模态词出现的位置与作用也不相同。在 (a) 中“必然”(从物模态词) 是以副词的形式出现，作为表示对象情况的成分参与到句子的形成中。这时的模态词是算子，使“必然大于”成为一个新的谓词。在 (b) 中“必然”(从言模态词) 是以形容词的形式出现，作为表示句子“9 大于7”的某一属性，形成一个关于“9 大于7”的命题，这时的模态词只是句子“9 大于7”的谓词。因此，从物模态和从言模态的区别也可以看成是模态词究竟是算子还是谓词的区别。
在一阶模态逻辑中，从形式上也把□□xP(x) 这类公式中的□看成从言模态词，而把□P(x) 或□x□P(x) 这类公式中的□看成从物模态词。区别在于□后面的公式是否含有自由变元，即通过判断模态词辖域里是否有自由变元来区分从物模态与从言模态。
（4） 由于可能世界语义在对从物模态的说明中承认了对象可以存在于不同的可能世界之中，也就是承认跨越不同可能世界的对象，从而导致了对象的跨界相等性和跨界识别 (transworld identity and transworld identification) 问题。
所谓跨界相等性和跨界识别问题就是指是否有在不同可能世界中同时存在(跨越不同可能世界) 的对象? 如果有，如何识别它们? 比如说在可能世界中的对象如何与现实世界中的对象相等。依据克里普克对“可能世界”做时间性的理解，苏格拉底在 20 岁时与他在 30 岁时，这两个不同时间上的对象如何相等? 依据不可辨别相等物原理3 (the indiscernibility of identicals，即两个相等的对象具有所有相同的性质)，苏格拉底既然是自我相等的，那么他在 20 岁时的性质与在 30 岁时的所具有的性质是一样的。这显然是错误的。对这一问题的解决方式有两种：
(a)借助于本质，苏格拉底在 20 岁时，与他在 30 岁时的本质相同，因而是相等的对象 (这
实际上违背了莱布尼茨的相等物不可辨别性原理)；
(b)将 30 岁时的苏格拉底看作 20 岁时的苏格拉底的一个对应物，两者之间不相等，但存
在直接的对应关系。
（5） 项的非存在 (non-existence) 和非指示 (non-designation) 问题以及项的严格性与非严格性(rigidity versus non-rigidity) 问题。
一阶模态逻辑中项的非存在和非指示问题是指当某个项所指示的对象在一个可能世界中不存在或者它根本就不可能指示一个对象时，我们应该怎样处理？我们在现实生活中经常会谈论一些事实上并不存在的人和事，比如我们会说嫦娥奔月、侦探福尔摩斯等等。那么在模态逻辑中，对于那些含有这些虚构人物的公式，我们怎么来确定其真值呢?
而项的严格性与非严格性问题则是指在可能世界语义中是否允许项在不同可能世界中指示不同的对象? 如果项在不同可能世界中所指示的对象可以不同，则称该项是非严格的(non-rigid)，否则称其为严格的 (rigid)。
前面讲到，对于常量和谓词符号，目前大家普遍认为它们是非严格的，即它们在不同可能世界中的解释可以不同。但是，对于变量是否是严格的，则存在着很多的争议，这一直以来就是一阶模态逻辑研究中的热点和难点。因而，变量的严格性与非严格性问题是当前的一阶模态逻辑语义研究中所面临的一个主要问题，也是最具挑战性的一个问题。针对这个问题，目前已经提出了很多种一阶模态逻辑系统。
4现有的一阶模态逻辑语义及其不足
3莱布尼茨律（Leibniz律，也称为相等物不可辨别原理the identity of indiscernibles）是说：如果两个对象具有所有相同性质，则两个对象是相等的。
为了解决第三节中我们所讨论过的在当前一阶模态逻辑语义研究中所面临的五大问题，到目前为止，逻辑学家们已经提出了很多种一阶模态逻辑的语义，分别用来解决上面的一个或者几个问题。下面，我们将就其中六种最具代表性的一阶模态逻辑语义进行详细的介绍。
（1）克里普克的一阶模态逻辑语义[32][33][34]。
这是最早出现的一类一阶模态逻辑语义，是由克里普克在 1963 年提出来的。系统的量化论域可以采用不变论域 (constant domain) 或者可变论域 (varying domain)，相应的模型分别称为不变论域模型或者可变论域模型。在克里普克的语义中，对变量的指派是独立于可能世界的，即对变量的指派不随可能世界的变化而发生变化，也就是说，变量是严格的 (rigid)。虽然这一点在很多情况下都是没有问题的，比如自然数肯定是严格的，但是变量的严格指称也会导致一些问题，例如我们前面所讨论过的晨星和昏星问题。在这一语义中谓词符号则是非严格的。
在一个克里普克的模型中，下面两个公式是有效（Valid）的：
LI：x = y→□(x = y) 和 LNI：x≠y → □(x≠y)
在现实世界中，晨星 =昏星，因此如果变量 x 和 y 都被指派为表达式“晨星”和“昏星”在现实世界中所指示的对象(即金星)，那么□(x = y) 肯定成立，因为这时只涉及到一个对象，即金星。但是，我们如何来表示这样一种很自然的观点 ——“晨星”和“昏星”可能并不相同，正如古巴比伦人所认为的那样。在这里，我们实际上是无法做到这一点的。
造成这个问题的主要原因就是在克里普克的语义中变量是严格的。实际上，并没有理由要求变量一定得是严格的。在不同的可能世界中对变量指派不同的值并不会导致任何的不一致。但是这样一来又会导致这种指派似乎完全是任意的和人工的。因为变量在语义和语法上都是无结构的，它的取值完全取决于对它的指派。
格尔森（J. W. Garson）和休斯等就给出三个理由来支持变量的非严格性[24][30]。休斯和克瑞斯韦尔（M. Cresswell ）还提出了一种被称为偶然相等系统的一阶模态逻辑语义。在偶然相等系统中，变量就是非严格的。
（2）偶然相等CI ( Contingent Identity) 系统[29][30]。
休斯和克瑞斯韦尔等人的偶然相等系统认为在克里普克的语义中成立的公式 LI 和 LNI 实际上是不可接受的。他们通过找出公式LI 和 LNI 的反例，提出我们需要重新来定义克里普克语义中对变量的指派方式。
在 CI 系统中，对变量的指派不再是一个从变量集合到对象论域 D 的函数，而是一个从变量集合到个体概念 (individual concepts) 集合的函数，而每个个体概念都是一个从可能世界集合 W 到对象论域 D 的全函数。由于个体概念在不同可能世界的取值可能不同，使得变量的取值也随着可能世界的变化而变化，即变量是非严格的。常量符号、函数符号和谓词符号也都是非严格的。系统的量化在所有个体概念的集合上进行，而不是直接在论域D 上进行[30]。
虽然 CI 系统极大地放松了克里普克语义中对变量的严格指称，从而可以解决类似于晨星和昏星的问题，但是这种过度的放松也带来了一些不好的副作用：在 CI 系统中所有的个体概念都可以作为对象来赋给变量，这明显是不合适的。比如说 CI 系统中可能会出现这样的个体概念，它在可能世界 w 中的取值为“David Lewis”，在w′中的取值为“a rock”，而在w′′中的取值为“a blade of grass”，其中w R w′且w′ R w′′。这明显是与我们的直观相违背的，因为一个可能世界中的人（刘易斯）到另外一个世界中去不可能变成一块石头。
休斯等人在他们的文章中也提到，如果不加选择地把所有的从W到D的函数都看作个体概念放
∈看作个入个体概念的集合中，或者只把从W到D的所有单值函数(即对所有 w W
∈，i(w) = d D)
体概念放入个体概念的集合中，都是不合适的 [30]。前者会造成上面所说的难题；而后者实际上又回到了克里普克的语义，因为这时由于个体概念和论域中的对象一一对应，在个体概念集合中取值就等价于从论域 D 中取值。休斯等人提出的解决方法是让模型来决定什么样的从W到D的函数应该看作个体概念，什么样的函数不应该看作个体概念，即对这些函数采取一种不平等的态度。
但是，我们认为让模态逻辑的模型本身来决定什么样的函数可以作为个体概念是不现实的，因为这不是模态逻辑本身所能解决的，它超出了逻辑所讨论的范围[50]。
（3）概念覆盖 (conceptual cover) 语义 [1]。
该语义是由阿洛尼在 2001年提出的。阿洛尼分析了克里普克语义以及偶然相等系统对于“Double Vision”等七个命题态度报告难题的解决能力。一个命题态度是一个人和一个命题之间的一种心理学上的关系。信念 (Belief)、期望 (desire)、意图 (intention)、发现 (discovery) 和知识(knowledge) 等等都是人和命题之间心理学上的关系 [39]。当我们报告 (report) 其他人的命题态度时，我们会发现很多的问题。比如相等替换规则和存在推广规则在命题态度报告中可能是不成立的[21][22]。对于命题态度报告难题的研究，一直是哲学家和逻辑学家们关注的一个焦点 [22][23][44][39]。到目前为止，已经有很多的难题被提出。
阿洛尼认为如果我们只是以从物模态的方式来理解命题态度报告，那么克里普克语义就可以解决相等替换规则和存在推广规则在命题态度报告中失效的问题[1]。但是克里普克语义对于其他的很多难题无法给出一个好的解决方法，比如“Double Vision”难题在克里普克语义中就是无法解决的[44]。
“Double Vision”难题
假定拉尔夫（Ralph）隐约的看见一个戴着棕色帽子的男人，由于某种迹象使得拉尔
夫怀疑他是一个间谍。另外还有一个灰白头发的男人，拉尔夫模糊地记得他是当前政府的
一个重要人物，除了有一次在海滩上，拉尔夫从未见过他，拉尔夫肯定不会认为这个人是
一个间谍。但是拉尔夫并不知道这两个人实际上是同一个人——奥特卡特（Ortcutt）。
这样，就会出现一个矛盾：一方面，拉尔夫相信戴着棕色帽子的男人是间谍，而这个
人是奥特卡特，所以拉尔夫相信奥特卡特是个间谍；另一方面，拉尔夫相信那个他在海滩
上见到的灰白头发的男人不是一个间谍，可是这个人也是奥特卡特，所以拉尔夫不相信奥
特卡特是一个间谍。拉尔夫不是一个逻辑混乱的人，他不可能同时相信一个人是间谍，又
不相信这个人是间谍。
对于“Double Vision”难题的解决，目前已经提出了很多种方法，比如偶然相等系统。偶然相等系统可以很好地解决“Double Vision”难题，但是它无法解决“最矮间谍”和“俄罗斯总统”等难题 [31] [1]。因此，阿洛尼进一步将偶然相等系统分为两种：CIA （Contingent Identity A）系统和 CIB （Contingent Identity B）系统。这两者的主要差别是：在 CIA 系统中变量的取值是在所有个体概念的集合 IC（Individual Concept）上进行；在 CIB 系统中，变量的取值不是在所有个体概念的集合 IC上进行，而是在 IC 的一个子集上进行，这个子集被称为合格的个体概念集合[1]。在 CIB 系统中，通过将一部分可能引起问题的个体概念从个体概念论域中去掉，来避免“最矮间谍”和“俄罗斯总统”等难题的发生。但是 CIB 系统还是不能解决所有的问题，比如“Odette 的情人”、“Susan 4。
的母亲”以及剧院难题[6][7]
4这些“难题”和前面的“Double Vision”难题类似，即仅用某种逻辑推理会形成悖论。
因此，阿洛尼最后提出了概念覆盖语义[1]，用来解决上面所有这些难题。
在概念覆盖语义中，一个概念覆盖 (conceptual cover，CC) 是满足这样条件的一组个体概念的集合：对于每个概念覆盖 CC 以及任意一个可能世界w，对象论域中的每个对象在 w 中都实例化CC 中唯一的一个概念。即给定一个可能世界集合 W 和对象论域D，基于 (W，D) 的概念覆盖 CC 是一个由从 W 到 D 的函数所组成的集合，使得
□w ∈W：□d ∈D：□! c∈CC：c(w) = d，
其中□! 是唯一存在量词。
即对于W中的每个可能世界w，对象
论域D中的每个对象d在w中都与概念覆
盖 CC中的一个概念c存在一一对应关系，
即D中的每个对象d都对应于CC中的唯
一的一个概念c，使得d = c(w)；并且CC
中的每个概念c都对应于D中的唯一的一
个对象d，使得c(w) = d。具体的情形如图所示：
因此, 概念覆盖是由那些完全且唯一覆盖对象论域的概念所组成的集合。在一个概念覆盖中，每个对象在每个可能世界中都有且仅有一个概念和它存在映射关系。这样，每个概念覆盖都和对象论域具有相同的基数。不同的概念覆盖构成对同一个对象论域的不同的表达方式。
前面讲到，在偶然相等系统 CIA 中，对于变量的指派没有任何限制，变量在每个可能世界中都可以取论域中的任何值，不用考虑它在当前世界的取值和它在其他世界中的取值之间是否有什么联系[50]。
在偶然相等系统 CIB 中，对变量指派的限制有所加强，即去掉了一些我们认为是不合格的个体概念。但是具体的哪些个体概念合格或不合格，则没有一个好的评价标准。我们有可能把本来是合格的个体概念当作不合格的个体概念去掉了；而把那些在不同世界的取值之间的联系不符合客观实际的个体概念保留下来。在 CIB 系统中，完全是由模态逻辑模型来确定合格的个体概念集合，但是模型本身是很难做到一点的[50]。
在概念覆盖语义中，对变量指派的限制也比 CIA 系统有所加强，但是它只是要求在每个可能世界 w 中每个概念覆盖中的概念 c 和对象论域 D 中的唯一的一个对象 d 存在对应关系，但对这个 d 本身仍然没有作任何限制，即 d 仍然可以是 D 中的任何一个对象。这里仍然没有考虑 c 在其他可能世界的取值对 d 是否有影响、如何影响等问题。所以在这里，仍然有可能出现这样的情形, 即 c 在可能世界 w 中的取值为“David Lewis”，在w′中的取值为“a rock”，而在w′′中的取值为“a blade of grass”，其中w R w′且w′ R w′′。
（4）对应物语义[35][36][37][38]。
该语义最初是由刘易斯在 1968 年提出的。他对于克里普克语义中变量的严格指称提出了置疑，于是提出了一个更为宽松的模态语义：不要求当前可能世界中的对象在其他的可能世界中也必须存在，而仅要求有一些和它相对应的对应物 (counterpart) 存在于这些可能世界中。该对象和它的对应物之间具有跨越不同可能世界的对应物关系。当前可能世界中的一个对象在其他可能世界中可以有多个对应物，也可以是多个对象对应于其他可能世界中的同一个对应物。这就在语义上提供了更大的灵活性[35] [18]。
在对应物语义中，个体只能是限界的个体 (bound world individual)，即一个个体不能存在于不同的可能世界中，而是只能存在于单个的可能世界中。所以，在刘易斯的理论中，每一个可能世界都有它自己的量词域，而所有的对象都没有跨越世界的相等性，但可能世界中的对象之间却有跨越可能世界的对应物关系。对于如何确定对应物关系的问题，即跨界识别问题，刘易斯是这样定义的 [35]：
对于w中的d和w′中的d′，只有当w′中没有任何对象比d′更类似于w中的d时，d′才是w中的d在w′中的对应物。
对应物语义的不足之处在于它无法用形式的模态语言来说明为什么不同可能世界中的对象之间会有这样的和那样的对应物关系。我们无法对对应物关系进行合理的限制 [50]。刘易斯认为对应物关系是一种近似 (similarity) 关系，但是由于近似关系一般情况下是无法确定的，所以对应物关系也是无法确定。因此在这里，很可能出现这样违背直观的情形，即 w 中的“David Lewis”，w′中的“a rock”，以及w′′中的“a blade of grass”这三者之间具有对应物关系, 其中w R w′且w′ R w′′。这明显是不合理的。
（5）层模型 (sheaf model) [27]。
层模型是由希尔肯等人在 1999 年为解决变量的严格指称与非严格指称问题而提出的。他们认识到现有的一阶模态逻辑语义在处理变量的非严格指称上存在困难。假设?是一个带有自由变元x 的公式，x 在每个可能世界中都指称一个对象。如果 x 在不同可能世界中所指称的对象可以不同，那么在命题□?中，□?表示?在所有当前世界可达的世界中都成立，这样 x 在这些当前世界可达的世界中的指称就会发生变化。而这种指称的变化则可能引起变量替换的问题。因此，(□?) [t=x] 和□(? [t=x]) 可能不是都有定义或者可能不等价。同样的，量词的范围也可能发生变化。比如说，在□x□?中，量化是在当前世界的所有对象上进行的；而在□(□x?) 中，量化是在当前世界可达的世界中的所有对象上进行的 [27]。
现有的一阶模态逻辑语义在处理变量的严格指称与非严格指称问题时通常采取的做法是限制模态逻辑的模型，即要求每个世界中的对象在任意该世界可达的世界中都必须存在，也就是说，模型的论域必须是递增的。甚至于有的系统要求所有可能世界的论域都是相同的，即只讨论常论域模型。然而这些做法是很难令人满意的。首先，它们都缺少一个逻辑的工具来处理变量的非严格指称，既没有任何符号也没有任何推导规则；其次，它们对模型的限制太苛刻：模态逻辑本来应该是一种用来处理变化的、动态情形的逻辑，然而我们恰恰限制了其核心—— 模型的论域不能改变。另外，虽然模态逻辑中采用了一种语言来描述对象的子集，即命题语言，但却没有一种语言用来描述不同可能世界中的对象之间的关系。这种关系实际上也是一个子集，是多个对象集合的笛卡儿集的子集[27]。
希尔肯的层模型语义可以有效地避免现有的一阶模态逻辑语义对模型的论域所施加的种种不合理限制，其关键思想是引入另外一种语法机制，通过提供一种语言来描述不同可能世界中的对象之间的联系。具体做法是通过定义多种形式的跨越（transition）命题，这些命题中包括来自不同可能世界中的项，从而建立起这些项之间的联系。这在一定程度上解决了变量的严格指称与非严格指称问题，而且还使得系统具备更强的逻辑表达能力。但是作者并没有给出该系统在可靠性和完备性方面的结果。
（6）一阶内涵逻辑(first order intensional logic) FOIL [18][19][20]。
费廷在 2004 年提出了一个他称之为一阶内涵逻辑 FOIL 的一阶模态逻辑语义[19]。费廷认为目前对一阶模态逻辑语义的研究大体上分为两种途径：基于对应物关系的方法和基于内涵对象的方
法。其中基于对应物关系的方法起源于刘易斯等人的工作 [35]；而内涵对象则可以追溯到蒙太古（R. Montague）[40]。经典逻辑只考虑推理过程的思维形式，涉及的只是推理表达式的外延。现代逻辑有些分支不但顾及外延，而且关注内涵，并注意到外延与内涵的相互关系。蒙太古建立的蒙太古内涵逻辑系统(即“蒙太古语法”) 是迄今最具代表性的内涵逻辑[40]。内涵逻辑将内涵定义为：“从可能世界(即可能的情况) 到外延的函数。”这样，我们就可以借助内涵来识别在各种可能的情况下(即“可能世界”) 可作为表达式外延的那些对象。相应地，外延则是函数的取值。因此，内涵就可以离散地、形式化地表达和演算。
在费廷的一阶内涵逻辑中，量词的量化论域中除了包括一般的个体对象之外，还包括内涵(或概念)。因此，在每一个 FOIL 的模型中都有两个论域：对象论域 DO 和内涵论域 DI，其中 DI 中的每个内涵都是一个从可能世界集合 W 到对象论域 DO 的函数。另外在 FOIL 中有两种类型的变量：对象变量和内涵变量。模型中的任意一个变量指派μ都将对象论域中一个的对象指派给对象变量，将内涵论域中的一个内涵指派给内涵变量。对象变量是严格的，它所指示的对象不随可能世界的变化而变化。由于内涵在不同的可能世界中可以指定不同的对象，因而使得内涵变量在不同的可能世界中也可以指定不同的对象，即内涵变量是非严格的。在后来的文章中，费廷进一步给出了 FOIL 的一个公理化系统并且证明了其可靠性与完备性[20]。
然而，FOIL 和前面的偶然相等系统以及概念覆盖语义面临同样的问题, 即到底哪些从W 到DO 的函数应该看作是内涵。费廷在文章中也提到，不应该要求内涵论域 DI 中包括所有从 W 到DO 的函数。不是所有数学上可能的东西都可以看作是一个内涵。另外，如果我们把所有从 W 到DO 的函数都放入内涵论域 DI 中，则会造成在我们的系统中，一个完全的证明过程几乎无法得到，正如我们在对二阶逻辑进行公理化时所遇到的问题[19]。
既然不能把所有从 W 到 DO 的函数都放入 DI 中，那么我们应该选择哪些函数呢? 费廷并没有给出一个好的解决方法。和休斯等人的做法一样，他实际上也是把这个问题推给了模型本身。这样，这里的问题和前面的偶然相等系统中的问题一样，让模型来决定什么样的从 W 到 DO 的函数应该看作内涵，什么样的函数不应该看作内涵，在很多时候模型本身是很难做到一点的。因为这个问题不是模态逻辑本身所能解决的，即这个问题超出了逻辑所讨论的范围。所以很显然的，模态逻辑在解决这个问题时就会遇到其自身无法解决的困难[50]。
5结束语
在由一阶逻辑或者命题模态逻辑向一阶模态逻辑的扩张过程中引发了很多的问题。而这些问题在以往的经典逻辑中往往是不存在的。因此，甚至有人对于模态逻辑本身的合理性产生质疑。比如奎因 (W. V. Quine) 就提出了模态逻辑所面临的哲学问题，他指出模态逻辑违反了经典谓词逻辑的基本原则[45][46]。例如，在经典谓词逻辑中，我们有相等替换规则(substitutivity of identicals)，其形式表示为：(a = b)∧F(a) → F(b)。这一原理规定：给定一个关于同一性的真陈述，可以用它的两个项中的一个替换另一个出现在任一真陈述中的项，而其结果将是真的 [49]。相等替换规则在经典谓词逻辑中是普遍有效的，但是奎因认为，在模态逻辑语境中它不再普遍成立。奎因给出下面的一个例子 [49]：
（1） 9 必然大于 8；
（2） 行星的数目= 9。
我们大家都知道，就在 2006 年的 8 月 24 日，国际天文学联合会大会通过决议，将地位备受争议的冥王星“开除”出太阳系行星行列，太阳系行星数目也因此降为 8 颗。因此，在 2006 年的 8 月 24 日之前(或者说在奎因论述这个问题的时候)，(1) 和 (2) 都是真命题，运用相等替换
规则，我们可以得到
（3） 行星的数目必然大于8。
如果从时态的角度来理解必然，(3) 表示在任何时候，行星的数目都大于8。显然， (3) 应该被认为是不成立的，因为行星的数目在2006 年的 8 月 24 日之前大于8，但是从2006 年的 8 月24 日起就不再大于8。因此，在2006 年的 8 月 24 日之前，对于 (1) 和 (2)，我们无法使用相等替换规则推出 (3)，因为我们无法知道今后行星的数目会不会改变（事实上就发生了改变）。
奎因认为这是由于模态词造成指称上的隐晦性 (referential opaque) 所致。另外，指称的隐晦性不仅可由“必然”、“可能”这样的模态词造成，还可由“知道”、“相信”、“怀疑”等表示信念的一类模态词造成。
由于人们在对一阶模态逻辑语义的研究过程中遇到了很多在经典逻辑中从未碰到过的困难和问题，并且这些问题和现实世界中的各种现象都是息息相关的，因此要解决这些问题需要我们不断的探索和研究。
参考文献
[1]M. Aloni, Quantification under conceptual covers, Ph. D. thesis, Univ. of Amsterdam, 2001.
[2]L. Aqvist, Deontic Logic, In Dov M. Gabbay, F. Guenthner (eds.): Handbook of Philosophical Logic, Second
Edition, vol. 8, 2002.
[3]R. C. Barcan, The deduction theorem in a functional calculus of first order based on strict implication. Journal
of Symbolic Logic, 11: 115-118, 1946.
[4]R. C. Barcan, The identity of individuals in a strict functional calculus of second order. Journal of Symbolic
Logic, 12: 12-15, 1947.
[5]G. V. Bochmann, Hardware specification with temporal logic: an example, IEEE Transactions on Computers,
vol. C-31, 223-231, 1982.
[6] A. Bonomi, Eventi Mentali. II Saggiatore. Milano, 1983.
[7] A. Bonomi, Transparency and specificity in intensional contexts. In P. Leonardi and M. Santambrogio (eds),
On Quine, New Essays. Cambridge University Press, 164-185, 1995.
[8]G. Boolos, The Logic of Provability. Cambridge University Press, 1993.
[9]R. Brafman, J. C. Latombe, Y. Moses, and Y. Shoham, Knowledge as a tool in motion planning under
uncertainty. In: Proceedings of the 5th conference on theoretical aspects of reasoning about knowledge,
California, 208-224, 1994.
[10]M. Burrows, M. Abadi, and R. Needham, Authetication: a practical study in belief and action, Proceedings of
the 2nd conference on theoretical aspects of reasoning about knowledge, 325-342, 1988.
[11]M. Burrows, M. Abadi, R. Needham, A logic of authentication. Research Report 39, Digital Systems Research
Center, 1989.
[12]R. Carnap, Meaning and Necessity. Chicago University Press, 1947.
[13]J. M. V. Castilho, M. A. Casanova, and A. L. Furtado, A temporal framework for database specification,
Proceedings of the 8th international conference on very large databases, 280-291, 1982.
[14] E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using
temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol. 8, 244-263,
1986.
[15]J. Clark, J. Jacob, A survey of authentication protocol literature.
https://www.doczj.com/doc/de4257484.html,/~jac/papers/drareviewps.ps, 1997.
[16] A. Dawar, S. Lindell, and S. Weinstein, Infinitary logic and inductive definability over finite structures,
Information and Computation, 119, 160-175, 1995.
[17]M. C. Fitting, and R. Mendelsohn, First-order modal logic, Kluwer, 1998.
[18]M. C. Fitting, On Quantified Modal Logic. Fundamenta Informaticae, 39(1-2) (1999) 105-121.
[19]M. C. Fitting, First-order intensional logic, Annals of Pure and Applied Logic, 127: 171-193 (2004).
[20]M. C. Fitting, FOIL Axiomatized. Unpublished Manuscript,
https://www.doczj.com/doc/de4257484.html,/fitting/bookspapers/modal.html, 2006.
[21]G. Frege, Correspondence with Russell, in N. Salmon and S. Soames (eds.), Propositions and Attitudes.
(Oxford: Oxford University Press, 1988), 1904.
[22]G. Frege, “Sense and reference”. Philosophical Review. 57: 209-230, 1948. [originally published in 1892].
[23]G. Frege, “The thought: A logical inquiry”. Mind. 65: 289-311, 1956. [originally published in 1918].
[24]J. W. Garson, Quantification in modal logic. In: Handbook of Philosophical Logic, Kluwer Academic
Publishers, Dordrecht, 267-323, 2001.
[25]J. Y. Halpern and Y. Moses, Knowledge and common knowledge in a distributed environment, Journal of the
ACM, vol. 37, 549-587, 1990.
[26] D. Harel, J. Tiuryn, D. Kozen, Dynamic Logic, The MIT Press, 2000.
[27] B. P. Hilken, Sheaf models of predicate intuitionistic modal logic I: Relational sheaves, In preparation:
Department of Computer Science, Manchester University, 1999.
[28]J. Hintikka, Knowledge and Belief: An Introduction to the Logic of the Two Notions. Cornell University Press,
1962.
[29]G. E. Hughes, and M. J. Cresswell, An Introduction to Modal Logic, London: Methuen, 1968.
[30]G. E. Hughes, and M. J. Cresswell, An New Introduction to Modal Logic, London: Routledge, 1996.
[31] D. Kaplan, Quantifying in. in D. Davidson and J. Hintikka (eds), Words and Objections: Essays on the Work of
W. V. Quine. Reidel. Dordrecht. 221-243, 1969.
[32][Kripke 1963] S. Kripke, Semantical considerations on modal logics. In: Acta Philosophica Fennica, Modal
and Many-valued Logics 16, 83-94, 1963.
[33][Kripke 1971] S. Kripke, Semantical considerations on modal logic. In L. Linsky, editor, Reference and
Modality, pages 101-111. Oxford University Press, Oxford, 1971.
[34]S. Kripke, Naming and Necessity. Harvard University Press, Cambridge, 1980.
[35] D. Lewis, Counterpart theory and quantified modal logic, Journal of Philosophy, 65: 113-126, 1968.
[36] D. Lewis, Counterparts of persons and their bodies, Journal of Philosophy, 68: 203-211, 1971.
[37] D. Lewis, Counterpart theory and quantified modal logic. In M. Loux, editor, The Possible and the Actual,
pages 110-128. Cornell University Press, N. Y., 1979.
[38] D. Lewis, On the Plurality of Worlds. Blackwell, Oxford, 1986.
[39]T. McKay, Propositional attitude reports, Stanford Encyclopedia of Philosophy, 2000.
[40]R. Montague, Pragmatics and Intensional Logic, Synthese, 22: 68-94, 1970.
[41] A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE symposium on foundations of
computer science, 46-57, 1977.
[42]V. R. Pratt, Semantical considerations on Floyd-Hoare logic, Proceedings of the 17th IEEE symposium on
foundations of computer science, 109-121, 1976.
[43] A. N. Prior, Time and Modality. Oxford University Press, Oxford, 1957.
[44]W. V. Quine, Quantifiers and propositional attitudes. Journal of Philosophy, 53. Reprinted in Marras, A. (ed.)
(1972) Intentionality, mind and language. Urbana: University of Illinois Press. 402-414.
[45]W. V. Quine, Reference and modality. In L. Linsky, editor, Reference and Modality, pages 17-34. Oxford
University Press, Oxford, 1971.
[46]W. V. Quine, Worlds away. Journal of Philosophy, 73: 859-863, 1976.
[47]J. H. Reif and A. P. Sistla, A multiprocessor network logic with temporal and spatial modalities, Proceedings
of the 12th international colloqium on automata, languages, and programming, Lecture Notes in Computer
Science, vol. 104, Springer Verlag, 1983.
[48]弓肇祥, 可能世界理论, 北京大学出版社, 2003 年.
[49]奎因, 从逻辑的观点看, 上海译文出版社, 1987 年.
[50]江峰, 基于本体的一阶模态逻辑研究, 中国科学院计算技术研究所, 博士论文, 2007.6.
[51]王震宇, 可能世界与智慧, 机械工业出版社, 2005 年.
[52]周北海, 模态逻辑导论, 北京大学出版社, 1997 年.
[53]周礼全, 模态逻辑引论, 上海人民出版社, 1986 年.
作者简介：
江 峰： 中国科学院计算技术研究所博士研究生。主要研究方向是人工智能、模态逻辑。
眭跃飞： 中国科学院计算技术研究所研究员，博士生导师。主要研究方向为人工智能、计算机科学中的逻辑。
曹存根： 中国科学院计算技术研究所研究员，博士生导师。主要研究方向为人工智能、大规模知识获取与知识表示。