信息与计算科学毕业设计.doc

《信息与计算科学毕业设计.doc》由会员分享，可在线阅读，更多相关《信息与计算科学毕业设计.doc（24页珍藏版）》请在三一办公上搜索。

1、安徽建筑工业学院毕 业 设 计 (论 文)专 业 信息与计算科学 班 级 07信息（2）班 学生姓名 汪保来 学 号 07207010214 课 题 不同逻辑间翻译的完备性 指导教师 王焕宝 2011年5月31日不同逻辑间翻译的完备性汪保来(安徽建筑工业学院数理系，合肥230022)摘要: 数理逻辑是用数学方法来研究推理的形式结构和推理规律的数学学科.它与数学的其他分支、计算机科学、人工智能、语言学等学科均有密切的联系，它日益显示出它的重要作用和更加广泛的应用前景.数理逻辑是形式逻辑与数学思想结合的产物但数理逻辑研究的是各学科共同遵从的一般性的逻辑规律，而各门学科只研究自身的具体规律. 本论文

2、讨论了在论域有限的情况下，命题逻辑与一阶逻辑的关系.该文提出了语义忠实和语义满两条逻辑性质来确保可满足的公式翻译为可满足的公式，不可满足公式翻译翻译为不可满足公式.本文说明了在Henkin语义下，二阶逻辑到一阶逻辑的翻译是满足完备性的.关键字: 完备性；语义忠实翻译；语义满翻译；二阶逻辑；一阶逻辑Logical completeness on translationbetween different logicalAbstract Mathematical logic is to use mathematical methods to study the structure and reaso

3、ning in the form of the law of mathematics reasoning. It with other branches of mathematics, computer science, artificial intelligence, linguistics and other subjects are closely linked, It is increasingly shows its important role and a more broad application prospects. Mathematical Logic is the pro

4、duct of the combination of Formal Logic and mathematical thinking, but mathematical logic is the study of various disciplines together to comply with the general laws of logic, but All subjects only research their own specific rules. The situation of this paper discusses the domain limited , the rel

5、ationship between Propositional logic and first-order logic. In this paper, two logic properties: the failthfulness and the fullness are defined to ensure the preservations of the satisfiability and the unsatisfiability. In this paper, translation between Second-order logic and first-order logic mee

6、ts Completeness in Henkin semantics.Key words completeness; faithful translation; full translation; second-order logic; first-order目 录摘要IIABSTRACTIII第一章 绪论11.1课题背景11.2 主要问题及研究意义1第二章 命题逻辑与一阶逻辑32.1命题符号化及联结词32.2命题公式及分类42.3 一阶逻辑基本概念42.4量词52.5一阶逻辑的合式公式52.6一阶逻辑的模型及赋值62.7命题逻辑与一阶逻辑的关系62.7.1总体说明两者的关系62.7.2分析

7、一阶逻辑与命题逻辑间的公式间的关系62.7.3实例讨论一阶逻辑与命题逻辑间的关系7第三章 二阶逻辑93.1 二阶逻辑的简介93.2二阶逻辑到一阶逻辑的翻译的性质113.2.1 性质的介绍及证明113.2.2 完备性定理123.2.3 二阶逻辑到一阶逻辑翻译的完备性的分析17第四章 总结与展望184.1 总结184.2 展望18参考文献19致谢20 第一章 绪论1.1课题背景数理逻辑这门学科建立以后，发展比较迅速，促进它发展的因素也是多方面的.比如，非欧几何的建立，促使人们去研究非欧几何和欧氏几何的无矛盾性. 数理逻辑近年来发展特别迅速，主要原因是这门学科对于数学其它分支如集合论、数论、代数、拓

