消解方法和逻辑公式的有效性判定

消解方法和逻辑公式的有效性判定 华东师范大学 2003年度硕士学位论文消解方法和逻辑公式的有效性判定专 业: 逻辑学 研究方向: 现代逻辑 导 师: 冯棉 教授 研 究 生: 唐平华 2003年 3月 0摘 要 在人工智能研究中,带有逻辑主义倾向的研究者主要面临两个问题:第一, 寻找适当的机器表达语言,比如有人把一阶语言作为机器的表达语言,甚至很多 人用 Prolog这样的基于一阶语言的计算机编程语言。第二,寻找语句是否有效 或是否可满足的判定程序。出于对第二个问题的关注,本文分析了逻辑公式有效 性判定问题的由来和历史、命题逻辑公式的判定方法、三段论推理的判定方法和 一阶谓词逻辑公式的判定方法。而文中的消解方法是分析问题的一条主线。 对于命题逻辑公式的判定,本文分析了真值表方法、语义表判定方法、范 式方法和消解方法。从对这些方法的分析中,我们可以看出要判定命题逻辑 公式 是否有效不是很难的。除本文介绍的方法外,我们还可以参考其他一些方法,比 如二叉判定树和 算法等。 为了扩大消解方法的应用范围,本文分析了弱消解,即基于反对关系的消 解,并且我们通过一些有效的公式进一步扩大了消解的应用范围,从而建立了适 合三段论和一阶谓词逻辑公式的一些消解。 对于三段论,主要考虑的是图形判定方法和消解方法,本文提出了两种新 的图形判定:三个变量的卡诺图法和笛卡儿坐标方法。卡诺图一般用来简化析取 范式,在电路分析和数字逻辑中用到,但是笔者发现使用三个变量的卡诺图来判 定三段论推理是否有效比凡恩图方法有更多的明晰性,且其画法要简单一些。因 为笛卡儿坐标使用八个象限,所以只要我们适当的安排变量在笛卡儿坐标各个象 限的分布,它就可以被用来判定三段论是否是有效的。而使用消解方法来判定一 个三段论是否有效的过程也是简便易行的。 一阶谓词逻辑公式的判定过程有些复杂且不是那么完美。因为我们知道一 阶谓词逻辑只具有半可判定性,就是说在理论上有的公式就不具备可判定 性。本 文介绍的基于 的判定方法和消解方法都是只能对部分公式进行判定, 而这本身也是不容易的。我们在对公式进行判定之前,还要对公式作一些处理, 这些处理可能会使得得到的公式与原来的公式不等值。 尽管自 1965年 J. A. Robinson提出消解原理以来,很多人都研究过消解并 提出了不同的消解策略,但是本文与其他研究的不同之处在于:我们是从逻辑学 角度分析了消解方法的。一般的消解是在有着矛盾关系的公式之间进行,本文提 出弱消解对一般的消解要求有所弱化,即只要求两公式之间存在不可同真的关系 就可以进行消解。而且为了适合谓词逻辑公式,我们利用一些有效式进一步扩充 消解方法的应用范围。在对谓词逻辑公式进行消解时,本文提出的消解过程没有 采用合一算法。1Abstract There are two problems that have to be dealt with by those researchers are called logicists in the study of artificial intelligence. Firstly, they have to deal with the languages. That’ s mean they have to choose or create machine-oriented languages which can be processed in a programmatic way. For example, some researchers have put in use of first-order language, and we all know that Prolog that bases on first-order language is prevailing in the AI programming. Secondly, they got to provide the decision procession for the sentences in the languages they put to use in the machinesSome logic languages are alternatives or potentially alternatives for some researchers in AI field. So the paper here focus on the problem of decision problem of some logic languages. Simply, the paper has analyzed the history of the study of decision problem of logic formulas, the methods of deciding the validity of proposition logic formulas, the methods of deciding the validity of syllogisms, and the methods of deciding the validity of first order predicative formulasIn the analysis of deciding the validity of proposition logic formulas, the paper gives an introduction to the methods of truth-value table, semantic tree, normal form and Resolution. From these analyses, we can see that it is not hard to decide the validity of proposition logic formulas. And we can also refer to some other decision method such as decision tree and DP algorithm Davis-Putnam algorithmTo implicate the Resolution method to further formulas, the paper gives a definition to minor Resolution, that is, the Resolution based on contrary and sub-contrary relations rather then contradictory relation, and through some valid formulas, the paper introduces more Resolution rules which are for deciding syllogisms and first order predicate formulasSome graph and Resolution methods are applied to the decision of syllogismsIt is not necessary to study Venn diagram, for many books have shown us the detail and the application of Venn diagram. The paper has analyzed some other graph methods like Karnaugh Map and Cartesian Coordinates. All these graphs are divided to eight unites, which represent the conjunction of two or three sets. The graphs indicate the validity or non-validity of a syllogism through the results of its premises and the requirement of its conclusion. The process of deciding the validity of a syllogism is very simple when the Resolution method is appliedFor the half-decidable character of first order predicate logic, it’ s not easy for deciding the validity of first order predicate formulas. The methods in the paper are based on Resolution principle or Herbrand theorem, and they are not complete or perfectThere are many researches on Resolution since the first article’ s publication of J. A. Robinson in 1965. Many strategies are applied to the practice in computation science. Different to those studies, the paper analyzes Resolution from the point of logic and introduces the minor-Resolution principle to enhance the application of Resolution principle. To make some formulas of first order predicate resoluble, the paper uses some valid formulas as rules. And the paper has managed to avoid2unification algorithmKarnaugh map and Cartesian coordinates are firstly implied to the decision of syllogisms in the paper. Generally, Karnaugh maps are restricted on the studies of circuit analysis and digit logic, but we find that it can also be used to deciding the validity of syllogism, and it is easier to draw and much clearer then Venn diagramFor 3-dimension Cartesian coordinates has eight quadrants, when the variables are well arranged in these quadrants, Cartesian coordinates can also be used to deciding the validity of syllogisms 3目录 摘要 ? Abstract? ? 第一节 历史和问题的由来 第二节 命题逻辑公式的判定方法 真值表方法 语义表判定方法 范式方法 消解方法 分析 第三节 弱消解 第四节 三段论的判定方法三段论规则 凡恩图方法 三个变量的卡诺图法笛 卡儿坐标方法 消解方法 分析 第五节 消解方法和一阶谓词逻辑公式的判定问题简述 基于 定理的判定方法 消解方法 分析 主要参考文献 其他参考文献 4消解方法和逻辑公式的有效性判定第一节 历史和问题的由来 “判定”这个概念很早就有了,至少在 19世纪末、20世纪初就有了明确 的要求对某些问题的判定,比如希尔伯特二十三个数学问题中的第十个问题:能 1 否在有限步骤内判定不定方程是否存在整数解?或者说丢番图方程是否有解? 它要求通过一种机械的方法(或者说提供一种算法)在有限步骤内对丢番图方程 是否有解作出判定。在数学的其它分支中,判定问题也是一个很重要的问题,比 如我国著名数学家吴文俊在初等几何判定问题上的贡献(Wu Wen-Tsün,1978) 2 3 。而在数理逻辑中,明确提出“判定问题”的人是 J. Herbrand,他说:根据希 尔伯特的想法,“数理逻辑的主要问题是在理论框架中寻找一种程序,通过这种 4 程序就可能认识到一个命题(Proposition)是否为真或者为假”。这可能有些粗 造,因为数理逻辑不是仅仅关心命题的。然而,大多数人可能会比较同意如下关 于判定问题的定义:给定一个集合 A和一些性质 P,去寻找一个算法,使它能告 知对于集合 A中的任何元素 a(即 a? ),是否具有性质 P;或者能证明不可能 5 找到这样的算法。但这样的定义可能对我们来说有些过宽了,我们主要关心逻 辑推演系统中句子(公式)是否可以在其中得证的问题,或者说是否有一个一般 6 的判定程序能使我们判定系统中的公式是否可以得证。在逻辑系统中,这样的问题是怎样产生的呢?我们知道,在 19世纪末、20 世纪初,数理逻辑飞速发展,有人甚至说是“数理逻辑的勃兴”、“数理逻辑的 凯1 ////0>. 维斯(Davis)、普特南(Putnan)、罗宾逊(Robinson)等取得关键性突破。1968 年,巴克 尔(Baker)、费罗斯(Philos)对含两个未知数的方程取得肯定结论。1970年。 苏联数学家 马蒂塞维奇最终证明:在一般情况下,是否定的。 2 W. W. Bledsoe and D. W. Loveland(Editors), Contemporary Mathematics, Automated Theorem Proving:After 25 Years,American Mathematical Society,1983,P213-234。 3 我接触的中文书的大多作者没有给出 J. Herbrand中文译名,为了查找方便, 我们也直接给 出英文明,下面直接写为 Herbrand。 4 这里为二次引用,出处为:Anton Dumitriu,History of Logic, V olume ?,English Edition, Abacus Press,1977,P184,原文出处为:J. Herbrand, Recherches sur la thé orie de la demonstration, “ Travaux de la Socié té ded Sciences et des lLettres de Varsovie” , el. ? No. 33, 19305 冯契(主编)《哲学大词典??逻辑学卷》,上海辞书出版社,1988年,上海,P249~250。 6 Alfred Tarski, Introduction to Logic and to The Methodology of Deductive science, Oxford University Press, Inc. , 1965, P136~137 51 旋”。经典逻辑比较完整地建立之后,即罗素、怀特海的《数学原理》发表以 后,大多数逻辑学家相信,在他们(包括希尔伯特)建立的经典逻辑系统中,应 该是毫无遗留的包含了所有有效的公式,就是说这些系统应该是完全的(有人说 2 每个直觉上正确的公式应该在这些有着适当公理的系统中得证 )。在此之前,希 尔伯特于 1899年发表了《几何基础》(Grundlagen der Geometrie),对欧氏几何 重新进行整理,给出了一个公理几何系统,这使得他萌发了推广形式公理方法的 3 想法(或许他在此之前就有了这种想法)以解决在数学中出现的集合论悖论。 这是数学界很有名的希尔伯特,即将数学公理化,从没有问题的公理出发, 建立在数学上(某个分支类)“无所不包”的系统,这样得到的系统将没有任何 矛盾,从而不出现悖论。希尔伯特的做法是对一个系统的公式作出判定,如果有 判定程序表明没有互为矛盾的公式在系统中获证,那么这个系统就是一致的。而 后来这样的想法受到了冲击(即使如此,希尔伯特的想法还是很重要的),即哥 4 德尔(Kurt G?del)对一些形式系统做的不完全性证明。他证明了这些系统是不 5 完全的,并且肯定了在这些系统中存在有不可判定的问题,系统的一致性问题 就是其中之一。也就是说这些系统不是当初人们想象的那么完美,比如可能有的 系统中的部分公式是没法被判定的。 逻辑系统中的公式也同样存在判定问题。对于命题逻辑,希尔伯特和阿克 曼将公式化成范式,从范式的形式我们就可以对这些公式作出判定了。所以,命 题逻辑的判定问题很容易就得到了解决。对于一阶谓词逻辑系统中公式的判定问 题,逻辑学家和数学家在 Herbrand和 G.Gentzen的工作基础上取得了一些成绩。 6 比如 L.L?wenheim证明了任何只有一个谓词的公式是可以判定的。其中司寇伦 (Thoralf Skolem)也做了不少贡献,他提出一种“判定函数”,指出一个公式在 某个解释中是真的,当且仅当有对应的判定函数存在。希尔伯特学派也在这个问 题上对一些特定形式的公式的可判定性作了证明,哥德尔给出了一些更为复杂的 7 公式的可判定性证明。但是,对于一阶谓词逻辑系统中的公式,却没有某种有1 让.迪厄多内(著),沈永欢(译),《当代数学??为了人类心智的荣耀》,上海教育出版 社,1999年,上海,P267,P270。 2 [波兰] 安德热依.莫斯托夫斯基(著),郭世铭、称安捷、修庆云译:《数学基础研究三十 年》,华中工学院出版社,1983年(原著于 1965年),武昌,P14 3 张尚水(编),《当代西方著名哲学家评传??第五卷 逻辑哲学》,山东人民出版社,1996 年,济南,P58 4 张尚水(编),《当代西方著名哲学家评传??第五卷 逻辑哲学》,山东人民出版社,1996 年,济南,P71:“(1)一个包含初等数论的形式系统,如果是协调的,那么就不是完全的; (2)如果这样的系统是协调的,则其协调性不能在该系统中得到证明。” 5 Howard Eves & Carroll V. Newsom,An Introduction to The Foundations And Fundamental Concepts,Holt,Rinehart,Winston,1965,P3056 Anton Dumitriu,History of Logic,Volume ?,English Edition,Abacus Press,1977,P1877 关于这些公式,我们会在第五节给出。6效的机械的统一规则来对它们在有限步内进行判定,也就是说没有一个一般的步 1 骤可以对一阶谓词逻辑的所有公式作出判定。 丘奇发现所有能判定的公式都是属于“递归类”的,或者说某个谓词是否 2 可以判定,要看它的特征函数是否是递归的。而另一种表达是图灵可计算函 数, 后来丘奇发现图灵可计算函数也是递归函数,而递归函数也是图灵可计算函数, 递归的和图灵可计算的实际上是等价的,尽管二者看起来是多么不同(一个是要 满足递归的一些性质,另一个是要能在某种理想机器上得以运算,并且这种运算 要能停下来以给出结果)。总之,不是所有的一阶逻辑公式都可以在一种程序下 得到判定。但是人们并没有放弃寻找这种判定方法的企图。因为可能有些方法可 以给出“很多”我们感兴趣的公式的判定,通过对这些程序进行修改,可以对更 多的公式作出判定,而判定的速度、效率可以得到改善。一旦有一种机械的方法 来实现,我们就可能借助机器来求解。 一个很有成效的判定方法是建立在 Herbrand的工作基础之上的。我们知道, 如果某个公式在任何一个解释下的任何赋值中都取值为真,那么这个公式当然是 有效的,如果一个公式在任何一个解释下的任何赋值中都取值为假,那么这个公 式就是不可满足的,但是我们不可能检查每一个解释下的每一个赋值。那么是否 可以把问题化归到某一个特定的解释上?答案是肯定的,恰好有一个称为 Herbrand域的特定域,在这个域的相关解释下,某个公式是有效的,当且仅当这 个公式在其 Herbrand域中的每一个赋值为真;某个公式是不可满足,当且仅当 这个公式在其 Herbrand 域中的每一个赋值为假。而 Herbrand 给出了一个定理 3 (Herbrand定理):一个公式是不可满足的,当且仅当存在该公式的有限个基例, 且这些基例是不可满足的。 Herbrand定理为我们提供了一种证明公式不可满足性 的方法,就是不断地生成所给公式的基例,然后去测试基例集是否可满足,如果 4 得到的基例集不可满足,那么原来的公式也就不可满足。这样就把一阶谓词逻 辑公式的判定转化为命题逻辑公式的判定了。人们基于 Herbrand的工作,给出 5 一些判定程序,比如 Davis-Putnam方法。但是要处理大量的基例也是一件很棘 手的事情,所以利用 Herbrand定理来对公式进行判定对有些公式来说不太有效。 1965年,J. A. Robinson提出消解原理,给出了逻辑公式判定的一种很好的1 尽管有一些程序可以对部分公式作出判定。也许对于某个程序不能判定的公式,我们可以 找到该公式的其他证明。 2 陆钟万:《数理逻辑与机器证明》,科学出版社,1983年,北京,P147-153。 3 一个公式的基例即是该公式的一个赋值。 4 张健,《逻辑公式的可满足性判定??方法、工具及应用》,科学出版社,2000年,北京, P77。 5 张健,《逻辑公式的可满足性判定??方法、工具及应用》,科学出版社,2000年,北京, P34。7方法,Robinson于 1964年将《建立在消解原理之上的机器逻辑》寄往《计算机 杂志》,但是等了一年才发出。因为消解方法十分有效,所以 Robinson的文章发 表后影响很大,并且消解方法得到很大的发展,人们提出了各种各样的消解策略 以赢得更多的机器时间和空间(即,减少计算机计算时间和内存)。 出于对逻辑公式判定的考虑,本文介绍并提出一些逻辑公式的判定方法。 同时在 Robinson工作的基础上,用消解方法来对命题逻辑公式、三段论推理和 一阶谓词逻辑公式的有效性的判定进行讨论。在讨论消解方法时,也试图对 Robinson的方法作些改进和解释。第二节命题逻辑公式的判定方法 2.1 真值表方法 判定一个命题逻辑公式是否有效,或者说看它是否是重言式(永真式)有 很多方法,常用的方法是穷举法。因为某个特定的命题逻辑公式涉及的变量是有 限的,而每个命题变元只有两种取值,所以可以通过直接给变元赋值来进行判定。 1 穷举法中的一种是真值表方法(一般认为真值表是由维特根斯坦发明的,有人 认为皮尔士也很明晰地提出了真值表的方法,而且真值表方法的历史也许很长 2 ),真值表方法在逻辑学教材中叙述得很详细,而且用得也很广泛,在此,我们 不再重复。 2.2 语义表判定方法 我们在这里称为语义表的是一种树结构。比如给定一个公式 A,A的语义 表是以 A为根、A的子公式为其节点的树,从 A到任一树叶是一个分支,如果 某个分支中包含一个子公式和它的否定,那么这条分支就是封闭的(我们将在该 分支下加一个“?”这样的符号 )。如果所有的分支都是封闭的,那么这个公式 就是不可满足的,它的否定就是有效的;如果有分支不是封闭的,且这些分支不 能继续分下去的话,那么这个公式就是可以满足的。做语义表的具体规则如下: 规则1 A?BA?BA B 它的意思是当且仅当 A、B同真时,A? 真。1 路德维希.维特根斯坦,《逻辑哲学论》,商务印书馆,1996年,北京,P56~57。 2 //.hensiki, A History of Formal Logic, Notre Dame, Indiana: University of Notre Dame Press, 1961 8规则2 ~(A?)~(A?) ~A ~B 它的意思是当且仅当或者~A真,或者~B真时,~(A?)真。 规则3 A?B A?B A B 它的意思是当且仅当或者 A真,或者 B真时,A?B真。 规则4 ~(A?B)~(A?B) ~ A ~ B 它的意思是当且仅当~A真且~B真时,~(A?)真。 规则5 A?B A?B~A B 它的意思是当且仅当或者~A真,或者 B真时,A?B真。 规则6 ~(A?B) ~(A?B) A ~B 它的意思是当且仅当 A真且~B真时,~(A?B)真。 规则7 ~~A ~~A A它的意思是当且仅当 A真时,~~A真。 规则8 A? B1 A? B A~A B~B 它的意思是当且仅当或者 A真且 B真,或者~A真且~B真时,A?B真。 规则9 ~(A?B) ~(A?B) A~A 9 ~B B 它的意思是当且仅当或者 A真且~B真,或者~A真且 B真时,~(A?B) 真。 下面我们举个例子说明语意表怎么使用: 例,判定公式(A?B)?(~B?~A)是否是有效的。 公式(A?B)?(~B?~A)的否定为~((A?B)?(~B?~A)) 画~((A?B)?(~B?~A))的语义判定表: 1,~((A?B)?(~B?~A))1,规则 6 2, A?B , ~(~B?~A) 3,规则 6 4, ~B 5,~~A2,规则 5 6,~A7, B ?(,)?(,) 根据语意表,我们知道公式~((A?B)?(~B?~A))的语意表有两条 分支,每条分支都是封闭的,所以~((A?B)?(~B?~A))是不可满足的, 那么公式(A?B)?(~B?~A)就是有效的。 2.3 范式方法 建立逻辑公式的范式也可以使得公式的某些性质在形式上得以明显,比如 一个析取范式,如果它的每一个合取支中含有一个原子命题和它的否定,那 么这 个析取范式就是一个永假式;一个合取范式,如果其每一个析取支中含有一 个原 子命题和它的否定,那么这个合取范式就是一个永真式。于是对于每一个命 题逻 1 辑公式,我们可以通过找到它的适当的范式来判别它是永真式还是永假式 2.4 消解方法: 我们可以给消解以下定义: 设两个简单析取式 , , 中有析取支(或~ ), 中有析取支~(或 者)从 中消去(或~)得到 ’,从 中消去~(或)得到 ’,将 ’, ’析取得到一个新的析取式 , 称为消解 , 的消解式。 命题:如果两个简单析取式可消解的话,那么这两个简单析取式的合取式1 王宪钧,《数理逻辑引论》,北京大学出版社,1982年 6月,北京,P82~86。10逻辑蕴涵这两个简单析取式的消解式。 证明:设任意两个简单析取式 ’?, ’?~,其合取式为? ,消解式为 ;我们可以用简化真值表方法知道(( ’? )?( ’?~))?( ’? ’)为一永真式。所以命题得证。 如果一个合取范式 是重言式,那么因为? ?(p?~ ),所以?~A? ~ (p?~ ),?~A(p?~ ),而 p?~ 的两个解析式消解后什么也没有留 下,我们将其结果称为空公式,用“?”标识。而我们知道 p?~ 为一个永假 式,所以约定“?”也是一个永假式。 所以要证明一个公式 A是否是重言式,那么先取其否定式~A,再将~A 化成合取范式 A’,然后对 A’不断消解,看最后是否可以得到一个空公式,如果 得到一个空公式,那么就是 A的否定逻辑蕴涵一个矛盾式,说明 A是重言式。 1 反之,如果不能消解为一个空公式,说明该公式不是重言式。 例,判定公式(p?)?(q?)?(p?)是否是有效式。 解:公式~((p?)?(q?)?(p? ))的一个合取范式为: 1),(~p?q)?(~q?r)??~ 式 的析取支为: ),~p?q 3),~q?r 4), ),~ , 消解得到: ), , 消解得到: ), , 消解得到: ),? 2 所以(p?)?(q?)?(p?)是一个有效式(重言式)。 在上面的例子中,我们看到,使用消解方法判定一个合取范式是否有效时, 我们只关心组成范式的各个简单析取式之间可否使用消解方法,并不在乎整 个式 3 子的形式,所以我们也常常将合取范式写成子句集形式。比如公式(~p?q) ?(~q?r)??~ 的子句集形式为(~p?q),(~q?r),,~ ,这样 可以给消解过程带来一些便利。 1 见本文第三节。 2 命题逻辑中,我们不明显区分语义和语法概念。 3 一个将合取范式的各个简单析取式作为元素的集合,其元素称为子句,即简单析取式。112.5 分析 除了以上我们介绍的方法外,还有一些方法,比如二叉判定树(Binary 1 Decision Diagrams)以及 DP算法也是比较常见的。总之,对于一个命题逻辑公 式,判定其有效性不是很难的,而且有很多机械的方法,所以可以编制一些程序, 让机器来证明一个公式是否是有效的,或者说在公理下是否可以证明。我们可以 2 参看一些程序(比如 lcp这样的一个程序)的结果。 在逻辑公式的判定方法中,真值表是通过对命题变元赋值的不同组合来确 定公式是否有效,或者是否可满足,这样看起来比较直观。但是这些组合的量是 随着变元的增加而呈指数增长的。如果变元比较多,比如十个变元,那么表的长 10 度将是 2 行,这会带来不便。语义表相对于真值表而言,很多情况都会少些步骤。语意表的树分支只要 其中包含了互为矛盾的公式,这个分支就是封闭的。而且我们可以看到,其实不 同分支之间是一种析取关系,整棵数可以看成一个析取式,每个分支的节点之间 是一种合取关系。如果分支中有互为矛盾的公式,那么说明它是一个矛盾式,如 果所有的分支都是矛盾式,其析取就是一个不可满足的结果。当然,我们也看到 语义表的制作需要的规则比较多。 范式方法和消解方法都是在范式的基础上进行的。消解方法只用到一条规 则,这样使得判定过程变得简单。消解到最后不要我们再去对剩下的公式做出判 断了,因为结果只有两种:空子句和非空子句,空子句说明公式是不可满足的, 非空而又不能继续消解的子句说明该子句是可以赋值为真的。第三节,弱消解 上一节我们介绍了怎样用消解方法来判定命题逻辑公式是否有效。我们对 一个公式不断地消解后,如果得到空句子就说明该公式逻辑蕴涵一个矛盾式,从 而说明它也是一个矛盾式。但是如果它不能消解到一个空句子,是否能说明它不 是一个矛盾式呢?答案是肯定的。因为如果一个合取范式不能继续消解,有以下 几种情况: ()一个空句子,我们不必再讨论了; ()各简单析取式中没有相同的原子公式; ( )各简单析取式中有相同的原子公式,但是它们是作为相同的析取支出 现的。1 张健,《逻辑公式的可满足性判定??方法、工具及应用》,科学出版社,2000年,北京, P18。 2 URL: 。12对于( ),我们可以对每个原子公式赋一个相应的值,使得其所在的析取 式取值为真,从而使得整个合取式为真,那么它不是矛盾式;对于( ),有相同 原子公式的不同析取支,我们对于该原子公式赋值使得这些析取式取值为真,其 它的析取式也可以赋值为真从而使得整个合取式为真。 总之,对于一个不能继续消解的公式,我们能够使得该公式有一个真的赋 值,从而说明它是一个非矛盾式。而整个过程可以给出机械的搜索策略。 从另一个角度来看,消解的目的是为了得到一个空子句,其做法就是不断 消解掉互为矛盾的部分,所以我们实际上可以这样消解:从公式((? )?(’ ?~ ))(其中 为任意公式)经过消解得到(?’ )。更进一步考虑,其实消 解的要求没有这么高,两个公式,只要它们是不同时取值为真,就可以消解了。 也就是满足逻辑方阵中的(上)反对关系的要求就可以了。为什么这样呢?下 面我们加以说明。 定义(反对关系):如果两个公式不可同真的话(其中一个公式为真的话, 另一个必然为假),我们说这两个公式具有反对关系。 定义(弱消解):设两个析取式 , , 中有析取支, 中有析取支’,和’有反对 关系;从 中消去 得到 ’,从 中消去’得到 ’,将 ’, ’析取得到一个新的析取式 ,称为消解 , 的弱消解式。 命题(弱消解原理),任意两个可以弱消解的合取式辑蕴涵它们的弱消解 式。 证明:设 和’是存在反对关系的两个公式,析取式 ’?, ’ ?’,其合取式为 ? ,消解式为 ,现要证明( ? )? 重言式,即 ( ’?)? ’?’ ?( ’? ’)是重言式: 我们对公式( ’?)? ’?’ ?( ’? ’)采用简化真 值表方法: ( ’?)? ’?’ ?( ’? ’) 最后 和’都为真了,出现矛盾,所以公式( ’? )? ’?’?( ’? ’) 是重言式。 证毕。1 彭漪涟:《逻辑学基础教程》,华东师范大学出版社, 年,上海, 。13 我们在学习传统形式逻辑中,有四个直言命题,分别为 、、、 ,其 中至少满足反对关系要求的有 和, 和, 和(即逻辑方阵中的上反对关 系和矛盾关系)。但是在谓词逻辑公式中,情形要更加复杂一些。我们来看看 下 面的情况是否可以消解: ,(")()? 和~()? 根据弱消解原理,可以消解得到?。 ,(") ()? 和~()? 我们首先用 替换 ,得到( )? 和~( )? ,消解得到 ()? ,(") ()? 和(")~() 我们知道公式 :(") ? ?((")?("))是有效式。 变形得到 :((" )~? ?(" ) )?(" )) ,我们把 中的 替换 为~ 得到(") ? ?(" )~ )?(") 。所以我们(") () ? 和(")~()可以消解得到(" )。 ,(") ()? 和(" )(~()?( )) 首先,由(" )(~( )?( ))可得到~()?()再根据, 我们可以将两个公式消解得到()?() 其次,我们知道:公式(" ) ( )? ?(" )(~( )? ( ))逻辑等值于公式 :(") ()? ?(~()?( ))逻辑蕴涵 : ( )? ?(~( ) ?( )),公式 逻辑蕴涵 : ?( ); 概括得到(") ?() 所以在此我们规定公式( ") ( )? ?(" )(~( )?( )) 可以消解得到(" ) ?()。 在此,我们对消解的限制就没有那么严格了。本节提到的弱消解和以上几 条规则我们统称为弱消解规则。起来,我们可以在下列情形下进行消解: 情形一,? 和~? 消解得到:?。 情形二,(")()? 和~()? 消解得到:?。 情形三,(") ()? 和~()? 消解得到: ?。 情形四,(") ( )? 和(" )~( )? 消解得到:(") ?。 情形五,(" )()? 和(" )(~()?( ))消解得到()?1 彭漪涟:《逻辑学基础教程》,华东师范大学出版社, 年,上海, ~ 。 2 彭漪涟:《逻辑学基础教程》,华东师范大学出版社, 年,上海, 。 3 冯棉,《经典逻辑和直觉主义逻辑》,上海人民出版社, 年,上海, 。14()或 者(" ) ?()。 我们在进行消解的过程中,可能会遇到有不同变元的公式,它们要得以消 解,需要在变元之间作一些替换。在可以进行变元替换的公式之间进行变元 替换, 我们遵从两个原则: 一, 在没有进行变元替换以前,如果有公式可以消解,那么替换要 等到所有可消解的部分完成消解后再进行。 二, 如果两个变元可以互相替换,比如,变元、,那么是用 替 换,还是用 替换 取决于哪种替换将可以得到最多的消解。 第四节,三段论的判定方法三段论规则 一个三段论是否有效,一般用以下四条规则就可以进行判定了: 规则,中项在前提中至少周延一次。 规则,如果大项或者小项在前提中不周延,那么在结论中也不得周延。 规则 ,如果两个前提都是否定的,那么它们不能得结论;前提之一是否定 的,结论也必须是否定的;结论是否定的,前提之中必有一个命题是否定的。 规则,两个特称前提不能得结论,前提之一是特称的,结论必须是特称 的。 凡恩图方法 用凡恩图表示出三段论中三个词项(大项、中项、小项)之间的外延关系, 然后可以通过图形来判断三段论是否有效。 三个变量的卡诺图法 在逻辑学上,卡诺图一般用来简化析取范式。它的画法是在一个长方形中 画出一些方格,变量被安排在长方形的边上,使得每一方格分别代表一变量或者 变量否定的合取式。画卡诺图的原则有两条:1,第一个变量一般放在长方形的 最上面一边上。 2,相邻的方格中的变量有且只有一对变量互相矛盾(互为否定)。 因为我们要用到三个变量的卡诺图,所以举一个相应的例子。设合取符号为“?”, 三个命题变量分别为 p, q, r,其否定分别为~p, ~q, ~r(在这里合取符号省略,即 pqr便表示p?q?r),这三个变量和其否定的合取式有: pqr, pq~r, p~qr, p~q~r, ~pqr, ~p~qr, ~pq~r, ~p~q~r。那么它们的卡诺图为: 15 我们注意到,第二条规则中要求的“相邻”,除了实际的图中的有公共边线 的格子外,还有长方形最左边的边和最右边的边也是相邻的边。当参量多的时候, 我们要将长方形上下左右都卷起来形成一个环形的圈,从而每个格子都有相同多 的邻格。 我们将简单性质命题A, E, I, O表示为集合的演算公式:SAP 表示为 Sn~P0;SEP表示为 SnP0;SIP表示为 S?P?0;SOP表示为 S?~P?0(其 中“~”表示否定符号、“=”为等于号、“?”为并、“?”为不等于号、“0”为 空集)。由此,我们设 S, M, P为三段论的大项,中项,小项;三个项在集合意义 下分别表示三个集合;卡诺图中的格子表示集合的区域,我们将每个格子从左到 右、从上到下用数字表示为 11、12、13、14、21、22、23、24。如果卡诺图的 某个区域是黑的,则表示这个格子没有元素;如果是灰的,则表示有元素;如果 是白的,则表示格子中没有区域不被元素充满。我们根据三段论集合表示方 法和 卡诺图的规定就可以判定三段论的有效性了。下面我们分别举两个例子一个是 有效的三段论,一个是无效的三段论来说明卡诺图的用法。例 1(如左图):对于三段论的第一格的 AAA 式,我们将它表达为集合演算公式:M?~P0; S ?~M0; 那么 S?~P0。画出卡诺图如左所示, 那么由 M?~P0知格子 12、13应涂黑,由 S? ~M0知格子 23、24应涂黑。现在我们来看结论 S?~P0,说的是 S和~P的相交区域 13、23是 黑,而这正是左图所显示的,那么该三段论有效。16 例 2(如右图):对于三段论的第二格的 AII式,我们将它表示为集合演算公式:P&~M0; S&M?0; 那么 S&P?0。画出卡诺图如右所示,那么由 P&~M0 知格子 21、24应涂黑,由 S&M?0知格子 13、14应 涂灰。现在我们来看结论 S&P?0,说的是 S和 P的 相交区域 14、24是灰,我们看到 14是灰的,但因为 13、14哪个区域有元素是不确定的,可能 14没有元 素。由此可知,这个三段论是无效的三段论。 4.4笛卡儿坐标方法。 如上,我们还是将简单性质命题A, E, I, O表示为集合的演算公式:SAP表 示为 S?~P0;SEP表示为 S?P0;SIP表示为 S?P?0;SOP表示为 S?~P ?0。我们将建立三维的笛卡儿坐标,三条坐标相交于原点,坐标的正向分别为 集合字母 S, M, P。负向为它们的否定~S, ~M, ~P。其中坐标平面将坐标分成 8个 象限,象限的分布是由正向形成的区域开始,然后逆时针方向,自上至下分别将 八个象限标识为第 1象限、第 2象限、第 3象限、第 4象限、第 5象限、第 6 象限、第 7象限、第 8象限;即,第 1象限的为 S?M?P的元素。第 2象限的 为~S?M?P的元素。第 3象限的为~S?M?~P的元素。第 4象限的为 S?M? ~P的元素。第 5象限的为 S?~M?P的元素。第 6象限的为~S?~M?P的元素。 第 7象限的为 S~?~M?~P的元素。第 8象限的为 S?~M?~P的元素。下面, 我们举一个例子来说明如何使用笛卡儿坐标判断一个三段论的有效性问题。 例 3(如左图):对于三段论的第二格的 AII式, 我们将它表达为集合演算公式: P&~M0; S&M#0; 那么 S&P#0。由 P&~M0知道左图的 笛卡儿坐标中第 5、第 6象限没有元素;由 S&M#0 知第 1或者第 2象限或者两个象限有元素;结论 S&P#0说得是第 1、第 5或者这两个象限有元素。 已知第 5象限没有元素,第 1象限是否有元素是 不定的所以结论错,从而判断出这个三段论是无 效的。 17我们同样可以象处理凡恩图和卡诺图一样来处理笛卡儿坐标,即在其八个 象限里着色,规则可以和以上我们对卡诺图的着色方法一样,但因为相同,且二 维平面表示三维量有些局限(比如在八个象限中着色,有的象限着色的话,会使 得另外得想象不可见),所以我们在此不再重复。 4.5消解方法 那么怎样利用消解方法来判定一个三段论是否有效呢? 首先,我们知道一个三段论是由三个论题组成,一个三段论是否有效就看 这个三段论的前提是否逻辑蕴涵其结论。也就说大前提加小前提是否逻辑蕴涵结 论。任意一个三段论,比如它的前提为、 ,结论为 ,那么一个三段论可以表 示为??,而(??)、(~(?)? )、(~((?)?~ ))彼此 等值,就是说,要判定一个三段论?? 是否有效,即是要判定~((?) ?~)是否有效,即要判定(?)?~ 是否不可满足(矛盾)。 、、、 四种命题分别为所有的 是,所有的 不是,有的 是, 有的 不是,可以分别表示为:("x)(S(x)?(x)),("x)(S(x)?~ (x)),($x)(S(x)?(x)),($x)(S(x)?~(x)),进而表示为("x) (~S(x)? (x)),("x)(~S(x)?~(x)),($x)(S(x)?(x)), 1 ($x)(S(x)?~(x))。为了消解的方便,我们将量词消去,但是出现变 元的地方,都认为变元是全称的,对于存在量词辖域内的变元,代替为个体常 元。 于是上述公式分别为~S(x)?(x),~S(x)?~(x),S(a)?(a), S(a)?~(a)。 对于任何一个三段论,我们根据弱消解规则进行消解。 例 1,判定三段论的第一格 AAA式(前提为 MAP,SAM,结论为 SAP) 是否有效