转自“硬科普
模态逻辑的语义考量
作者:索尔·A·克里普克
译者:Sub(y,17,y)
本文阐述了模态逻辑语义理论的一些特征¹。在S5的某个量化扩展中,该理论已在[1]中提出,并在[2]中进行了总结。本文将集中讨论该理论的一个方面——引入量词,并将主要限制于实现这一目标的一种方法。本文的重点将完全是语义的,因此将省略使用语义表的部分,而语义表对于理论的完整呈现至关重要。(关于语义表,请参见[1]和[11]。)此外,证明过程在本文中也将大部分被省略
我们考察四个模态系统。公式 是由原子公式,以及连接词 和 构建的。系统 具有以下公理模式和规则:
A1.
A2.
R1.
R2.
如果我们添加以下公理模式,则得到S4:
如果我们在 中添加以下公理,则得到Brouwersche 系统:
如果我们添加:
则得到S5系统。
¹ 此处所述的理论与许多作者有联系:关于这些作者的列表,请参见[11]和Hintikka [6]。与目前理论最接近的作者似乎是Hintikka和Kanger。然而,就我所知,目前关于量化的处理方法是独特的,尽管它从Prior和Hintikka截然不同的方法中汲取了一些灵感。
那些其定理在规则和下闭合,并包含系统 所有定理的模态系统,被称为“正常(normal)”系统。尽管我们已经发展出适用于Lewis的和等非正常系统的理论,但我们在此将自己局限于正常系统。
为了给模态逻辑提供语义,我们引入(正常)模型结构的概念。一个模型结构(m.s.)是有序三元组,其中 是一个集合, 是 上的自反关系,。直观上,我们可以这样理解: 是所有“可能世界”的集合; 是“真实世界”。如果 和 是两个世界, 的直观含义是相对于 是可能的;也就是说,在 中为真的每个命题在 中都是可能的。因此,关系 必须是自反的;因为每个世界 对自身而言是可能的,因为在 中为真的每个命题在自身中自然也是可能的。自反性因此成为直观上自然的要求
我们可以施加额外的要求,来对应模态逻辑的各种“归约公理”:如果 是传递的,则 是模型结构;如果 是对称的, 是Brouwersche 模型结构;而如果 是等价关系,我们称 为模型结构。不加任何限制的模型结构也被称为-模型结构。
为了完善这个理论框架,我们还需要模型的概念。给定模型结构,一个 **模型*给每个原子公式(命题变量) 在每个世界 中赋予一个真值 或。形式上,一个模型 在模型结构 上是一个二元函数,其中 在原子公式中变化,而 在 的元素中变化,其值域是集合。
给定一个模型,我们可以通过归纳法定义非原子公式的真值分配。假设对所有, 和 已经被定义。如果,则定义;否则,。 定义为,当且仅当;否则,。最后,我们定义,当且仅当对所有 且,;否则,。直观上,这意味着 在 中为真,当且仅当 在相对于 的所有世界 中都为真。
完全性定理
在(,, 及 Brouwersche 系统) 中,当且仅当对于任意模型,有,其中 是一个(、、Brouwersche)模型结构,则 可证明(记作)。
(关于证明,请参见[11]。)
这个完全性定理将模态系统中语法上的可证性 概念与语义上的有效性 概念等同起来。
本文的其余部分,除了一些特定的讨论外,将继续围绕这一点展开。
为了引入量词,我们必须将每个世界与一个个体域相关联,也就是存在于那个世界的个体。形式上,我们将一个量化模型结构(q.m.s.)定义为模型结构,再加上一个函数,该函数将每个 映射到一个集合,称之为 的域。直观上, 是存在于 中的所有个体的集合。当然请注意, 不必对不同的 具有相同的集合,就像直观理解的那样,在某些不同于真实世界的世界中,一些实际存在的个体可能缺席,而新的个体(如飞马)可能出现。
接着我们可以在模态逻辑的符号中,加入无限个个体变量,对于每个非负整数,引入-元谓词字母。这些上标在上下文中有时可以忽略。我们将命题变量(原子公式)视作“零元”谓词字母。然后,我们用通常的方式构建良构公式,现在我们可以定义一个量化模型。
要定义量化模型,我们必须扩展原有的概念,该概念将真值分配给每个世界中的原子公式。类似地,我们必须假设,在每个世界中,给定的-元谓词字母决定了该世界中有序-元组的集合,即谓词在该世界中的外延。例如,考虑单一谓词字母。我们希望说,在世界 中,谓词 对 中的某些个体为真,而对其他个体为假;形式上,我们可以说,相对于 中元素的特定分配,如果,则为真;而对于其他分配。在 中 为真的所有个体的集合被称为 在 中的外延。
但这里出现了一个问题:当 被分配为某个其他 世界 中的值,而非 的域时, 是否应当被赋予一个真值?直观上,假设 意味着“ 是秃头的”——我们如何为替换实例“福尔摩斯是秃头的”分配真值?福尔摩斯并不存在,但在其他状态下,如果他存在,他就会存在。我们是否应该为“他是秃头的”这一陈述分配明确的真值?弗雷格[3]和斯特劳森[4]不会为该陈述分配真值;罗素[5]则会¹。
¹罗素 认为,“福尔摩斯”因此不是真正的名字;弗雷格 则会排除这种空名,视其为人为构造。
对于这个问题的答案,代表了各种替代性约定。所有约定都是可以接受的。我所见过的关于该问题的现有讨论,出现在Hintikka [6] 和 Prior [7] 的著作中——他们都采用了弗雷格-斯特劳森的观点。这一观点必然导致对通常的模态逻辑进行某些修改。原因在于,我们之前给出的模态命题逻辑的语义假设,每个公式在每个世界中都有一个真值;然而,现在对于包含自由变量 的公式,弗雷格-斯特劳森的观点要求,当 被赋予一个不属于该世界 域的个体时,它不被赋予一个真值。
因此,我们不能再期望模态命题逻辑的原始规律适用于包含自由变量的陈述,我们面临着一个选择:要么修正模态命题逻辑,要么限制替换规则。 采取了前者,而 选择了后者。弗雷格-斯特劳森的选择涉及更多替代方案:我们是否应该将(在 中)理解为 在所有可能世界中(相对于)都为真,还是只要在任何这样的世界中不为假?第二个选择仅要求 在每个世界中要么为真,要么缺少真值。
在 的系统 中,实际上承认了两种必然性,一种是,另一种是。类似的问题也出现在合取中:如果 为假且 没有真值,那么我们是否应当将 看作是假的还是无真值的?
在对语义理论的完整陈述中,我们将探讨弗雷格-斯特劳森观点的所有变体。在这里,我们将采取另一种选择,假设包含自由变量的陈述,对于自由变量的每个赋值,在每个世界中都有一个真值¹。形式上,我们如下表述该问题:令 是 的第 个笛卡尔积。我们在量化模型结构 上定义一个量化模型作为一个二元函数。
¹ 自然地,我们可以假设,在世界 中,一个原子谓词在那些不存在的个体上为假;也就是说,谓词字母的外延必须仅由实际存在的个体组成。我们可以通过语义上要求 来实现;这种语义处理方式在其他方面不会发生改变。但如果这样做,我们必须将所有形如 的公式的闭包添加到公理系统中。我们选择不这样做,因为替换规则将不再成立;定理对原子公式成立,但在将原子公式替换为任意公式时不再成立。(这回答了 Putnam 和 Kalmar 的一个问题。)
函数 中,首个变量取-元谓词字母, 是任意值,而 是 的元素。当 时,;如果,则 是 的子集。
现在,我们通过归纳法定义,对于每个公式 和每个,相对于自由变量 的元素 的给定赋值,赋予 一个真值。对于命题变量的情形是显然的。对于原子公式,其中 是-元谓词字母且,对于将元素 赋给 的情况,我们定义:
当且仅当否则,
给定这些原子公式的赋值,我们通过归纳法构建复合公式的赋值。对于命题连接词 的归纳步骤已经给出。假设我们有公式,其中 和 是唯一的自由变量,且对于每个自由变量赋值, 的真值已定义。那么我们定义:
当且仅当
对于 的赋值(其中 是 的元素),
对于每个元素,。
否则,。
注意, 的限制意味着,在 中,我们仅对实际存在于 中的对象进行量化。
为了说明语义,我们给出模态量化理论中两条著名提案的反例,即巴坎公式:
及其逆命题
对于每种情况,我们考虑模型结构,其中,,且 是 的笛卡尔积。显然, 是自反的、传递的且对称的,因此我们的讨论甚至适用于S5系统。
对于巴坎公式,我们将模型结构 扩展为量化模型结构,定义:
其中 和 是不同的。然后,我们定义单一谓词字母 的模型,使得:
因此,当将 分配给 时, 在 中为真;因为 是 的域中唯一的对象,所以 也在 中为真。然而,当将 分配给 时, 在 中显然为假(因为)。因此:
我们得到了巴坎公式的反例。
请注意,这个反例与是否将 赋予 中的真值无关,因此它同样适用于 Hintikka 和 Prior 的系统。这样的反例可以被禁止,巴坎公式也可被恢复,只要我们要求模型结构满足如下条件:
对于巴坎公式的逆命题,设,,其中。定义:
其中 是给定的单一谓词字母。于是 在 和 中都成立,因此。但是,当将 赋给 时,,因此当 被赋为 时:因此,,这就得到了巴坎公式逆命题的反例。
然而,这个反例依赖于这样一个断言:在 中,当 被赋予 时, 实际上为假。如果我们声明 在 中缺少真值,则反例可能消失。在这种情况下,如果我们要求一个必然陈述在所有可能世界中都为真( 的),我们仍然有反例;但如果我们仅要求它永不为假( 的),那么反例便消失。在我们当前的约定下,我们可以通过对每个量化模型结构要求 当 时,来消除反例。
这些反例导致了一个特殊的困难:在量化的 系统中,我们已经提供了反模型,使得巴坎公式及其逆命题均不成立。然而, 似乎在 [8] 中表明,巴坎公式在量化的 中是可导的;而逆命题甚至在量化的 中也可以通过以下论证推导出来:
(A)
(B)
(C)
(D)
(E)
(F)
我们似乎通过模型理论中应当有效的原则得出了这个结论。事实上,缺陷出现在对公式 (A) 应用必然性规则的过程中。在公式 (A) 中,我们假设...
对于自由变量的一般性解释¹:当 作为定理断言时,它代表了其通常的普遍闭包,即:
现在,如果我们将必然性应用于,就会得到:
另一方面, 本身的解释是断言:
要从 推导出,我们需要一个形式为 的规律,这正是我们试图证明的巴坎公式的逆命题。事实上,很容易验证,对于前面给出的逆巴坎公式的反模型,如果我们将 替换为, 就不成立。
如果我们遵循 [15] 的方法,可以避免此类困难,我们会构建量化理论,使得只有闭合公式被断言。断言包含自由变量的公式,最多是一种便利;断言含有自由变量 的 始终可以被 的断言替代。
如果 是一个包含自由变量的公式,我们定义 的闭包为任何通过在 前加上普遍量词和必然性符号(顺序任意)所获得的不含自由变量的公式。我们将量化系统 的公理定义为以下图式的闭包:
(0) 真值功能的重言式
(1)
(2)
(3),其中 在 中不是自由的。
(4)
(5)
¹ 并未断言,对包含自由变量的定理进行一般性解释是唯一可能的选择。人们可能希望,对于某个公式,如果对于每个模型, 对 的自由变量的每个赋值都成立,那么 就是可证明的。但在这种情况下, 将不再是一个定理;事实上,在上述的巴坎公式的反模型中,如果将,当 被赋予 时,量化理论将不得不按照 [9] 和 [10] 的思路进行修正。这种方法有很多优点,但我们没有采用,因为我们希望展示,这一困难可以在不修改量化理论或模态命题逻辑的情况下解决。
推理规则是对物质蕴含的分离规则。必然性可以作为一个导出规则获得。
要获得、 和 系统的量化扩展,只需将所有合适的归约公理的闭包加入公理图式中。
我们所得到的系统具有以下性质:它们是模态命题逻辑的直接扩展,无需 的 系统中的修改;替换规则在这里没有任何限制,与 的呈现不同;但巴坎公式及其逆命题均不可导。此外,所有量化理论的规律(经过修改以允许空域)依然成立。我们为模态命题逻辑提供的语义完全性定理可以扩展到这些新系统。
我们可以在当前系统中引入存在性作为谓词,如果需要的话。从语义上讲,存在性是一个一元谓词,对于模型结构,每个模型 满足:对于,有:在公理化层面,我们可以通过以下形式的公式的闭包来引入它:在上述反例中使用的谓词,现在可以被识别为简单的存在性。这一事实表明了存在性与重言谓词 的不同,尽管:是可证的,但:则不成立;虽然必然存在某物,但这并不意味着一切都具有必然存在的属性。
我们还可以在模型理论中语义性地引入同一性,通过定义 在世界 中为真,当且仅当 和 被赋予相同的值;否则为假。存在性也可以通过同一性来定义,规定 意味着:由于某些未在此处讨论的原因,如果我们复杂化量化模型结构的概念,可以获得更广泛的同一性理论。
我们以一些简要而粗略的备注结束,讨论可证明性的模态逻辑解释,这里仅限于命题演算的情况。如果读者略过本节,依然能掌握本文的核心内容。可证明性解释基于将必然性算子加入形式系统的愿望,例如在皮亚诺算术中,通过这样的方式,使得对于系统中的任何公式, 将被解释为当且仅当 是...
在系统中可证明。如果说这种可证明性解释的模态算子是可有可无的,那么可以转而使用可证明性谓词,将其附加到公式 的哥德尔编号上;但 Montague 教授对本书的贡献至少对这一观点投下了一些疑问。
让我们考虑皮亚诺算术(PA)的形式系统,如 Kleene [12] 所形式化的。我们在其构成规则中加入算子(合取)、(否定)和(必然性)。注意,这些添加的算子不同于原系统中的算子,它们仅作用于闭合公式。在我们之前给出的模型理论中,原子公式被看作命题变量,或带有括号的个体变量的谓词字母;在这里,我们将其视为PA 的闭合良构公式(而不仅仅是 PA 的原子公式)。
我们定义一个模型结构,其中 是所有不同(非同构)的PA 可数模型的集合, 是自然数中的标准模型, 是 的笛卡尔积。我们通过如下方式定义一个模型:对于任意原子公式 和,若 在模型 中为真(假),则:(请记住, 是PA 的良构公式,而 是PA 的一个可数模型。)然后我们像之前一样构建复合公式的赋值¹。要说 是真,就是说它在真实世界 中为真;对于任何原子公式,有:(注意, 当且仅当 在直观意义上为真。)由于 是一个 S5 模型结构,S5 的所有规律在这种解释中都有效。我们还可以证明,只有 S5 的规律是普遍有效的。(例如,如果 是哥德尔的不可判定公式,则:这是对“规律” 的反例。)
另一个可证明性的解释如下:我们再次将原子公式看作是PA 的闭合公式,然后通过加入的连接词、 和 构建新的公式。
¹ 可能有人会反驳说,PA 已经包含了合取和否定的符号,比如 “&” 和 “−”;那么我们为什么还要加入新的符号 “” 和 “” 呢?答案是,如果 和 是原子公式,那么 在当前意义上也是原子的,因为它在PA 中是良构的;但 不是。为了能够应用之前的理论(其中原子公式的合取不再是原子的),我们需要 “” 符号。然而,对于任何 和原子公式 和,有:
,
因此 “&” 与 “” 的混用在实践中并无影响。类似的说明也适用于否定以及下一段中关于 S4 的可证明性解释。
设 是所有有序对 的集合,其中 是PA 的一致扩展,而 是系统 的(可数)模型。令,其中 是PA 的标准模型。我们说:对于任意原子公式,定义:然后我们可以证明,对于任意原子公式,有:特别地:
由于 是一个-模型结构, 的所有规律都成立。但并非 的所有规律都成立;例如,如果 是哥德尔的不可判定公式,则:但也存在一些在 中不可证明的公式是有效的;特别地,我们可以证明,对于任意,有:这得出了 McKinsey 的 系统的定理(参见[13])。通过适当的修改,这一困难可以被消除;但在此我们不深入讨论。
类似的 和Brouwersche 系统的解释也可以被提出,但在本文作者看来,这些解释的趣味性较小。我们提到另一类可证明性解释,即PA 的“自反性”扩展。令 为包含PA 的形式系统,其良构公式通过PA 的闭合公式与连接词 &、 和 组成。(我这里使用与PA 相同的合取与否定符号“&” 和 “−”,未引入新符号。参见第91页脚注1。)我们称 为PA 的自反性扩展,当且仅当:
它是PA 的一个非本质扩展; 若 在E 中是可证明的,则 在E 中是可证明的; 存在一个赋值,将E 的闭合公式映射到集合,使得合取和否定遵循通常的真值表,所有在PA 中为真的闭合公式在E 中的取值为,且所有E 的定理的取值也为。可以证明,存在包含 或甚至 公理的PA 自反性扩展,但不存在包含 的扩展。
最后,我们指出,通过将直觉主义逻辑映射到,我们可以为直觉主义谓词演算建立一个模型理论。我们不在这里给出该模型理论,而是讨论一个特别有用的解释,仅限于命题演算。令 为PA 的任意一致扩展。我们说,公式 在E 中是验证的,当且仅当 在E 中是可证明的。我们将PA 的闭合良构公式视为原子公式,并用直觉主义的连接词、、 和 构建新公式。我们递归地规定:
在E 中,当且仅当 或 是被验证的, 才会在E 中被验证;当且仅当不存在验证 的一致扩展时, 在E 中被验证;当且仅当所有验证 的一致扩展E' 也验证 时, 在E 中被验证。
因此,直觉主义逻辑的每一个规律在PA 中都被验证;但例如, 不成立,如果 是哥德尔的不可判定公式。在未来的工作中,我们将进一步扩展这种解释,并展示我们可以找到 Kreisel 系统FC 的一个解释,该系统涉及绝对自由选择序列(参见[14])。顺便说一下,很明显,在 和 的可证明性解释中,PA 可以被任何真值功能系统替代(即,任何系统的模型确定每个闭合公式的真假);而直觉主义的解释适用于任何形式系统。
哈佛大学
参考文献
[1]Saul A. Kripke.A completeness theorem in modal logic.The journal of symbolic logic, vol. 24 (1959), pp. 1–15.
[2]Saul A. Kripke.Semantical analysis of modal logic (abstract).The journal of symbolic logic, vol. 24 (1959), pp. 323–324.
[3]Gottlob Frege.Über Sinn und Bedeutung.Zeitschrift für Philosophie und philosophische Kritik, vol. 100 (1892), pp. 25–50. 英文译文见:P. Geach 和 M. Black 编,Translations from the philosophical writings of Gottlob Frege, Basil Blackwell, Oxford 1952;以及 H. Feigl 和 W. Sellars 编,Readings in philosophical analysis, Appleton-Century-Crofts, Inc., New York 1949.
[4]P. F. Strawson.On referring.Mind, n. s., vol. 59 (1950), pp. 320–344.
[5]Bertrand Russell.On denoting.Mind, n. s., vol. 14 (1905), pp. 479–493.
[6]Jaakko Hintikka.Modality and quantification.Theoria (Lund), vol. 27 (1961), pp. 119–128.
[7]A. N. Prior.Time and modality. Clarendon Press, Oxford 1957, viii + 148 pp.
[8]A. N. Prior.Modality and quantification in S5.The journal of symbolic logic, vol. 21 (1956), pp. 60–62.
[9]Jaakko Hintikka.Existential presuppositions and existential commitments.The journal of philosophy, vol. 56 (1959), pp. 125–137.
[10]Hugues Leblanc 和Theodore Hailperin.Nondesignating singular terms.Philosophical review, vol. 68 (1959), pp. 239–243.
[11]Saul A. Kripke.Semantical analysis of modal logic I.Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 9 (1963), pp. 67–96.
[12]Stephen C. Kleene.Introduction to metamathematics. D. Van Nostrand, New York 1952, x + 550 pp.
[13]J. C. C. McKinsey.On the syntactical construction of systems of modal logic.The journal of symbolic logic, vol. 10 (1945), pp. 83–94.
[14]G. Kreisel.A remark on free choice sequences and the topological completeness proofs.The journal of symbolic logic, vol. 23 (1958), pp. 369–388.
[15]W. Van O. Quine.Mathematical logic. Harvard University Press, Cambridge, Mass., 1940; second ed., revised, 1951, xii + 346 pp.