8、扑学等的发展有重大的影响，特别是对新近形成的计算机科学的发展起了推动作用.反过来，其他学科的发展也推动了数理逻辑的发展.正因为它是以门新近兴起而又发展很快的学科，所以它本身也存在许多问题有待于深入研究.现在许多数学家正针对数理逻辑本身的问题进行研究.人工智能逻辑方面的研究很广阔，一般说来，所有的哲学逻辑都是人工智能逻辑，方向上涉及心理学、认知、决策、计算机等等都可以，数理逻辑和模态逻辑是它的基础.在人工智能知识表示领域根据不同的实际应用需求，人们可以使用多种不同的式工具表示知识.比如：直觉多值逻辑，模糊模态逻辑，描述逻辑等等.表达能力和推理任务是一个逻辑的两个重要的特征.面对这些不同形式的逻辑

9、，如何比较它们在表达能力和推理任务上的差异，目前通常的做法是建立两个逻辑间的翻译，即把一个逻辑（源逻辑）翻译到另一个逻辑（目标逻辑）之上，怎样确保翻译是好的翻译，在提出语义忠实与语义满两条逻辑性质来说明可满足的公式翻译为可满足的公式，不可满足公式翻译翻译为不可满足公式，并进一步可以证明在Henkin语义下，二阶逻辑到一阶逻辑的语义忠实与语义满的翻译，也是满足完备性.应用前景，坦白说，不管是学人工智能逻辑还是数理逻辑，将来最合适的还是呆在研究机构里搞研究，而且主要是搞将元理论应用于其他理论的交叉研究；至于能否应用于实际，这个比前面说的将理论应用于理论要难很多，要看研究人员的机遇、原来的学科背景和

10、能力了.1.2 主要问题及研究意义一个逻辑的表达能力可以从以下的3个角度来分析：（1）给定一个逻辑，什么样的符号串是该逻辑的公式（well-formed formula）；（2）一个逻辑公式的语义解释；（3）利用翻译把一个逻辑翻译到另一个逻辑之上，然后比较两个逻辑的相对表达能力.现有的许多翻译主要侧重讨论两个逻辑间语法的对应关系，建立逻辑语言间的翻译和公式间的翻译，验证这样的翻译具备如下逻辑性质：（1）可靠性（the soundness）.对任意的公式，如果可满足则翻译后的公式也满足.（2）完备性（the completeness）.对任意的公式，如果可满足，则可满足.由式（1）和式（2）可知

11、，公式的可满足性在可靠和完备的翻译下被保持.但是这样的翻译不保持不可满足性，即可靠的和完备的翻译可以将不可满足的公式翻译为可满足的公式.造成这一问题的主要原因是在建立翻译的时候只考虑了语言间的翻译和公式间的翻译，没有建立其相应的语义翻译.针对上述问题，定义一个逻辑到另一个逻辑间的翻译由语法层翻译和语义层翻译组成.语法层翻译是由逻辑语言间的翻译和公式间的翻译构成；语义层翻译是由模型间的翻译和赋值间的翻译构成.为了确保源逻辑的可满足公式翻译为目标逻辑的可满足公式，不可满足公式翻译为不可满足公式.第二章 命题逻辑与一阶逻辑2.1命题符号化及联结词 数理逻辑研究的中心问题是推理，而推理的前提和结论都是

12、表达判断的陈述句.因而，表达判断的陈述句构成了推理的基本单位.于是，称能判断真假的陈述句为命题.这种陈述句的判断只有两种可能，一种是正确的判断，一种是错误的判断.称判断为正确的命题的真值为真，称判断为错误的命题的真值为假，因而又可以称命题逻辑是具有唯一真值的陈述句.如：（1）2是素数.（2）3能被2整除.（1）和（2）都是简单的陈述句，都不能分解成更简单的句子，称这样的命题为简单命题或原子命题.本论文中用小写的英文字母，,表示简单命题，将表示命题的符号放在该命题的前面，称为命题符号化.以上讨论的是简单命题.在命题逻辑中，主要是研究由简单命题用联结词联结而成的命题，这样的命题称为复合命题.以下是

