谓词抽象及其作用，本文主要内容关键词为：谓词论文,抽象论文,作用论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
[中图分类号]B81 [文献标识码]A [文章编号]1002-8862(2008)05-0090-06
当今，命题模态逻辑作为一种标准的形式工具，已被广泛应用于计算机科学和人工智能的各个领域。然而，与命题模态逻辑不同，通常的一阶模态逻辑语言的表达力是不充分的，这是许多重要问题背后的原因所在，这些重要问题包括：模态逻辑中没能出现与经典逻辑相媲美的赫伯兰(Herbrand)定理、非严格指称问题、同一性问题、罗素的限定摹状词理论、动态逻辑的指派表达等等。美国当代逻辑学家、证明论专家菲汀(M.C.Fitting)充分认识到通常的一阶模态逻辑表达力不充分所产生的弊端，他通过把谓词抽象引入通常的一阶模态逻辑的语形和语义，以一种极其简单和自然的形式加强了一阶模态语言的表达力，从而使上述问题迎刃而解。本文首先介绍谓词抽象的基本思想及其简史，然后重点阐述谓词抽象在模态赫伯兰定理以及其他领域的重要作用。
一 谓词抽象及其简史
谓词是经典逻辑中的重要概念，它表示个体具有的性质或个体之间的关系。例如，把“3是素数”这一命题用符号表示为F(a)，其中的F就是一个谓词，表示“＿是素数”这一性质，而a表示一个具有素数这种性质的个体；同样地，把命题“周建人是鲁迅的弟弟”用符号表示为D(b，c)，D也是一个谓词，表示“＿和＿是兄弟”这一关系，而b、c表示具有兄弟关系的两个个体。
谓词抽象的思想最早是由斯托尔内克尔(R.Stalnaker)和托马森(R.Thomason)引入模态逻辑②中的。当初他们引入谓词抽象的目的是明确日常表达中诸如“太阳系行星的数目是偶数，这是必然的”和“太阳系行星的数目必然是偶数”这样两个句子之间的区别。从非形式的角度分析，前一个句子表达了“太阳系行星的数目是偶数”这一事实是必然的，而后一个句子表达了词项——“太阳系行星的数目”在现实世界指称的对象具有“必然是偶数”这一性质。根据国际天文学联合会大会2006年8月24日通过的决议，地位备受争议的冥王星被“开除”出太阳系行星行列，由此太阳系行星数目降为8。也就是在现实世界中，“太阳系行星的数目”指称的对象是数字8，毫无疑问，8在所有的世界都是偶数，也就是8具有“必然是偶数”的性质；而在2006年8月24以前的很长一段时间里我们曾经认为太阳系行星的数目是9，也就是说“太阳系行星的数目是偶数”这不是必然的，由此，借助于特殊的背景知识，我们将上面两种表达区别为一个错误的表达和一个正确的表达。
1972年布雷森(A.Bressan)在《一般解释下的模态演算》(A General Interpreted Modal Calculus)一书中，试图把谓词抽象的思想推广到高阶模态逻辑，但并未取得预期的效果，因此影响甚小。
谓词抽象的详细阐述和推广与菲汀的工作是分不开的。菲汀的工作集中于20世纪70年代和90年代。在20世纪70年代，菲汀基于斯托尔内克尔和托马森的基本思想，主要在模态逻辑领域应用谓词抽象，包括在1972年的文章《一个一阶S4ε-演算系统》和1975年的文章《一个模态ε-演算》中，菲汀使用谓词抽象给出一种基于希尔伯特(Hilbert)经典ε-演算的一阶模态系统，这样，一阶模态逻辑的表述除了公理系统、矢列系统、自然系统、表列系统以外，又多了一种表述方式；在1973年的文章《一个模态斯穆里安基本定理》中，菲汀使用谓词抽象给出一个模态斯穆里安定理。
20世纪90年代，菲汀意识到通常的一阶模态逻辑语言不充分的表达力不仅限制模态逻辑未能表达与经典逻辑相媲美的赫伯兰定理，而且也是许多其他领域重要问题“背后”的原因所在。菲汀通过把谓词抽象引入通常的一阶模态逻辑的语形和语义，以一种很自然的方式加强了一阶模态逻辑语言的表达力，从而给出没有巴坎(R.Barcan)公式的模态系统K的赫伯兰定理；不仅如此，菲汀还使用谓词抽象解决哲学、动态逻辑等领域的相关问题，这样，谓词抽象作为一种工具，其作用得到充分发挥。
二 谓词抽象在赫伯兰定理中的作用
作为经典逻辑的一条重要的元定理，赫伯兰定理为人工智能中定理的机器证明提供了理论基础。自动定理证明的中心问题是寻找判定合式公式是否有效的通用方法，命题逻辑的合式公式的有效性问题是可判定的。而对于一阶逻辑的合式公式来说，情况却不是那么简单，一阶公式的有效性问题不是可判定的，仅是半可判定的。这一结果由丘奇(A.Church)和图灵(A.M.Tunng)在1936年证明，他们指出，如果一个一阶公式是有效的，则存在检验逻辑真的算法，如果不是逻辑真的，则无法在有穷步骤内判定。赫伯兰1930年博士论文第五章的基本定理为自动定理证明建立了一种重要方法，它把每一个一阶公式X与一个公式序列
…联系起来，使得X有一个一阶证明，当且仅当
是一个重言式，这样就把一个一阶问题转化为一个命题问题，从而为自动机的定理证明提供了理论基础。基于赫伯兰定理的理论基础，罗宾逊(Robinson)于1965年建立归结原理，使自动机定理证明达到了实用的阶段。
然而，尽管赫伯兰定理本身有着良好的性质，但它的影响主要停留在经典逻辑。诚然，在20世纪70年代至90年代，人们做过把赫伯兰定理推广到模态逻辑的各种尝试，包括菲汀1973年的工作④、查尔迪(M.Cialdea)和塞罗(L.Cerro)1986年的工作⑤和1993年的工作⑥以及康诺利杰(K.Konolige)1986年的工作⑦等等，但由于各种原因，这些尝试都未能取得完全令人满意的结果。
经典逻辑自动定理证明的一个重要的步骤是斯科伦(Skolem)化，即去掉量词，在保持可满足性(去存在量词)或有效性(去全称量词)的基础上引入新的函数符号。例如对于公式(
x)Φ(x)，我们用Φ(c)加以取代，其中c是新引入的常元符号。然而在模态逻辑中，情况却并非那么简单。例如公式◇(x)Φ(x)的斯科伦化形式是什么？而(x)◇Φ(x)的斯科伦化形式又是什么？根据经典逻辑的做法，两者似乎都是◇Φ(c)，但这不合乎逻辑，因为公式◇(x)Φ(x)和(x)◇Φ(x)是不等价的。假如◇(x)Φ(x)的斯科伦化形式是◇Φ(c)，那么根据斯科伦化保持有效性的原则，若◇(x)Φ(x)在某一克里普克(Kripke)模型的某个可能世界w上是假的，则在w的所有可及世界中，(x)Φ(x)是假的，即在w所有可及世界的定义域中至少存在一个对象不具有性质Φ，但是没有理由规定在w的每一可及世界的定义域中，这样的对象必须是同一对象。这样，若◇(x)Φ(x)的斯科伦化形式是◇Φ(c)，那么c就允许在w的可及世界的定义域中指称不同的对象。词项在不同的可能世界指称不同的对象被哲学家称为非严格(non-rigid)指称；反之，词项在不同的可能世界指称相同的对象被称为严格(rigid)指称。可见，模态逻辑公式的斯科伦化要求非严格指称。
根据上面的分析，我们可以理解为，公式□P(c)中涉及两种“运算”：指称运算和世界之间的通达运算。两种运算的先后次序不同，导致结果完全不同。显然，在前一种读法中，先进行世界间的通达运算，后进行指称运算；而在后一种读法中，先进行指称运算，后进行世界间的通达运算。只有在严格指称的情况下，两种运算的先后次序才可以交换(commute)，而在非严格指称的情况下两种运算的次序不可交换。为了避免上述问题的出现，通常的一阶模态逻辑采取禁止非严格指称的原则，这样就人为地舍去第一种读法，因此不能对公式□P(c)做出上述两种读法的区分，结果导致表达力大大减弱。
由于模态逻辑公式的斯科伦化要求非严格指称，而通常的一阶模态逻辑采取禁止非严格指称的原则，因此在模态赫伯兰定理的第一个步骤就产生了困难，后面的步骤无法进行。
菲汀认识到必须对通常的一阶模态逻辑进行改进，他在吸取前人工作并把其工作向前进的基础上，于1996年发表《一个模态赫伯兰定理》(A Modal Herbrand Theorem)一文。在这篇具有标志性和开创性的文章中，菲汀第一次系统地把谓词抽象引入通常的一阶模态逻辑的语形和语义，使其表达力大大增强，从而以一种很自然的方式得出没有巴坎公式的模态系统K的赫伯兰定理。
在语义方面，除了考虑非严格模型(即允许词项在不同的世界指称不同的对象)以外，菲汀基本上采用标准的可能世界语义学。同时增加一条公式在模型中为真的条件，公式〈λx.Φ(x)＞(t)的在模型的某个世界中为真，当且仅当Φ中的变元x被指派为
在该世界上所指称的对象时，Φ在该世界上是可满足的。⑧
不仅如此，赫伯兰定理的下一个步骤——赫伯兰扩张(expansion)，以及赫伯兰定理的证明，也是与谓词抽象密切相关的。在进行赫伯兰扩张的过程中，菲汀使用一个考虑谓词抽象的矢列演算(sequent calculus)(其中的兰姆达规则和约束(bind)规则引入谓词抽象)给出一个赫伯兰扩张的关系定义，从而模态赫伯兰扩张得以实现；而在定理的证明过程中，菲汀使用的是考虑谓词抽象的表列系统(tableau system)，在证明过程中，公式中的自由变元的排除是借助于谓词抽象实现的，限于篇幅，这里不再一一陈述。
1999年菲汀在其发表的《模态逻辑的赫伯兰定理》(Herbrand's Theorem for Modal Logic)一文中，简要概括1996年文章的基本思想，并指出：相似的结果可以从其他的模态系统如D、T、S4、S5等获得。为贯彻菲汀的思想，本文的作者通过在菲汀工作的基础上增加相应条件，已经给出K的最小扩张——D系统的赫伯兰定理，从原则上讲，通过增加相应的条件，系统T、S4、S5的赫伯兰定理也是可以给出的。在以后的工作中，本文的作者还将寻求一定范围内模态系统的赫伯兰定理的统一处理方法。不管是在单个系统还是一定范围内的模态系统的赫伯兰定理中，谓词抽象的使用都起着决定性的作用。
三 谓词抽象在其他领域的重要作用
谓词抽象的使用不仅使我们获得了迄今为止与经典逻辑最为接近的模态领域的赫伯兰定理，而且借助于谓词抽象，许多领域的重要问题如晨星/昏星问题、罗素的限定摹状词理论、动态逻辑的指派表达等可以从一种全新的角度得以阐释或解决。
1.对晨星/昏星(即同一性)问题的解决
同一性是事物之间的一种关系，我们说两个事物是同一的，即两个事物之间具有同一关系。同一关系的一个显著特征是同一替换规则。也就是说如果A和B具有同一关系，那么用B替换A在一个句子中的所有出现，所得到的句子的真值不会改变。这使我们想起晨星/昏星的例子。晨星(the morning star)和昏星(the evening star)是同一个星球的名字，这最早大约是巴比伦的天文学家经过观测所确定的结果。如果用m表示“晨星”，e表示“昏星”，那么m=e表示晨星和昏星具有同一关系。虽然古人一度不知道晨星指称的对象与昏星指称的对象是同一对象，但是古人知道一个对象与自身是同一的，如果用K表示“古人知道”，那么K(m=m)表示“古人知道晨星是晨星”，这是一个真命题。如果我们对公式K(m=m)使用同一替换规则，用e去替换第二个m的出现，得到K(m=e)，这一公式断定了“古人知道晨星是昏星”，这显然是一个假命题，同一替换原则在这里不成立。
关于同一替换规则在模态语境中不成立的原因，奎因(Quine)归结于“模态语境的指称晦暗性”(referentially opaque)。⑨而弗雷格则提出含义(sense)与指称(denotation)的区别⑩，他坚持认为晨星这样的词项既有“涵义”，又有“指称”。它的指称是指一个特殊的天文学对象，它的含义是指这一天文学对象是如何被指称的，而且在认知逻辑这种非真值函项的背景下，真正起作用的是含义。但是这种区别也没能真正解决问题，而是使弗雷格进一步陷入困惑之中。
我们认为对象层面上的同一替换原则是成立的，问题出在我们的谈话中，并不直接使用对象，而是使用它们的名称，而在一个世界中指称同一对象的两个名称在其他世界可以指称不同的对象。对象层面上的同一替换原则成立这是下面的解决方式的关键。我们考虑修改和扩充后的一阶模态逻辑的认知模型，其中的可能世界是古人的知识储备，而现实世界是其中的一个可能世界。在现实世界中，常元符号m和e分别用来指称“晨星”和“昏星”两个对象，而且在现实世界中它们指称同一对象，但在其他世界它们不指称同一对象；□表示“古人知道”，我们如何在不使用同一替换规则的情况下从m=e得到□(m=e)。谓词抽象的使用帮助我们把有歧义的表达式(m=e)→□(m=e)，区分为有效式〈λx，y.x=y〉(m，e)→〈λx，y.□(x=y)〉(m，e)和非有效式〈λx，y.x=y〉(m，e)→□〈λx，y.x=y〉(m，e)，这两个公式的区分大致对应于弗雷格使用的指称与含义的区分。(11)
2.对罗素限定摹状词理论的阐释
那么“当今法国国王不是秃子”这一命题的真值又是什么呢？罗素指出，“当今法国国王不是秃子”这一命题是有歧义的。我们应该把它理解为这一命题断定了，当今法国国王具有某种否定的性质——不是秃头的，还是理解为这一命题是对“当今法国国王具有不是秃头的这一性质”的断定做否定呢？用罗素的话说是否定谓词B(x)，还是该否定整个句子呢？两者是不等价的。
对此，罗素提出前面提到的狭域与广域的区别，尽管后来的事实证明，狭域与广域的区别不足以解决问题，但是做这种区分背后的思想是有意义的。罗素在把限定摹状词转化为形式语言时，引入了存在量词，存在量词是有(形式)辖域的，相应的在句子中，限定摹状词也应该有辖域。一般而言，在自然语言中限定摹状词的辖域是不明显的，我们往往需要借助语境加以区分和界定；而在形式语言中，我们又如何界定指称限定摹状词的词项的辖域呢？借助于谓词抽象，问题可得以轻松解决。
3.对动态逻辑指派陈述问题的处理
动态逻辑是关于计算机程序的逻辑，它是在通常的模态逻辑的基础上引入一组计算机的行为，且这些行为在各种运算例如先后顺序运算、重复运算下是封闭的。对于每一个行为α，存在一个与之对应的模态算子[α]。从非形式的角度，公式[α]X读作：在完成α行为后，X将是真的。存在一个与之相应的语义学，其中的可能世界是计算机在计算过程中出现的各种可能状态。
动态逻辑的一个典型的原则是[α；β]X≡[α][β]X，其中的分号对应于行为的先后顺序。尽管动态逻辑为复合行为提供了一种很好的处理方式，但是对于原子行为的处理并非那么简单。考虑下面的指派陈述c：=c+1刻画的是什么动态过程呢？假设我们熟悉指派陈述关于行为前后的概念，那么该陈述等号右边使用的是c在当前状态下的值，等号左边反映了在执行+1行为后所获得的新的值。可见，在指派陈述c：=c+1中，行为前后，c的值是不同的。为了对之做形式化的处理，必然要求c是非严格指称的，即c在不同的计算状态指称不同的对象。假设算数运算是在通常的意义上使用的，并且我们使用□作为[c：=c+1]的简写，那么
的一个逻辑后承。(12)
可见，动态逻辑处理原子行为的指派陈述时需要非严格指称。
总之，借助谓词抽象这种灵活而有效的工具，人们不仅解决了模态逻辑领域的一些重大问题，而且也使一些经典的哲学问题从一种全新的视角被加以阐释和解决。需要指出的是，人们应该致力于开拓谓词抽象发挥作用的其他领域和其他的哲学问题如存在性问题、词项的指称问题等等。相信随着人们对谓词抽象这种工具的广泛应用，它能够在更多的领域发挥作用。
注释：
①Fitting M.C.& Mendelsohn R.,First-Order Modal Logic,Kluwer Academic Publishers,1998,p.197.
②这里的模态逻辑是包括时态逻辑、认知逻辑、道义逻辑等在内的广义模态逻辑。
③Stalnaker R.and Thomason R.,"Abstraction in First- order Modal Logic",Theoria 34,1968,pp.203～207.
④Fitting M.C.,"A Modal Logic Analog of Smullyan's Fundamental Theorem",Zeitschrift für Mathematische Logik und Gründlagen der Mathematik,19(1973),pp.1～16.
⑤Cialdea Mand Luis Fari
as del Cerro,"A Modal Herbrand Property",Zeitschrift für Mathematische Logik und Grundlagen der Mathematik,32(1986),pp.523～530.
⑥M.Cialdea Mayer,"Herbrand style Proof Procedures for Modal Logics",Journal of Applied Non-Classical Logics,3(1993),pp.205～223.
⑦Kurt Konolige,A Deduction Model of Belief,Morgan Kaufman,Los Altos,CA,1986.
⑧Fitting M.C.,"A Modal Herbrand Theorem",Fundamenta Informaticae,28(1996),pp.101～122.
⑨Willard Van Orman Quine,From a Logical Point of View:9 Logico -philosophical Essays,Cambridge,Mass,Harvard University Press,1980,p.143.
⑩Russell B.,On Denoting Mind,14(1905),pp.479～493,Reprinted in Robert C.Marsh,ed.,Logic and Knowledge:Essays 1901-1950,by Bertrand Russell,Allen & Unwin,London,1956.
(11)(12)Fitting M.C.,Bertrand Russell,"Herbrand's Theorem,and the Assignment Statement",Artificial Intelligence and Symbolic Computation,Springer,LNAI 1476,1998,pp.14～28.