信息与计算科学毕业设计

安徽建筑工业学院安徽建筑工业学院毕 业 设 计 (论 文)专专 业业 信息与计算科学信息与计算科学 班班 级级 07 信息（信息（2）班）班 学生姓名学生姓名 汪保来汪保来 学学 号号 07207010214 课课 题题 不同逻辑间翻译的完备性不同逻辑间翻译的完备性 指导教师指导教师 王焕宝王焕宝 2011 年年 5 月月 31 日日安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）II不同逻辑间翻译的完备性汪保来(安徽建筑工业学院数理系，合肥 230022)摘要摘要: 数理逻辑是用数学方法来研究推理的形式结构和推理规律的数学学科.它与数学的其他分支、计算机科学、人工智能、语言学等学科均有密切的联系，它日益显示出它的重要作用和更加广泛的应用前景.数理逻辑是形式逻辑与数学思想结合的产物但数理逻辑研究的是各学科共同遵从的一般性的逻辑规律，而各门学科只研究自身的具体规律. 本论文讨论了在论域有限的情况下，命题逻辑与一阶逻辑的关系.该文提出了语义忠实和语义满两条逻辑性质来确保可满足的公式翻译为可满足的公式，不可满足公式翻译翻译为不可满足公式.本文说明了在 Henkin 语义下，二阶逻辑到一阶逻辑的翻译是满足完备性的.关键字关键字: : 完备性；语义忠实翻译；语义满翻译；二阶逻辑；一阶逻辑安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）IIILogical completeness on translationbetween different logicalAbstract Mathematical logic is to use mathematical methods to study the structure and reasoning 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 product 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 relationship 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 meets Completeness in Henkin semantics.Key words completeness; faithful translation; full translation; second-order logic; first-order目目 录录安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）IV摘要摘要.IIABSTRACT .III第一章第一章 绪论绪论.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分析一阶逻辑与命题逻辑间的公式间的关系.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.1 课题背景数理逻辑这门学科建立以后，发展比较迅速，促进它发展的因素也是多方面的.比如，非欧几何的建立，促使人们去研究非欧几何和欧氏几何的无矛盾性. 数理逻辑近年来发展特别迅速，主要原因是这门学科对于数学其它分支如集合论、数论、代数、拓扑学等的发展有重大的影响，特别是对新近形成的计算机科学的发展起了推动作用 .反过来，其他学科的发展也推动了数理逻辑的发展.正因为它是以门新近兴起而又发展很快的学科，所以它本身也存在许多问题有待于深入研究 .现在许多数学家正针对数理逻辑本身的问题进行研究.人工智能逻辑方面的研究很广阔，一般说来，所有的哲学逻辑都是人工智能逻辑，方向上涉及心理学、认知、决策、计算机等等都可以，数理逻辑和模态逻辑是它的基础.在人工智能知识表示领域根据不同的实际应用需求，人们可以使用多种不同的式工具表示知识.比如：直觉多值逻辑，模糊模态逻辑，描述逻辑等等.表达能力和推理任务是一个逻辑的两个重要的特征.面对这些不同形式的逻辑，如何比较它们在表达能力和推理任务上的差异，目前通常的做法是建立两个逻辑间的翻译，即把一个逻辑（源逻辑）翻译到另一个逻辑（目标逻辑）之上，怎样确保翻译是好的翻译，在提出语义忠实与语义满两条逻辑性质来说明可满足的公式翻译为可满足的公式，不可满足公式翻译翻译为不可满足公式，并进一步可以证明在 Henkin 语义下，二阶逻辑到一阶逻辑的语义忠实与语义满的翻译，也是满足完备性.应用前景，坦白说，不管是学人工智能逻辑还是数理逻辑，将来最合适的还是呆在研究机构里搞研究，而且主要是搞将元理论应用于其他理论的交叉研究；至于能否应用于实际，这个比前面说的将理论应用于理论要难很多，要看研究人员的机遇、原来的学科背景和能力了.1.2 主要问题及研究意义一个逻辑的表达能力可以从以下的 3 个角度来分析：（1）给定一个逻辑，什么样的符号串是该逻辑的公式（well-formed formula） ；（2）一个逻辑公式的语义解释；（3）利用翻译把一个逻辑翻译到另一个逻辑之上，然后比较两个安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）2逻辑的相对表达能力.现有的许多翻译主要侧重讨论两个逻辑间语法的对应关系，建立逻辑语言间的翻译和公式间的翻译，验证这样的翻译具备如下逻辑性质：（1）可靠性（the soundness）.对任意的公式，如果可满足则翻译后的公式也满足.（2）完备性（the completeness）.对任意的公式，如果可满足，则可满足.由式（1）和式（2）可知，公式的可满足性在可靠和完备的翻译下被保持.但是这样的翻译不保持不可满足性，即可靠的和完备的翻译可以将不可满足的公式翻译为可满足的公式.造成这一问题的主要原因是在建立翻译的时候只考虑了语言间的翻译和公式间的翻译，没有建立其相应的语义翻译.针对上述问题，定义一个逻辑到另一个逻辑间的翻译由语法层翻译和语义层翻译组成.语法层翻译是由逻辑语言间的翻译和公式间的翻译构成；语义层翻译是由模型间的翻译和赋值间的翻译构成.为了确保源逻辑的可满足公式翻译为目标逻辑的可满足公式，不可满足公式翻译为不可满足公式.安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）3第二章第二章 命题逻辑与一阶逻辑命题逻辑与一阶逻辑2.1 命题符号化及联结词 数理逻辑研究的中心问题是推理，而推理的前提和结论都是表达判断的陈述句.因而，表达判断的陈述句构成了推理的基本单位.于是，称能判断真假的陈述句为命题.这种陈述句的判断只有两种可能，一种是正确的判断，一种是错误的判断.称判断为正确的命题的真值为真，称判断为错误的命题的真值为假，因而又可以称命题逻辑是具有唯一真值的陈述句.如：（1）2 是素数.（2）3 能被 2 整除.（1）和（2）都是简单的陈述句，都不能分解成更简单的句子，称这样的命题为简单命题或原子命题.本论文中用小写的英文字母，p， ，, ,表示简单命题，将表示命题的符号放在该命题的前面，qripiqir称为命题符号化.以上讨论的是简单命题.在命题逻辑中，主要是研究由简单命题用联结词联结而成的命题，这样的命题称为复合命题.以下是对联结词的定义：定义 2.1.1 设为任一命题.复合命题“非”（或“的否定”）称2 ppp为的否定式，记作.为否定联结词.为真当且仅当为假.pppp定义 2.1.2 设，为两命题.复合命题“并且”（或“和”）2 pqpqpq称作与的合取式，记作.为合取联结词.为真当且仅当与同pqpqpqpq时为真.定义 2.1.3 设，为两命题.复合命题“或”称作与的析取式，2 pqpqpq记作.为析取联结词.为真当且仅当与中至少一个为真.pqpqpq定义 2.1.4 设，为两命题.复合命题“如果，则”称作与的2 pqpqpq蕴涵式，记作，称蕴涵式的前件，为蕴涵式的后件.称作蕴涵联结pqpq词.为假当且仅当为真且为假.pqpq定义 2.1.5 设，为两命题.复合命题“当且仅当”称作与的2 pqpqpq等价式，记作.称作等价联结词.真当且仅当，真值相同.pqpqpq安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）42.2 命题公式及分类 真值可以变化的简单陈述句称为命题变项或命题变元，也用， ，pqr, ,表示.命题变项不是命题.若在复合命题中， 等不仅可以ipiqirpqr代表常项，还可以代表命题变项，这样组成的复合命题形式称为命题公式.抽象的说，命题公式是由命题常项，命题变项，联结词，括号等组成的符号串.但并不是由这些符号组成的符号串都是命题公式，因而，必须给出命题公式的严格定义：定义定义 2.2.12.2.1 （1）单个命题常项或变项， ，, ,，0，1pqripiqir是合式公式；（2）如果是合式公式，则（）也是合式公式；AA（3）如果，是合式公式，则（） ， （） ， （） ， （ABABABAB）也是合式公式；AB（4）只有有限次地应用（1）（3）组成的符号串才是合式公式.在本论文中将合式公式称为命题公式，或简称为公式.定义定义 2.2.22.2.2 设为一个命题公式.A（1）若在它的各种赋值下取值均为真，则称为重言式或永真式；AA（2）若在它的各种赋值下取值均为假，则称为矛盾式或永假式；AA（3）若至少存在一组赋值是成真赋值，则是可满足式.AA2.3 一阶逻辑基本概念在一阶逻辑中，简单命题被分解成个体词和谓词两部分.所谓个体词是指可以独立存在的客体，它可以是一个具体的事物，也可以是一个抽象的概念.例如，李明，玫瑰花，黑板，自然数等都可以作为个体词.而谓词是刻画个体词的性质或个体词之间关系的词，如下面 2 个简单命题中：（1）王宏是程序员.（2）小李比小赵高 2 厘米.“王宏”，“小李”，“小赵”都是个体词.“.是程序员”，“.比.高 2 厘米”都是谓词.表示具体的或特定的个体的词称为个体常项，一般用小写的英文自母,ab,.表示.表示抽象的，或泛指的个体的词称为个体变项，常用小写英文字母c，表示.个体变项的取值范围称为个体域或论域，个体域可以是有xyz限事物的集合，也可以是无限事物的集合.称表示具体性质或关系的谓词谓词常项，用大写英文字母，FGH表示，例如表示“是无理数”.而表示抽象的或泛指的谓词称为谓词变项，F也用，表示.个体变项具有性质，记作.个体变项，FGHxF( )F xx安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）5具有性质，记作，论文中称这种个体变项和谓词的联合体，yL( , )L x y2 ( )F x等为谓词.( , )L x y2.4 量词在一阶命题逻辑中，除了个体词和谓词外，还有表示数量的词，称表示数量的词为量词.量词有两种：1.全称量词：对应日常语言中的“一切” ， “所有的” ， “任意的”等词，用符号“”表示.表示对个体域里的所有个体.表示个体域里的所有x( )xF x个体都有性质.F2.存在量词：对应日常语言中的“存在着” ， “有一个” ， “至少有一个”等词，用符号“”表示.表示存在个体域里的个体.表示存在着个体域x( )xF x里的个体具有性质.F命题逻辑中的五中联结词在一阶逻辑中均可应用.2.5 一阶逻辑的合式公式定义定义 2.5.12.5.1 项的定义如下：（1） 个体常项和变项是项（2） 若是任意元函数， ，是项，则12( ,.,)nx xxn1t2tnt也是项；12( , ,.,)nt tt（3） 只有有限次的使用（1） ， （2）生成的符号串才是项.定义定义 2.5.22.5.2 设是任意的元谓词， ，是项，则称12( ,.,)nR x xxn1t2tnt为原子公式.12( , ,.,)nR t tt定义定义 2.5.32.5.3 合式公式的定义如下：（1） 原子公式是合式公式；（2） 若是合式公式，则（）也是合式公式；AA（3） 若 ，是合式公式，则（） ， （） ， （） ， （）ABABABABAB也是合式公式；（4） 若是合式公式，则，也是合式公式；AxAxA（5） 只有有限次地应用（1）（4）构成的符号串才是合式公式（也称谓词公式）.定义定义 2.5.42.5.4 设为一谓词公式，如果在任何赋值下都是真的，则称为逻辑AAA有效式；如果在任何赋值下都是假的，则称是不可满足式；若至少存在一AA个赋值使为真，则是可满足式.AA安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）62.6 一阶逻辑的模型及赋值一般情况下，一个一阶逻辑合式公式中含有：个体常项，个体变项，谓词变项等.由此我们可以定义一个模型：I定义定义 2.6.12.6.1 一个模型由下面 4 部分组成：I9 （1） 非空个体域；D（2）中一部分特定元素；D（3）上一些特定的函数；D（4）上一些特定的谓词；D对各种变项指定特殊的常项去代替，就构成了一个公式的赋值.2.7 命题逻辑与一阶逻辑的关系2.7.1 总体说明两者的关系总体说明两者的关系在谓词中所包含的个体词数称为元数.含（）个个体词的谓词称为n1n 元谓词.用表示元谓词，它是以个体变项的个体域为定义域n12( ,.)nP x xxn（论文中为有限域） ，以0，1为值域的元函数，在这里个个变项的顺序不nn能随意改动.谓词不是命题，它的真值无法确定，要想使它成为命12( ,.)nP x xx题，必须指定某一谓词常项代替，同时还要用个个体常项代替个个体变Pnn项.例如，是一个 2 元谓词，它不是命题.当令表示“小于”( , )L x y( , )L x yxy之后，该谓词中的谓词部分已为常项，但它还不是命题.当取为 2，为 3 时，ab才是命题，并且是真命题.当取 为 2，为 1 时，为假命题.将不( , )L a bcd( , )L c d带个体变项的谓词称为 0 元谓词，例如，等都是 0 元谓词.一旦( , )L a b( , )L c d其中的的意义明确之后，0 元谓词都是命题.因而命题逻辑中的简单命题都可L以用 0 元谓词表示.2.7.2 分析一阶逻辑与命题逻辑间的公式间的关系分析一阶逻辑与命题逻辑间的公式间的关系在上文我们定义可知个体变项和谓词（在这里我们规定此谓词为谓词常项）的联合体，等为谓词，我们又知在一阶逻辑中，简单命题被分为个( )F x( , )L x y体词和谓词（这里的谓词是谓词常项）.由上文对命题变元的定义可知，命题变元可被分为个体变项与谓词.所以我们可以对，等谓词可以用命题( )F x( , )L x y逻辑中的命题变元，表示.所以可以总结出：pq安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）7设是含一阶逻辑的原子公式，的谓词公式，0A1A2AnA，是个命题变元或命题常元，可以用处处代替（） ，1p2pnpnipiA1in 所得命题公式称为的替代.A0A在有限域中，如，由量词的意义对于任意的谓词，都12 ,.,nDa aa( )A x有：（1），此时的为个12( )()().()nxA xA aA aA a8 ( )(1,2,., )iA ainia体常项，即为 0 元谓词，则可以用命题逻辑中的简单命题表示.所以对( )iA aip此形式的在命题逻辑中可以用复合命题来表示.( )xA x12.nppp（2），此时的为个12( )()().()nxA xA aA aA a8 ( )(1,2,., )iA ainia体常项，即为 0 元谓词，则可以用命题逻辑中的简单命题表示.所以对( )iA aiq此形式的在命题逻辑中可以用复合命题表示.( )xA x2.inqqq2.7.3 实例讨论一阶逻辑与命题逻辑间的关系实例讨论一阶逻辑与命题逻辑间的关系对于谓词公式，并且对模型赋值为个体域为有限域( )( )xF xxF x ，这里没有特定元素和函数，谓词定义为“大于 0”.由以上1,2,3D ( )F xx的一阶逻辑与命题逻辑公式间的替换规则可知，该谓词公式可以替换为命题逻辑中的复合命题公式（）（）.我们知道 0 元谓词就123ppp123ppp是命题逻辑中的简单命题，在这里就是表示的意义，即 大于 0.对ip( )(1,2,3)F i i i赋值后的谓词公式进行分析，在这里表示“1，2，3( )( )xF xxF x ( )xF x都大于 0” ，则为真，在这里表示“在 1，2，3 中存在大于 0 的( )xF x( )xF x数” ，则为真，可知谓词公式在此种赋值情况下为真.( )xF x( )( )xF xxF x 分析翻译后的复合命题公式（）（） ，由表示的意123ppp123pppip义可知为真，则和都为真，则复合命题公式（ip123ppp123ppp）（）为真，有以上分析，可以归纳为：123ppp123ppp（1） 谓词公式：；( )( )xF xxF x （2） 个体域；1,2,3D （3） 谓词：表示“大于 0” ；( )F xx（4） 翻译：（）（） （( )( )xF xxF x 123ppp123ppp表示“ 大于 0” ，与意义相同） ；并且在这种赋值情况(1,2,3)ip i i( )(1,2,3)F i i 下替换前和替换后的公式的真值都为真.上面的例子说明在模型中不一定要写出特定元素与特定的函数，下面的例子来做含有此两项的讨论：对于一阶逻辑合式公式，规( ( ( )( ,( )x F f xG a f x定个体域为；中的特定元素；函数为，2,3D D2a ( )f x(2)3f安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）8；谓词表示“是偶数” ，表示“大于” ；有公式间的(3)2f( )F xx( , )G x yxy替换规则可知可被替换为命题逻辑中的复合公式( ( ( )( ,( )x F f xG a f x，并且与表示相同的意义，即“3 是偶数” ，所以1122()()pqpq1p( (2)F f的真值为假，与表示相同的意义，即“2 是偶数” ，所以的真值1p2p( (3)F f2p为真；与表示相同的意义.即“2 大于 2” ，所以真值为假，与1q( ,(2)G a f1q2q表示相同的意义，即“2 大于 3” ，真值为假，可知( ,(3)G a f2q的真值为假；而此时表示“在 2，31122()()pqpq( ( ( )( ,( )x F f xG a f x中存在偶数并且存在着小于 2 的数” ，可知的真值为假.( ( ( )( ,( )x F f xG a f x在这里要知道函数的定义域与值域必须是论域的除空集的子集，如果值( )f xD域不是论域的除空集的子集，比如说的值域有不是中的元素，则对谓词( )f xD进行赋值时就会含有不是论域中的个体常项，则进一步就说明论域要含有D，则与不含有矛盾，所以的值域论域的除空集的子集.D( )f xD安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）9第三章第三章 二阶逻辑二阶逻辑3.1 二阶逻辑的简介为了得到比一阶逻辑更丰富，更富有表现力的语言，我们可以对谓词符号和函数符号添加量词.例如，是一个谓词公式，而( ( )( )x P xxP x是一个二阶逻辑的公式.为了说明二阶逻辑的公式，下面( ( )( )P x P xxP x 介绍一下逻辑符号：（1） 谓词变元：对于每个正整数，我们有元谓词变元，10nn1nX2nX（2） 函数变元：对于每个正整数，我们有元函数变元，10nn1nF2nF下面定义二阶逻辑的合式公式：定义定义 5.5.15.5.1 设是任意的元谓词， ，是项，则称12( ,.,)nR x xxn1t2tnt为原子公式.12( , ,.,)nR t tt定义定义 5.5.25.5.2 合式公式的定义如下：（1） 原子公式是合式公式；（2） 若是合式公式，则（）也是合式公式；AA（3） 若 ，是合式公式，则（） ， （） ， （） ， （）ABABABABAB也是合式公式；（4） 若是合式公式，则，也是合式公式；AxAxA（5） 若是合式公式，则，也是合式公式；AniX AniF A（6） 只有有限次地应用（1）（5）构成的符号串才是合式公式.对于二阶逻辑的模型其满足一阶逻辑模型的 4 部分，并且有所扩展：设是V所有个体变元，谓词变元和函数变元的集合，并设 是上的函数，且满足sV是论域中的一个元素，是论域中的元关系，是元运算，1( )s v()ns XUn()ns Fn这样可知谓词变元和函数变元的集合为.2U11现在对二阶逻辑做出总结，在这之前我们我们来看一个定义：定义定义 5.5.35.5.3 若任一真值函数都可以用仅含某一联结词集中的联结词的命题公式表示，则称该联结词集为全功能集.由定义 5.5.3 可知为一全功能集，在证明这个结论前，先来介绍几, 6 个等值式，设为任意的命题公式：12,A B（蕴涵等值式）ABAB (双重否定律)AA （等价等值式）()()ABABBA，；（德.摩根律）()ABAB ()ABAB 证明：由以上分析可知 5 个联结词组成的联结词集为.由于, , , 安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）10（1）pq （双重否定律）pqpq （蕴涵等值式）pqpq 即pqpq （2）pq（双重否定律）()pqpq （德.摩根律）()()pqpq （蕴涵等值式）()()pqpq 即()pqpq （3）pq（等价等值式）()()pqpqqp（双重否定律）()()()()pqqppqqp （德.摩根律）()()( ()()pqqppqqp （蕴涵等值式）( ()()()()pqqppqqp 由定义 5.5.1 可知为全功能集 ，证完., 我们可以用替换.x x7 由以上我们总结二阶逻辑：二阶逻辑语言包含下列符号：元谓词符号：，；n0p1p逻辑联结词：；, 全称量词符号：；个体变元：，；0 x1x函数变量符号和谓词变量符号：，；0X1X标点符号：（， ）.二阶逻辑的公式，定义为：12( , ,.,)|( )|()nR t ttxxXX 二阶逻辑有两种语义：一种是标准语义；另一种是 Henkin 语义.如果二1 阶逻辑采用的是标准语义，那么完备性定理在二阶逻辑中不成立；如果二阶逻辑采用的是 Henkin 语义，那么完备性定理在二阶逻辑中成立.二阶逻辑在 Henkin 语义下的模型是一个三元组（， ） ，MUnn NAI其中为一个非空集合，为的非空子集，表示函数变量符号和谓词变量UnA2U符号的取值域，是一个解释，使得是上的带类型的关系.nXnAIIpU一个赋值函数 是变量集合到模型论域上的一个函数：对于任何个体变量， vx；对任何函数变量和谓词变量，.( )v xUnXnnXA 二阶逻辑在 Henkin 语义下到一阶逻辑的翻译既是语义满的又是语义忠安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）11实的.1 3.2 二阶逻辑到一阶逻辑的翻译的性质3.2.1 性质的介绍及证明性质的介绍及证明一个逻辑到另一个逻辑间的翻译由语法层翻译和语义层翻译组成.语法层翻译是由逻辑语言间的翻译和公式间的翻译构成；语义层翻译是由模型间的翻译和赋值间的翻译组成.现在用表示一个逻辑，表示逻辑所在的逻辑语言；SS表示可满足关系；假定的逻辑语言不含相等符号；表示上全体|S( )FormS公式所构成的集合；表示上所有模型所构成的集合；是上所有( )ModS( )vS赋值所构成的集合，给出如下到翻译的定义：SS定义定义 3.2.13.2.1 给定两个逻辑和，一个到的翻译是满足如下条件的SSSS一个映射：（1）语法层.对中的任意非逻辑符号 ，映射 为中的非逻辑符号；1 ss对中的任意公式，映射为中的公式.( )Form()Form（2）语法层.对中的任意模型，映射为中的模型；1 ( )ModMM()Mod对中的任意赋值 ，映射中的赋值.( )vv()v定义定义 3.2.23.2.2 设是到的一个翻译，如果满足：对于任意给定的上SSS的公式，模型，赋值 ，都有（， ）当且仅当（，）MvMv|()M( )v，则称为一个语义忠实的翻译.|( ) 定义定义 3.2.33.2.3 设是到的一个翻译，如果满足：对于任意给定的3 SS上的公式，任意的模型，赋值都有：如果（，），那SSMvMv|( ) 么存在的模型和赋值 使得（， ）并且，则SMvMv|()MM( )vv称为一个语义满的翻译.命题命题 3.2.43.2.4.如果一个翻译是到的既语义忠实又语义满的翻译，那么SS对的任意公式，在中不可满足当且仅当在中不可满足.SS( ) S证明：假设在中不可满足但是在中可满足，那么存在模型和赋S( ) SM值使得（，）.因为是语义满翻译，所以就有：的模型和vMv|( ) SM赋值 使得（， ）.这与在中不可满足矛盾.反之，若在中vMv|S( ) S不可满足，但是在中可满足，那么存在模型和赋值 使得（， ）SSMvMv.因为是语义忠实的翻译，所以就有（，）.这与|()M( )v|( ) 在中不可满足矛盾.证毕.( ) S安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）123.2.2 完备性定理完备性定理定义定义 3.2.53.2.5（协调性）（表示公式的集合） ，当且仅当4 ( )Form ，使得并且（表示形式可推演性关系）( )AFormA A14定义定义 3.2.63.2.6 （极大协调性）公式集是极大协调的，当且仅当满足15一下的（1）和（2）：（1）是协调集；（2）对于任何，是不协调的.A A定理定理 3.2.73.2.7 设是极大协调集.于是，对于任何，当且仅当.AA A证明：如果，则有（） ，.下面证明其逆命题，设.如果AAA ，则由于是极大协调的，所以是不协调的.于是，因而A AA不协调，这与的极大协调性矛盾.因此.A定理定理 3.2.83.2.8 设是极大协调集.则对于任何和，AB（1），当且仅当；A A（2），当且仅当并且；ABAB（3），当且仅当或；ABAB（4），当且仅当蕴涵；ABAB（5），当且仅当等值于.ABAB证明：证（1）先证.设.如果，则有（）可得AA A A和，即是不协调的，与假设的的极大协调性矛盾.因此.AA A 下面证.设，如果，则可依次得到：AA AA （1）是不协调的；A （2）；A （3）.A这与矛盾.因此.AA 证（2）先证并且.设并且.由定理 3.2.7 可ABAB AB得及（） （如果，则）：A B AB（1）；AA （2）.BB 因此.AB 下面证并且.设.如果“并且”ABA BABAB不成立，则依次可得：（1），；AB （2）， （由本定理（1） ） ；AB安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）13（3）（由本定理（2） ） ；AB （4）；AB （5）AB 又由假设可知，这样是不协调的，与的极大协调性矛盾.因ABAB此并且.AB证（3）先证或.设或.由定理 3.2.7 及ABAB AB（） （如果则，）可得：A ABBA（1）；AAABAB （2）.BBABAB 因此.AB 下面证或.设.如果“或”不ABA BABAB成立，则依次可得：（1），；AB （2）， （由本定理（1） ） ；AB（3）（由本定理（3） ） ；AB （4）；AB （5）()AB又由假设可知，这样是不协调的，与的极大协调性矛盾.因ABAB此或.AB证（4）先证蕴涵.有定理 3.2.7 及（） （如果，ABABA 则,）和（） （如果,则）：A ABABB.B , ABABAB因此AB 下面证蕴涵.如果“蕴涵”不成立，ABABAB依次可得：（1），；AB（2）（由本定理（1） ） ；B （3）（由本定理（3） ） ；AB （4）；AB（5）()AB 又由于可知，即，这样是不协调的，与AB()AB()AB 的极大协调性矛盾.因此蕴涵.AB证（5）先证等值于.由定理 3.2.7 及（） （如果ABAB ，则）和（）可得：, AB,BAAB安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）14（1）；AA ,BA （2）；,BBAB 由（1） （2）可知，所以.ABAB下面证等值于.如果“等值于”不成立，ABABAB依次可得：（1），；AB（2）（由本定理（1） ） ；B （3）（由本定理（1） ， （2） ， （3） ） ；( ()()ABBA （4）；( ()()ABBA （5）()()ABBA又由于可知，这样是不协调的，与的AB()()ABBA极大协调性矛盾.所以等值于.证毕.AB定理定理 3.2.93.2.9 如果，存在有限的，使得.A 0 0A 证：对的结构作归纳.AA基始.有规则（Ref）生成的的前提本身是一个公式，所以16AAA有定理中所说的性质.AA归纳步骤.证明在剩下十种推演规则的情形.规则（）的情形：如果，A 则，.A由归纳假设，存在有限的，使得.也是，的有限子集.因0 0A 0此规则（）保存定理中所说的性质.规则（）的情形： 如果，AB ，AB 则.A 我们先要证明：（1）存在有限的，使得，.1 1AB（2）存在有限的，使得，.2 2AB由归纳假设，存在有限的，使得.若，则是 ,A B A 的有限子集.根据（） ，有可得，.令，这就B AB1AB是（1）.若，则是的有限子集.令.我们有A A 1A ，从而得到（1）.1,A （2）的证明是类似的.安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）15 根据（） ，可以由（1）和（2）得到： 1，2AB 1，2AB由此可得，其中的，是的有限子集.故规则（）保存12A 125 定理中所说的性质. 规则（）的情形： 如果，AB A ， 则.B 由归纳假设，存在的有限子集和，使得并且.根据121AB2A （） ，可得： 1，2AB 1，.2A 于是有，其中的，是的有限子集.故规则（）保存定理12B 12 中所说的性质.其他情形的证明是类似的.由基始和归纳步骤，定理得证.定理定理 3.2.103.2.10（Lindenbaum）任何协调的公式集能够扩充为极大协调集.17证：设是协调的公式集.是可数无限集.另( )Form（1），是所有公式的任何一个排列.定义的无限0A1A2A( )nForm 序列（）如下：0n 0 ，如果协调，则，否则 ；于是有：nnA 1nnnA 1nn （2）.1nn （3）是协调的.n其中的（2）是显然的， （3）能够由对作归纳而证明.n令.显然有.下面证明是本定理所要求的极大协调集.*nn N * *先证是协调集.如果不协调，即有，使得并且.根据*B*B *B定理 3.2.9，有中的有限个公式，和，使得：*1BkB1kBlB 1B，；kBB 1kB，.lBB由此得到： 1B，.lBBB故，是不协调的.1BlB设，并且.由（2）可得，(1)iitBil 1max( ,.,)nttt1BlBt 安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）16因此是不协调的，这和（3）矛盾.故是协调的.t*令，即.是（1）中的公式，令.根据的构*C(0)nCnCmCA1m作情形，可知（即）是不协调的.（如果是协调的，mmA mC mmA 则，因此，即，这与，矛盾.）1mmmA 1mmA1mCnC (0)n 这样，因为，故是不协调的，因此是极大协调集.*m * C *引理 3.2.11 设是极大协调集.构作真假赋值 ，使得对于任何原*()pForm v子公式，当且仅当，于是，对于任何，当且p1vp *p()pAForm1vA 仅当.*A证明：对的结构作归纳.A基始.是原子公式.由假设，引理成立.A归纳步骤.有，或五种情形.ABBCBCBCBCAB 的情形：*B （由定理 3.2.8（1） ）*B（由归纳假设）0vB .()1vBABC的情形：*BC或（由定理 3.2.8（3） ）*B*C或（由归纳假设）1vB 1vC ()1vBCABC的情形 BC*并且（由定理 3.2.8（2） ）*B*C并且（由归纳假设）1vB 1vC ()1vBCABC的情形：*BC蕴涵（由定理 3.2.8（4） ）*B*C蕴涵（由归纳假设）1vB 1vC ()1vBCABC的情形： *BC 等值于（由定理 3.2.8（5） ）*B*C安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）17 等值于（由归纳假设）1vB 1vC ()1vBC由基始和归纳步骤，引理得证.定理 3.2.12（完备性）设，()pForm ()pAForm（1）如果是协调的，则是可满足的；（2）如果是协调的，则是可满足的.AA证：设是协调的.取任何.把扩充为极大协调集（由定理 3.2.10） ，B*则有.由引理 3.2.11，使用其中的真假赋值 ，可得.因此 满足，*Bv1vB v这就证明了（1）.（2）是（1）的特殊情形.得证.3.2.3 二阶逻辑到一阶逻辑翻译的完备性的分析二阶逻辑到一阶逻辑翻译的完备性的分析如果二阶逻辑在 Henkin 语义下的翻译不是完备性翻译，我们可令二阶逻辑合式公式集是满足完备性的，但翻译为一阶逻辑的合式公式集后不满足完*备性了，由定理 3.2.12 可以说是可满足的合式公式但翻译为一阶逻辑合式公式集后含有了不可满足的公式，即有二阶逻辑中的可满足公式翻译为一阶逻*辑的不可满足公式.我们又知道二阶逻辑在 Henkin 语义下与一阶逻辑的翻译既是语义忠实又是语义满的翻译，这样由命题 3.2.4 可知一阶逻辑不可满足式翻译前在二阶逻辑中只能是不可满足式，这与是满足完备性相矛盾.所以二阶逻辑在 Henkin 语义下翻译为一阶逻辑是完备性翻译.安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）18第四章第四章 总结与展望总结与展望4.1 总结本文分阐述了命题逻辑与一阶逻辑，通过分析它们的概念与定义，了解到了在论域有限的情况下，命题逻辑与一阶逻辑的关系，总结出了他们公式间所对应的关系.本文定义了一个逻辑到另一个逻辑间的翻译是由语法层翻译和语义层翻译组成.语法层翻译是由逻辑语言间的翻译和赋值间的翻译构成.为了确保源逻辑的可满足公式翻译为目标逻辑的可满足公式，不可满足公式翻译为目标逻辑的不可满足公式翻译为目标逻辑的不可满足公式，本文定义了翻译的两条逻辑性质：语义忠实性和语义满性.本文说明了在 Henkin 语义下二阶逻辑到一阶逻辑的翻译是语义忠实与语义满的翻译的情况下，这个翻译也是满足完备性的.4.2 展望由上面的总结，下一步需进一步研究命题逻辑与一阶逻辑在无限论域下的关系.二阶逻辑有两种不同语义：一种是标准语义；另一种是 Henkin 语义；我们可以研究完备性定理在标准语义下是否成立.安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）19参考文献参考文献1申宇铭，马越 ,不同逻辑间翻译的逻辑性质 ,计算机学报，2009，32(10):2091-2097.2耿素云，屈婉凌，张立昂，离散数学（第四版） ，清华大学出版社，2008.3Boolos G. On second-order logic.Journal of Philosophy，1975，72(16):509-527.4陆钟万，面向计算机科学的数理逻辑（第二版） ，科学出版社，2007.5石纯一, 数理逻辑与集合论(第二版)，清华大学出版社，2000.6Herbert 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 王国俊，一阶逻辑完备性定理的代数证明，陕西师范大学学报，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 IJCA91.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安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）20致谢致谢在论文完成之际，我真心感谢所有给予我关怀和帮助的人.衷心感谢我的指导老师王焕保老师在论文期间对我的悉心指导.从课题的提出到实现方案的确定，王老师始终对我的工作给予了大量的帮助和鼓励，有对成绩的表扬与肯定，也有对错误的批判与宽容.王老师严谨的治学态度、豁达的胸怀都深深地影响并启发着我，将使我终生受益. 最后，衷心感谢各位评委的批评和指导.安徽建筑工业学院安徽建筑工业学院 毕业设计（论文）21