13、对联结词的定义：定义2.1.1 设为任一命题.复合命题“非”（或“的否定”）称为的否定式，记作.为否定联结词.为真当且仅当为假.定义2.1.2 设，为两命题.复合命题“并且”（或“和”）称作与的合取式，记作.为合取联结词.为真当且仅当与同时为真.定义2.1.3 设，为两命题.复合命题“或”称作与的析取式，记作.为析取联结词.为真当且仅当与中至少一个为真.定义2.1.4 设，为两命题.复合命题“如果，则”称作与的蕴涵式，记作，称蕴涵式的前件，为蕴涵式的后件.称作蕴涵联结词.为假当且仅当为真且为假.定义2.1.5 设，为两命题.复合命题“当且仅当”称作与的等价式，记作.称作等价联结词.真当且仅当，

14、真值相同.2.2命题公式及分类 真值可以变化的简单陈述句称为命题变项或命题变元，也用，,表示.命题变项不是命题.若在复合命题中，等不仅可以代表常项，还可以代表命题变项，这样组成的复合命题形式称为命题公式.抽象的说，命题公式是由命题常项，命题变项，联结词，括号等组成的符号串.但并不是由这些符号组成的符号串都是命题公式，因而，必须给出命题公式的严格定义：定义2.2.1 （1）单个命题常项或变项，,，0，1是合式公式；（2）如果是合式公式，则（）也是合式公式；（3）如果，是合式公式，则（），（），（），（）也是合式公式；（4）只有有限次地应用（1）（3）组成的符号串才是合式公式.在本论文中将合式公式

15、称为命题公式，或简称为公式.定义2.2.2 设为一个命题公式.（1）若在它的各种赋值下取值均为真，则称为重言式或永真式；（2）若在它的各种赋值下取值均为假，则称为矛盾式或永假式；（3）若至少存在一组赋值是成真赋值，则是可满足式.2.3 一阶逻辑基本概念在一阶逻辑中，简单命题被分解成个体词和谓词两部分.所谓个体词是指可以独立存在的客体，它可以是一个具体的事物，也可以是一个抽象的概念.例如，李明，玫瑰花，黑板，自然数等都可以作为个体词.而谓词是刻画个体词的性质或个体词之间关系的词，如下面2个简单命题中：（1）王宏是程序员.（2）小李比小赵高2厘米.“王宏”，“小李”，“小赵”都是个体词.“.是程序

16、员”，“.比.高2厘米”都是谓词.表示具体的或特定的个体的词称为个体常项，一般用小写的英文自母,.表示.表示抽象的，或泛指的个体的词称为个体变项，常用小写英文字母，表示.个体变项的取值范围称为个体域或论域，个体域可以是有限事物的集合，也可以是无限事物的集合.称表示具体性质或关系的谓词谓词常项，用大写英文字母，表示，例如表示“是无理数”.而表示抽象的或泛指的谓词称为谓词变项，也用，表示.个体变项具有性质，记作.个体变项，具有性质，记作，论文中称这种个体变项和谓词的联合体，等为谓词.2.4量词在一阶命题逻辑中，除了个体词和谓词外，还有表示数量的词，称表示数量的词为量词.量词有两种：1.全称量词：对

17、应日常语言中的“一切”，“所有的”，“任意的”等词，用符号“”表示.表示对个体域里的所有个体.表示个体域里的所有个体都有性质.2.存在量词：对应日常语言中的“存在着”，“有一个”，“至少有一个”等词，用符号“”表示.表示存在个体域里的个体.表示存在着个体域里的个体具有性质.命题逻辑中的五中联结词在一阶逻辑中均可应用.2.5一阶逻辑的合式公式定义 2.5.1 项的定义如下：（1） 个体常项和变项是项（2） 若是任意元函数，是项，则也是项；（3） 只有有限次的使用（1），（2）生成的符号串才是项.定义 2.5.2 设是任意的元谓词，是项，则称为原子公式.定义 2.5.3 合式公式的定义如下：（1）

18、 原子公式是合式公式；（2） 若是合式公式，则（）也是合式公式；（3） 若 ，是合式公式，则（），（），（），（）也是合式公式；（4） 若是合式公式，则，也是合式公式；（5） 只有有限次地应用（1）（4）构成的符号串才是合式公式（也称谓词公式）.定义 2.5.4 设为一谓词公式，如果在任何赋值下都是真的，则称为逻辑有效式；如果在任何赋值下都是假的，则称是不可满足式；若至少存在一个赋值使为真，则是可满足式.2.6一阶逻辑的模型及赋值一般情况下，一个一阶逻辑合式公式中含有：个体常项，个体变项，谓词变项等.由此我们可以定义一个模型：定义2.6.1 一个模型由下面4部分组成：（1） 非空个体域；（2）

19、 中一部分特定元素；（3） 上一些特定的函数；（4） 上一些特定的谓词；对各种变项指定特殊的常项去代替，就构成了一个公式的赋值.2.7命题逻辑与一阶逻辑的关系2.7.1总体说明两者的关系在谓词中所包含的个体词数称为元数.含（）个个体词的谓词称为元谓词.用表示元谓词，它是以个体变项的个体域为定义域（论文中为有限域），以0，1为值域的元函数，在这里个个变项的顺序不能随意改动.谓词不是命题，它的真值无法确定，要想使它成为命题，必须指定某一谓词常项代替，同时还要用个个体常项代替个个体变项.例如，是一个2元谓词，它不是命题.当令表示“小于”之后，该谓词中的谓词部分已为常项，但它还不是命题.当取为2，为3

20、时，才是命题，并且是真命题.当取为2，为1时，为假命题.将不带个体变项的谓词称为0元谓词，例如，等都是0元谓词.一旦其中的的意义明确之后，0元谓词都是命题.因而命题逻辑中的简单命题都可以用0元谓词表示.2.7.2分析一阶逻辑与命题逻辑间的公式间的关系在上文我们定义可知个体变项和谓词（在这里我们规定此谓词为谓词常项）的联合体，等为谓词，我们又知在一阶逻辑中，简单命题被分为个体词和谓词（这里的谓词是谓词常项）.由上文对命题变元的定义可知，命题变元可被分为个体变项与谓词.所以我们可以对，等谓词可以用命题逻辑中的命题变元，表示.所以可以总结出：设是含一阶逻辑的原子公式，的谓词公式，是个命题变元或命题常

21、元，可以用处处代替（），所得命题公式称为的替代.在有限域中，如，由量词的意义对于任意的谓词，都有：（1），此时的为个体常项，即为0元谓词，则可以用命题逻辑中的简单命题表示.所以对此形式的在命题逻辑中可以用复合命题来表示.（2），此时的为个体常项，即为0元谓词，则可以用命题逻辑中的简单命题表示.所以对此形式的在命题逻辑中可以用复合命题表示.2.7.3实例讨论一阶逻辑与命题逻辑间的关系对于谓词公式，并且对模型赋值为个体域为有限域，这里没有特定元素和函数，谓词定义为“大于0”.由以上的一阶逻辑与命题逻辑公式间的替换规则可知，该谓词公式可以替换为命题逻辑中的复合命题公式（）（）.我们知道0元谓词就是命

22、题逻辑中的简单命题，在这里就是表示的意义，即大于0.对赋值后的谓词公式进行分析，在这里表示“1，2，3都大于0”，则为真，在这里表示“在1，2，3中存在大于0的数”，则为真，可知谓词公式在此种赋值情况下为真.分析翻译后的复合命题公式（）（），由表示的意义可知为真，则和都为真，则复合命题公式（）（）为真，有以上分析，可以归纳为：（1） 谓词公式：；（2） 个体域；（3） 谓词：表示“大于0”；（4） 翻译：（）（）（表示“大于0”，与意义相同）；并且在这种赋值情况下替换前和替换后的公式的真值都为真.上面的例子说明在模型中不一定要写出特定元素与特定的函数，下面的例子来做含有此两项的讨论：对于一阶逻

23、辑合式公式，规定个体域为；中的特定元素；函数为，；谓词表示“是偶数”，表示“大于”；有公式间的替换规则可知可被替换为命题逻辑中的复合公式，并且与表示相同的意义，即“3是偶数”，所以的真值为假，与表示相同的意义，即“2是偶数”，所以的真值为真；与表示相同的意义.即“2大于2”，所以真值为假，与表示相同的意义，即“2大于3”，真值为假，可知的真值为假；而此时表示“在2，3中存在偶数并且存在着小于2的数”，可知的真值为假.在这里要知道函数的定义域与值域必须是论域的除空集的子集，如果值域不是论域的除空集的子集，比如说的值域有不是中的元素，则对谓词进行赋值时就会含有不是论域中的个体常项，则进一步就说明论

24、域要含有，则与不含有矛盾，所以的值域论域的除空集的子集.第三章 二阶逻辑3.1 二阶逻辑的简介为了得到比一阶逻辑更丰富，更富有表现力的语言，我们可以对谓词符号和函数符号添加量词.例如，是一个谓词公式，而是一个二阶逻辑的公式.为了说明二阶逻辑的公式，下面介绍一下逻辑符号：（1） 谓词变元：对于每个正整数，我们有元谓词变元，（2） 函数变元：对于每个正整数，我们有元函数变元，下面定义二阶逻辑的合式公式：定义 5.5.1 设是任意的元谓词，是项，则称为原子公式.定义 5.5.2 合式公式的定义如下：（1） 原子公式是合式公式；（2） 若是合式公式，则（）也是合式公式；（3） 若 ，是合式公式，则（）

25、，（），（），（）也是合式公式；（4） 若是合式公式，则，也是合式公式；（5） 若是合式公式，则，也是合式公式；（6） 只有有限次地应用（1）（5）构成的符号串才是合式公式.对于二阶逻辑的模型其满足一阶逻辑模型的4部分，并且有所扩展：设是所有个体变元，谓词变元和函数变元的集合，并设是上的函数，且满足是论域中的一个元素，是论域中的元关系，是元运算，这样可知谓词变元和函数变元的集合为.现在对二阶逻辑做出总结，在这之前我们我们来看一个定义：定义 5.5.3 若任一真值函数都可以用仅含某一联结词集中的联结词的命题公式表示，则称该联结词集为全功能集.由定义5.5.3可知为一全功能集，在证明这个结论前，先

26、来介绍几个等值式，设为任意的命题公式：（蕴涵等值式）(双重否定律) （等价等值式），；（德.摩根律）证明：由以上分析可知5个联结词组成的联结词集为.由于（1） （双重否定律）（蕴涵等值式）即（2）（双重否定律）（德.摩根律）（蕴涵等值式）即（3）（等价等值式）（双重否定律）（德.摩根律）（蕴涵等值式）由定义5.5.1可知为全功能集 ，证完.我们可以用替换.由以上我们总结二阶逻辑：二阶逻辑语言包含下列符号：元谓词符号：，；逻辑联结词：；全称量词符号：；个体变元：，；函数变量符号和谓词变量符号：，；标点符号：（，）.二阶逻辑的公式，定义为：二阶逻辑有两种语义：一种是标准语义；另一种是Henkin语

27、义.如果二阶逻辑采用的是标准语义，那么完备性定理在二阶逻辑中不成立；如果二阶逻辑采用的是Henkin语义，那么完备性定理在二阶逻辑中成立.二阶逻辑在Henkin语义下的模型是一个三元组（， ），其中为一个非空集合，为的非空子集，表示函数变量符号和谓词变量符号的取值域，是一个解释，使得是上的带类型的关系.一个赋值函数是变量集合到模型论域上的一个函数：对于任何个体变量， ；对任何函数变量和谓词变量，. 二阶逻辑在Henkin语义下到一阶逻辑的翻译既是语义满的又是语义忠实的.3.2二阶逻辑到一阶逻辑的翻译的性质3.2.1 性质的介绍及证明一个逻辑到另一个逻辑间的翻译由语法层翻译和语义层翻译组成.语法

28、层翻译是由逻辑语言间的翻译和公式间的翻译构成；语义层翻译是由模型间的翻译和赋值间的翻译组成.现在用表示一个逻辑，表示逻辑所在的逻辑语言；表示可满足关系；假定的逻辑语言不含相等符号；表示上全体公式所构成的集合；表示上所有模型所构成的集合；是上所有赋值所构成的集合，给出如下到翻译的定义：定义3.2.1 给定两个逻辑和，一个到的翻译是满足如下条件的一个映射：（1） 语法层.对中的任意非逻辑符号，映射为中的非逻辑符号；对中的任意公式，映射为中的公式.（2） 语法层.对中的任意模型，映射为中的模型；对中的任意赋值，映射中的赋值.定义 3.2.2 设是到的一个翻译，如果满足：对于任意给定的上的公式，模型，

29、赋值，都有（，）当且仅当（，），则称为一个语义忠实的翻译.定义 3.2.3 设是到的一个翻译，如果满足：对于任意给定的上的公式，任意的模型，赋值都有：如果（，），那么存在的模型和赋值使得（，）并且，则称为一个语义满的翻译.命题3.2.4.如果一个翻译是到的既语义忠实又语义满的翻译，那么对的任意公式，在中不可满足当且仅当在中不可满足.证明：假设在中不可满足但是在中可满足，那么存在模型和赋值使得（，）.因为是语义满翻译，所以就有：的模型和赋值使得（，）.这与在中不可满足矛盾.反之，若在中不可满足，但是在中可满足，那么存在模型和赋值使得（，）.因为是语义忠实的翻译，所以就有（，）.这与在中不可满足矛

30、盾.证毕.3.2.2 完备性定理定义3.2.5（协调性）（表示公式的集合），当且仅当，使得并且（表示形式可推演性关系）定义3.2.6 （极大协调性）公式集是极大协调的，当且仅当满足一下的（1）和（2）：（1）是协调集；（2）对于任何，是不协调的.定理3.2.7设是极大协调集.于是，对于任何，当且仅当.证明：如果，则有（），.下面证明其逆命题，设.如果，则由于是极大协调的，所以是不协调的.于是，因而不协调，这与的极大协调性矛盾.因此.定理3.2.8 设是极大协调集.则对于任何和，（1），当且仅当；（2），当且仅当并且；（3），当且仅当或；（4），当且仅当蕴涵；（5），当且仅当等值于.证明：证（1

31、）先证.设.如果，则有（）可得和，即是不协调的，与假设的的极大协调性矛盾.因此. 下面证.设，如果，则可依次得到：（1）是不协调的；（2）；（3）.这与矛盾.因此.证（2）先证并且.设并且.由定理3.2.7可得及（）（如果，则）：（1）；（2）.因此. 下面证并且.设.如果“并且”不成立，则依次可得：（1），；（2）， （由本定理（1）；（3）（由本定理（2）；（4）；（5）又由假设可知，这样是不协调的，与的极大协调性矛盾.因此并且.证（3）先证或.设或.由定理3.2.7及（）（如果则，）可得：（1）；（2）.因此. 下面证或.设.如果“或”不成立，则依次可得：（1），；（2）， （由本定理（

32、1）；（3）（由本定理（3）；（4）；（5）又由假设可知，这样是不协调的，与的极大协调性矛盾.因此或.证（4）先证蕴涵.有定理3.2.7及（）（如果，则,）和（）（如果,则）：.因此 下面证蕴涵.如果“蕴涵”不成立，依次可得：（1），；（2）（由本定理（1）；（3）（由本定理（3）；（4）；（5）又由于可知，即，这样是不协调的，与的极大协调性矛盾.因此蕴涵.证（5）先证等值于.由定理3.2.7及（）（如果，则）和（）可得：（1）；（2）；由（1）（2）可知，所以.下面证等值于.如果“等值于”不成立，依次可得：（1），；（2）（由本定理（1）；（3）（由本定理（1），（2），（3）；（4）；（5

33、）又由于可知，这样是不协调的，与的极大协调性矛盾.所以等值于.证毕.定理 3.2.9如果，存在有限的，使得.证：对的结构作归纳.基始.有规则（Ref）生成的的前提本身是一个公式，所以有定理中所说的性质.归纳步骤.证明在剩下十种推演规则的情形.规则（）的情形：如果， 则，.由归纳假设，存在有限的，使得.也是，的有限子集.因此规则（）保存定理中所说的性质.规则（）的情形： 如果， ， 则.我们先要证明：（1）存在有限的，使得，.（2）存在有限的，使得，.由归纳假设，存在有限的，使得.若，则是的有限子集.根据（），有可得，.令，这就是（1）.若，则是的有限子集.令.我们有，从而得到（1）.（2）的证

34、明是类似的. 根据（），可以由（1）和（2）得到： ， ，由此可得，其中的，是的有限子集.故规则（）保存定理中所说的性质. 规则（）的情形： 如果， ， 则.由归纳假设，存在的有限子集和，使得并且.根据（），可得： ， ，.于是有，其中的，是的有限子集.故规则（）保存定理中所说的性质.其他情形的证明是类似的.由基始和归纳步骤，定理得证.定理 3.2.10（Lindenbaum）任何协调的公式集能够扩充为极大协调集.证：设是协调的公式集.是可数无限集.另（1），是所有公式的任何一个排列.定义的无限序列（）如下：，如果协调，则，否则 ；于是有：（2）.（3）是协调的.其中的（2）是显然的，（3）能

35、够由对作归纳而证明.令.显然有.下面证明是本定理所要求的极大协调集.先证是协调集.如果不协调，即有，使得并且.根据定理3.2.9，有中的有限个公式，和，使得： ，； ，.由此得到： ，.故，是不协调的.设，并且.由（2）可得，因此是不协调的，这和（3）矛盾.故是协调的.令，即.是（1）中的公式，令.根据的构作情形，可知（即）是不协调的.（如果是协调的，则，因此，即，这与，矛盾.）这样，因为，故是不协调的，因此是极大协调集.引理3.2.11设是极大协调集.构作真假赋值，使得对于任何原子公式，当且仅当，于是，对于任何，当且仅当.证明：对的结构作归纳.基始.是原子公式.由假设，引理成立.归纳步骤.有

36、，或五种情形.的情形：（由定理3.2.8（1）（由归纳假设）.的情形：或（由定理3.2.8（3）或（由归纳假设）的情形 并且（由定理3.2.8（2）并且（由归纳假设）的情形：蕴涵（由定理3.2.8（4）蕴涵（由归纳假设）的情形： 等值于（由定理3.2.8（5） 等值于（由归纳假设） 由基始和归纳步骤，引理得证.定理3.2.12（完备性）设，（1）如果是协调的，则是可满足的；（2）如果是协调的，则是可满足的.证：设是协调的.取任何.把扩充为极大协调集（由定理3.2.10），则有.由引理3.2.11，使用其中的真假赋值，可得.因此满足，这就证明了（1）.（2）是（1）的特殊情形.得证.3.2.3

37、二阶逻辑到一阶逻辑翻译的完备性的分析如果二阶逻辑在Henkin语义下的翻译不是完备性翻译，我们可令二阶逻辑合式公式集是满足完备性的，但翻译为一阶逻辑的合式公式集后不满足完备性了，由定理3.2.12可以说是可满足的合式公式但翻译为一阶逻辑合式公式集后含有了不可满足的公式，即有二阶逻辑中的可满足公式翻译为一阶逻辑的不可满足公式.我们又知道二阶逻辑在Henkin语义下与一阶逻辑的翻译既是语义忠实又是语义满的翻译，这样由命题3.2.4可知一阶逻辑不可满足式翻译前在二阶逻辑中只能是不可满足式，这与是满足完备性相矛盾.所以二阶逻辑在Henkin语义下翻译为一阶逻辑是完备性翻译.第四章 总结与展望4.1 总

38、结本文分阐述了命题逻辑与一阶逻辑，通过分析它们的概念与定义，了解到了在论域有限的情况下，命题逻辑与一阶逻辑的关系，总结出了他们公式间所对应的关系.本文定义了一个逻辑到另一个逻辑间的翻译是由语法层翻译和语义层翻译组成.语法层翻译是由逻辑语言间的翻译和赋值间的翻译构成.为了确保源逻辑的可满足公式翻译为目标逻辑的可满足公式，不可满足公式翻译为目标逻辑的不可满足公式翻译为目标逻辑的不可满足公式，本文定义了翻译的两条逻辑性质：语义忠实性和语义满性.本文说明了在Henkin语义下二阶逻辑到一阶逻辑的翻译是语义忠实与语义满的翻译的情况下，这个翻译也是满足完备性的.4.2 展望由上面的总结，下一步需进一步研究

39、命题逻辑与一阶逻辑在无限论域下的关系.二阶逻辑有两种不同语义：一种是标准语义；另一种是Henkin语义；我们可以研究完备性定理在标准语义下是否成立.参考文献1 申宇铭，马越,不同逻辑间翻译的逻辑性质,计算机学报，2009，32(10):2091-2097.2 耿素云，屈婉凌，张立昂，离散数学（第四版），清华大学出版社，2008.3 Boolos G. On second-order logic.Journal of Philosophy，1975，72(16):509-527.4 陆钟万，面向计算机科学的数理逻辑（第二版），科学出版社，2007.5 石纯一, 数理逻辑与集合论(第二版)，清华大

40、学出版社，2000.6 Herbert B.Enderton，A Mathematicatical Introduction to Logic(Second Edition).7 孙明湘，李建华，关系命题的语形和语义，湖南科技大学学报，2004，7(2):19-22.8 杜国平，命题逻辑语法完全性问题，浙江社会科学,1994，1：156-159.9 熊明，一阶逻辑的内涵语义，湖南科技大学学报，2006，9(6):27-31.10 张立群，鹿旭东，蒋志方，曲阜师范大学学报，2000，26(3):49-50.11 王彦华,计算机科学中的离散数学,信息与电脑,2009,7:120-121.12 王国

41、俊，一阶逻辑完备性定理的代数证明，陕西师范大学学报，2002，30(4):7-11.13 王湘云，一阶谓词逻辑在人工智能知识表示中的应用，重庆工学院学报，2007，21(9):69-71.14 张锦华，命题逻辑及谓词逻辑推理证明中的化归法，福建电脑，2009，9：167-168.15 张一民，孙吉贵，一阶逻辑模型生成器的实现，吉林大学学报，2004，42(2):189-194.16 Kara M. How to prove higher order theorems in first order logic/Mylopoulos J.Reiter R eds.Proceedings of IJ

42、CA91.Sydney,1991:137-142.17 hlhaeh H，Sehmidt RFunctional translation and secondorder frame properties of modal logicsJournal of Logic and Computation，19977(5)：581-603致谢在论文完成之际，我真心感谢所有给予我关怀和帮助的人.衷心感谢我的指导老师王焕保老师在论文期间对我的悉心指导.从课题的提出到实现方案的确定，王老师始终对我的工作给予了大量的帮助和鼓励，有对成绩的表扬与肯定，也有对错误的批判与宽容.王老师严谨的治学态度、豁达的胸怀都深深地影响并启发着我，将使我终生受益. 最后，衷心感谢各位评委的批评和指导.