逻辑公理系统马殿富马殿富北航计算机学院北航计算机学院dfmabuaa.edu.cndfmabuaa.edu.cn202010-1210-12计算机学院2计算机学院2 2主要内容主要内容概述概述命题逻辑公理系统命题逻辑公理系统谓词逻辑公理系统谓词逻辑公理系统总结总结计算机学院3计算机学院3 3科学的数学化科学的数学化数学描述自然规律数学描述自然规律伽利略落体定律发现，使他成为精确描述伽利略落体定律发现，使他成为精确描述自然知识的创始人。自然知识的创始人。经典物理学中的因果原理经典物理学中的因果原理牛顿用数学描述自然规律牛顿用数学描述自然规律；用数学函数表达的事件间的相互联系用数学函数表达的事件间的相互联系。每。每一事件均被解释为状态的变化；每一状态一事件均被解释为状态的变化；每一状态均由某些量值表明其特征，而每一自然律均由某些量值表明其特征，而每一自然律则陈述这些量值的各种变化之间的关系，则陈述这些量值的各种变化之间的关系，正是这些量值的变化描述了各种各样的事正是这些量值的变化描述了各种各样的事件。件。微分方程；微分方程；函数论；函数论；泛函分析；泛函分析；拓扑学、运筹学拓扑学、运筹学数学依然是自然规律描述方法数学依然是自然规律描述方法伽利略伽利略牛顿牛顿计算机学院4计算机学院4 4科学知识表达科学知识表达人类的知识人类的知识 英英 罗素罗素关于人类的知识我们可以提出两个问题：关于人类的知识我们可以提出两个问题：第一、我们知道什么？第一、我们知道什么？第二、第二、我们是怎样知道这些知识的我们是怎样知道这些知识的？科学知识的目的在于去掉一切个人的因素，说出人类科学知识的目的在于去掉一切个人的因素，说出人类集体智慧的发现。集体智慧的发现。语言，这个我们借以表达科学知识的唯一工具语言，这个我们借以表达科学知识的唯一工具自然哲学自然哲学 德德 莫里茨莫里茨. .石里克石里克自然知识表述为命题自然知识表述为命题；所有的自然律也同样是以命题；所有的自然律也同样是以命题的形式来表达的。的形式来表达的。自然科学的全部任务仅仅就在于坚持不懈地审查其命自然科学的全部任务仅仅就在于坚持不懈地审查其命题的正确性，结果这些命题就发展成为越来越牢固地题的正确性，结果这些命题就发展成为越来越牢固地确立的假设。确立的假设。自然科学在普遍性之外还具有精确性自然科学在普遍性之外还具有精确性。精确知识就是。精确知识就是那种可以按照逻辑的原则完全地清楚地表达出来的知那种可以按照逻辑的原则完全地清楚地表达出来的知识。识。一门科学所达到的抽象程度越高，它洞察实在的本质一门科学所达到的抽象程度越高，它洞察实在的本质就愈深。就愈深。石里克石里克罗素罗素计算机学院5计算机学院5 5科学认识方法科学认识方法观察和经验与数学演绎结合起来，建立了近代科学。观察和经验与数学演绎结合起来，建立了近代科学。用数学方程式形式来表述物理规律，这就似乎物理必然用数学方程式形式来表述物理规律，这就似乎物理必然性也可以变换为数学必然性；性也可以变换为数学必然性；数学方法中给近代物理学以预言能力；数学方法中给近代物理学以预言能力；自然的规律具有数学规律的结构、必然性和普遍性自然的规律具有数学规律的结构、必然性和普遍性建立理论模型，形成重要定理建立理论模型，形成重要定理数学分析、数学物理方程数学分析、数学物理方程逻辑定理逻辑定理通过解释，将数学规律的确定性又被移转到物理现象，通过解释，将数学规律的确定性又被移转到物理现象，把数学预言得精确成果变为可以验证的物理学成果。把数学预言得精确成果变为可以验证的物理学成果。计算机学院6计算机学院6 6公理化哲学的思考公理化哲学的思考世界的逻辑构造世界的逻辑构造构造系统的任务要把一切概念都构造系统的任务要把一切概念都从某些基本概念中逐步地引导出从某些基本概念中逐步地引导出来，形成概念系谱。来，形成概念系谱。一种理论的公理化就在于：一种理论的公理化就在于：这个理论的全部命题都被安排在这个理论的全部命题都被安排在以公理为其基础的演绎系统中以公理为其基础的演绎系统中; ;这个理论的全部概念都被安排在这个理论的全部概念都被安排在以基本概念为其基础的构造系统以基本概念为其基础的构造系统中。中。鲁道夫鲁道夫卡尔纳普卡尔纳普(R.Carnap 1891-1970)计算机学院7计算机学院7 7公理系统公理系统亚里士多德的演绎证明逻辑结构：亚里士多德的演绎证明逻辑结构：基本概念基本概念通过定义派生概念通过定义派生概念公理或公设公理或公设通过逻辑证明定理通过逻辑证明定理由初始概念、定义、公理、推理规则、定理等所构成由初始概念、定义、公理、推理规则、定理等所构成的演绎体系，称为公理系统。的演绎体系，称为公理系统。三个公理系统三个公理系统实质公理学：欧几里德，实质公理学：欧几里德， 几何原本几何原本概括公理：罗巴切夫斯基和黎曼，非欧几何概括公理：罗巴切夫斯基和黎曼，非欧几何形式公理：希尔伯特，形式公理：希尔伯特，几何基础几何基础计算机学院8计算机学院8 8欧几里德几何学欧几里德几何学几何原本几何原本是一个实质公理系统是一个实质公理系统把点、线、面、角等分为原始定义概念把点、线、面、角等分为原始定义概念（2323）和可定义概念；）和可定义概念；命题分为公理（命题分为公理（5 5）、公设（）、公设（5 5）；）；由公理公设出发加以证明的定理（由公理公设出发加以证明的定理（467467）从简单到复杂，证明相当严格。从而建立了从简单到复杂，证明相当严格。从而建立了欧几里得几何学的第一个公理化数学体系。欧几里得几何学的第一个公理化数学体系。欧几里德欧几里德325 BC -265 BC 1 1等于同量的量彼此相等等于同量的量彼此相等2 2等最加等量，其和仍相等等最加等量，其和仍相等3 3，等量减等量，其差仍相等，等量减等量，其差仍相等4 4彼此能重合的物体是全等的彼此能重合的物体是全等的5 5整体大于部分整体大于部分1. 1.由任意一点到另外任意一点可以画直线。由任意一点到另外任意一点可以画直线。2. 2.一条有限直线可以继续延长。一条有限直线可以继续延长。3. 3.以任意点为心及任意的距离可以画圆。以任意点为心及任意的距离可以画圆。4. 4.凡直角都彼此相等。凡直角都彼此相等。5. 5.平行公理平行公理计算机学院9计算机学院9 9非欧几何非欧几何俄国数学家罗巴切夫斯基发现了锐角非俄国数学家罗巴切夫斯基发现了锐角非欧几何。欧几何。从直线外一点，至少可以做两条直线和从直线外一点，至少可以做两条直线和这条直线平行。这条直线平行。三角形内角和小于三角形内角和小于9090度，圆周率大于度，圆周率大于 。18541854年黎曼发现了钝角非欧几何。年黎曼发现了钝角非欧几何。在同一平面内任何两条直线都有交点。在同一平面内任何两条直线都有交点。三角形内角和大于三角形内角和大于9090度，圆周率小于度，圆周率小于 。计算机学院10计算机学院1010非欧几何的模型非欧几何的模型意大利数学家贝尔特拉米的模型：意大利数学家贝尔特拉米的模型：“伪球面伪球面”它由平面曳物线绕其渐近线旋转一周而得。它由平面曳物线绕其渐近线旋转一周而得。18681868年用伪球面作为罗氏几何的平面有限部分的年用伪球面作为罗氏几何的平面有限部分的模型模型18691869提出用球面作为黎曼的二重椭圆几何模型。提出用球面作为黎曼的二重椭圆几何模型。18701870年，德国数学家克莱因用不包括圆周的年，德国数学家克莱因用不包括圆周的圆内部一罗氏平面一来解释罗巴切夫斯基几圆内部一罗氏平面一来解释罗巴切夫斯基几何的工作，使非欧几何在欧氏几何中得到解何的工作，使非欧几何在欧氏几何中得到解释。释。1919世纪末，希尔伯特在实数算术理论中为欧世纪末，希尔伯特在实数算术理论中为欧氏几何建立了一个模型。氏几何建立了一个模型。贝尔特拉米和克莱因使非欧几何建立在欧氏贝尔特拉米和克莱因使非欧几何建立在欧氏几何模型上；希尔伯特使欧氏几何建立在实几何模型上；希尔伯特使欧氏几何建立在实数模型上。数模型上。计算机学院11计算机学院1111希尔伯特希尔伯特几何基础几何基础希尔伯特希尔伯特18991899年发表了年发表了几何基础几何基础，完成了公理几何学的，完成了公理几何学的形式化。用准确的语言，严格地叙述了欧儿里得几何。形式化。用准确的语言，严格地叙述了欧儿里得几何。 重新定义了几何元素，点、线、面这三个基本概念此没有定义，也重新定义了几何元素，点、线、面这三个基本概念此没有定义，也没有直观的解释，其它概念是基本概念的导出概念，这是形式公理没有直观的解释，其它概念是基本概念的导出概念，这是形式公理方法的特征方法的特征确立了五组确立了五组2020条公理（分别是条公理（分别是8 8条关联公理，条关联公理，4 4条顺序公理，条顺序公理，5 5条合同条合同公理，公理，2 2条连续公理，条连续公理，1 1条平行公理）条平行公理）这个系统可以有各种不同的解释即模型。这个系统可以有各种不同的解释即模型。给出了欧氏几何的一个形式公理系统，而丛具体地解决了公给出了欧氏几何的一个形式公理系统，而丛具体地解决了公理方法的一些逻辑理论问题。理方法的一些逻辑理论问题。第一个逻辑理论问题是公理的无矛盾性第一个逻辑理论问题是公理的无矛盾性在实数的算术理论中为欧氏几何构造一个模型，这就是笛卡儿几何，在此模型中在实数的算术理论中为欧氏几何构造一个模型，这就是笛卡儿几何，在此模型中欧几里德几何五组公理都真。欧几里德几何五组公理都真。第二个逻辑理论问题是公理的相互独立性第二个逻辑理论问题是公理的相互独立性利用模型方法作出了证明。利用模型方法作出了证明。计算机学院12计算机学院1212形式公理学形式公理学形式公理几何学形式公理几何学通过一组公理隐含的定义对象、运算和关系；通过一组公理隐含的定义对象、运算和关系；一组公理既限制了对象、运算及关系可能作出的解释，一组公理既限制了对象、运算及关系可能作出的解释，又充当系统推导时所需的一切前提；又充当系统推导时所需的一切前提；这种公理系统可以有多种不同的解释，所以称为形式这种公理系统可以有多种不同的解释，所以称为形式公理学。公理学。计算机学院13计算机学院1313公理系统比较公理系统比较实质公理：欧几里德，实质公理：欧几里德， 几何原本几何原本对象、性质和关系先是具体唯一给定的；对象、性质和关系先是具体唯一给定的；给定具体初始概念，以及具体导出概念；给定具体初始概念，以及具体导出概念；公理是从已知的事实中选出的少数自明的基本原理；公理是从已知的事实中选出的少数自明的基本原理；用演绎推理来证明这个对象域中的真理用演绎推理来证明这个对象域中的真理欧几里得几何和牛顿力学都是实质公理学。欧几里得几何和牛顿力学都是实质公理学。概括公理：罗巴切夫斯基和黎曼，非欧几何概括公理：罗巴切夫斯基和黎曼，非欧几何抽象初始概念；抽象初始概念；从直观的空间上升到抽象的空间，几何公理不具有自明性；从直观的空间上升到抽象的空间，几何公理不具有自明性；数学绝对真理变为相对真理数学绝对真理变为相对真理形式公理：希尔伯特，形式公理：希尔伯特，几何基础几何基础抽象的符号对象域；抽象的符号对象域；初始概念不加定义；初始概念不加定义；公理是初始概念的定义；公理是初始概念的定义；公式形式的推演；公式形式的推演；对初始概念经过不同的解释，一个形式公理系统可以有许多论域（模型）。对初始概念经过不同的解释，一个形式公理系统可以有许多论域（模型）。计算机学院14计算机学院1414主要内容主要内容概述概述命题逻辑公理系统命题逻辑公理系统谓词逻辑公理系统谓词逻辑公理系统总结总结计算机学院15计算机学院1515逻辑公理系统逻辑公理系统公理系统公理系统从一些从一些公理公理出发，根据出发，根据演绎法演绎法，推导出一系列，推导出一系列定理定理，形成的演绎体，形成的演绎体系叫作系叫作公理系统公理系统。公理系统的组成：公理系统的组成：符号集；符号集；公式集公式集公式是用于表达命题的符号串；公式是用于表达命题的符号串；公理集公理集公理是用于表达推理由之出发的初始肯定命题；公理是用于表达推理由之出发的初始肯定命题；推理规则集推理规则集推理规则是由公理及已证定理得出新定理的规则；推理规则是由公理及已证定理得出新定理的规则；定理集定理集表达了肯定的所有命题。表达了肯定的所有命题。计算机学院16计算机学院1616命题逻辑的公理系统命题逻辑的公理系统定义定义3.1 3.1 命题逻辑的公理系统定义命题逻辑的公理系统定义: :符号符号命题变元命题变元p p1 1,p ,p2 2, ,p pn n联结词符号联结词符号，; ;括号括号(,)(,)合式公式合式公式命题变元是合式公式；命题变元是合式公式；若若Q Q是公式，则是公式，则( (Q)是合式公式；是合式公式；若若Q,RQ,R是公式，则是公式，则(Q(QR)R)是合式公式。是合式公式。定义了所有合式公式定义了所有合式公式计算机学院17计算机学院1717命题逻辑的公理系统命题逻辑的公理系统有以下三个公理模式，其中有以下三个公理模式，其中P,Q,RP,Q,R可为任意公式可为任意公式公理模式公理模式A1Q Q (RQ)公理模式公理模式A2(P(P (QR) (PQ) (PR)公理模式公理模式A3( (Q R) (RQ)推理规则推理规则( (分离规则分离规则,MP,MP规则规则) )从从Q Q和和Q QR R推出推出R RQ Q和和Q QR R称为前提称为前提R R称为结论称为结论计算机学院18计算机学院1818公理系统公理系统罗素公理系统罗素公理系统Q Q Q Q Q QQ QQ Q R RQ Q R RR R Q Q(P(PQ)Q)(P(P R RQ Q R R) )弗雷格公理系统弗雷格公理系统Q(RQ)(P(QR) (PQ) (PR)(P(QR) (Q(PR)(QR) (RQ)QQQQ卢卡西维茨公理系统卢卡西维茨公理系统Q(RQ)(P(QR) (PQ) (PR)(QR) (R Q)计算机学院19计算机学院1919缩写公式缩写公式QR=(QR)QR= (QR)QR=(QR) (RQ)QR= (QR)计算机学院20计算机学院2020公式复杂度公式复杂度公式公式Q的复杂度表示为的复杂度表示为FC(Q)命题变元复杂度为命题变元复杂度为0 0，如果，如果Q是命题变元，则是命题变元，则FC (Q)=0。如果公式如果公式Q= R，则，则FC (Q)=FC(R)+1。如果公式如果公式Q=R1R2，则，则FC (Q)=maxFC(R1), FC(R2)+1。计算机学院21计算机学院2121推理序列推理序列已知已知Q成立成立， 证明证明RQ成立成立A1= Q (RQ) A A1A2= Q Q A3= RQ推理序列推理序列 =Q，公式集，公式集前提前提A A1 1、A A2 2、A A3 3 推理序列推理序列A A3 3 结论结论计算机学院22计算机学院2222演绎与推理序列演绎与推理序列定义定义3.2 3.2 设设是合式公式集是合式公式集, , Q Q是是合式公式，有推理步骤合式公式，有推理步骤A A1 1,A,A2 2, ,A An n，公式序列，公式序列 1 1, , 2 2, , n n ，其中，其中A A1 1=1 1A A2 2=2 2. .A An n=n n ( ( n n =Q=Q) )每个每个 k k满足以下条件之一，满足以下条件之一，(1) (1) 是公理；是公理；(2) (2) k k ；(3) (3) 有有i,jk i,jk k k= = i i j j由由 i i, , j j用用MPMP规则规则推出。推出。则称它为则称它为Q Q的从的从的一个的一个推演推演( (演绎演绎) ), ,记为记为 Q Q。 称为推演的称为推演的前提集前提集，称称为为结论结论推理序列推理序列如果推理步骤序列如果推理步骤序列是是A A1 1,A,A2 2, ,A An n，则推则推理序列长度理序列长度n n。推论：推论：如果如果Q Q是公理或是公理或 Q ，则则 Q计算机学院23计算机学院2323证明与定理证明与定理如果存在从如果存在从推演出推演出Q，则记为，则记为Q 。Q1,Q2,QnQ简记为简记为Q1,Q2,Qn Q 如果如果为空集为空集 ，则记为，则记为Q。如果如果Q，并且有推理步骤，并且有推理步骤A1,A2,An，则则A1,A2,An称为的一个称为的一个证明证明。如果如果Q ，则，则Q称为称为定理定理。计算机学院24计算机学院2424P, Q(PR)QRA1= P A1A2=P (QP) A1 A1 A3=QP A2 = A1 A3 A4= Q(PR) A4 A5= (Q(PR)(QP)(QR) A2 A2 A6= (QP)(QR) A5 = A4A6 A7= (QR) A6 = A3A7 计算机学院25计算机学院2525例：例：(QR) (QQ)A1=Q (RQ) A A1 1A2= (Q (RQ) (QR) (QQ) A A2 2A3= (QR) (QQ) A2=A1A3计算机学院26计算机学院2626重要定律重要定律三段论：三段论：Q, QR R传递律：传递律：PQ,QRPR反证律反证律：如果如果, Q R, , Q R,则则 Q归谬律归谬律：如果如果, Q R, , Q R，则，则 Q计算机学院27计算机学院2727重要定理重要定理QQQQ QQ (QR)(QR) (P(QR) (Q(PR)Q(QR) R)(Q R)(PQ)(PR)(P Q)(QR)(PR)(QR)( RQ)( QR)( RQ) Q(Q R)( QQ)(RQ)( QQ)Q 计算机学院28计算机学院2828例：例：QQ分析分析(QR) (QQ)R=(QQ)(Q(QQ) (QQ)(Q(QQ)(QQ)计算机学院29计算机学院2929QQA1=(Q (QQ)Q)(Q(QQ)(QQ) A A2 2A2=Q (QQ) Q) A1A1A3=(Q (QQ) (QQ) A1=A2A3A4=Q (QQ) A1A1A5=QQ A3=A4A5计算机学院30计算机学院3030三段论三段论Q, QR RA1= QR A1 A2= Q A2 A3= R A1=A2 A3 计算机学院31计算机学院3131传递律传递律PQ,QRPRA1=(QR) (P (QR) A1 A1A2=QR A2 A3=P (QR) A1=A2 A3 A4=(P (QR) (PQ) (PR) A2A2A5=(PQ) (PR) A4=A3 A5A6=(PQ) A6 A7=(PR) A5=A6A7计算机学院32计算机学院3232QQA1=Q (QQ) A1A1A2= (QQ) ( QQ) A3A3A3=( QQ) (QQ) A3A3A4= Q (QQ) A1, A2, A3 A4A5=(Q (QQ) (Q Q) (Q Q) A2A2A6=(Q Q) (Q Q) A5=A4 A6 A7=(Q Q) Q QA8=Q Q A6=A7 A8 计算机学院33计算机学院3333 Q QA1= (Q Q)(QQ) A3 A3A2= (Q Q) QQA3= (QQ) (QQ ) A3 A3A4= QQ A3=A2 A4 计算机学院34计算机学院3434 (Q(QR)R)( (Q QR) R) A A1 1= R= RR R Q QQ QA A2 2=(R=(RR)R)( (Q Q(R(RR) R) A A 1 1A A3 3= =Q Q(R(RR) AR) A2 2=A=A1 1 A A3 3A A4 4=(=(Q Q(R(RR)R)( ( (Q QR)R)( (Q QR)R) ) A A 2 2A A5 5= (= (Q QR)R)( (Q QR) AR) A4 4=A=A3 3 A A5 5A A6 6= = Q Q Q Q Q QQ QA A7 7=(=(Q Q Q)Q)(Q(QR)R)( (Q Q R) R) (P(P Q)Q)(Q (Q R)R)(P (P R)R)A A8 8=(Q=(QR)R)( (Q Q R) AR) A7 7=A=A6 6 A A8 8A A9 9=(Q=(QR)R)( (Q QR) AR) A8 8, A, A5 5A A9 9计算机学院35计算机学院3535 (P(QR)(Q(PR)A A1 1=(P =(P (Q (Q R) R) ( P ( P Q)Q)(P (P R) R) A A 2 2A A2 2= = ( P ( P Q)Q)(P (P R)R)(Q(Q( P ( P Q)Q)(P (P R) R) A A 1 1A A3 3=(=(Q Q( P ( P Q)Q)(P (P R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R) R) A A 2 2A A4 4= (P = (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R) AR) A1 1, , A A2 2, , A A3 3 A A4 4A A5 5= =(P (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) (Q(Q(P (P R)R) ( (P ( (P (Q (Q R) R) ( Q( Q( P ( P Q)Q) (P (P (Q (Q R) R) (Q (Q (P (P R) R) A A 2 2A A6 6= =(P (P (Q (Q R)R)(Q(Q(P(PQ)Q)(P(P(Q (Q R)R)(Q(Q(P(PR) AR) A5 5=A=A4 4 A A6 6A A7 7= Q= Q(P(PQ) Q) A A 1 1A A8 8= (Q= (Q( P ( P Q) Q) ( (P ( (P (Q (Q R) R) ( Q( Q( P ( P Q) Q) A A 1 1A A9 9= (P = (P (Q (Q R) R) ( Q( Q( P ( P Q) AQ) A8 8=A=A7 7 A A9 9A A1010=(P =(P (Q (Q R) R) (Q (Q (P (P R) AR) A6 6=A=A9 9 A A1010计算机学院36计算机学院3636Q(QR) R)A A1 1=(Q=(QR)R)(Q(QR) R) Q QQ QA A2 2=(Q=(QR)R)(Q(QR)R)( (Q Q( (Q QR R) )R) R) (P (P(Q(QR)R)(Q(Q(P(PR)R)A A3 3= Q= Q(Q(QR)R)R) R) A A2 2= =A A1 1 A A3 3计算机学院37计算机学院3737(Q R)(P Q) (PR)A1= (Q R) (P (Q R) A1 A1A2= (P(Q R) (P Q) (P R) A2 A2A3= (Q R)(P Q)(P R) A1, A2 A3计算机学院38计算机学院3838(PQ)(QR)(PR)A1=(Q R) (P Q) (P R) (Q R)(P Q) (PR)A2=(Q R) (P Q) (P R) (P Q)(Q R) (P R) (P(QR) (Q(PR)A3=(P Q)(QR)(PR) A A2 2= =A A1 1 A A3 3计算机学院39计算机学院3939(QR) ( R Q)A1 1= (QR)(QR) (Q(QR)R)( (Q QR) R) A2 2= ( Q R) ( R Q) A3A3A3 3= (QR)( Q R) A A2 2= =A A1 1 A A3 3 计算机学院40计算机学院4040( Q R )( RQ)A1 1= ( QR)( RQ) (QR) ( R Q)A2 2= QQ QQA3 3= (Q Q)( RQ)( RQ) (Q R)(P Q) (PR) A4 4= ( RQ)( RQ) A A3 3= =A A2 2 A A4 4A5 5= ( QR) ( RQ) A1, A4 A5计算机学院41计算机学院4141 Q(Q R)(涵义涵义)A1= Q(RQ) A1A1A2= ( RQ) (QR) A3A3A3= Q(QR) A1， A2 A3 计算机学院42计算机学院4242( ( Q QQ)Q)(R(RQ)Q)A A1 1= = Q Q( (R RQ) Q) A1A1A A2 2=(=(R RQ)Q)(Q(QR R) ) A3A3A A3 3= = Q Q (Q(QR R) ) A A1 1, A, A2 2A A3 3A A4 4=(=( Q Q(Q(QR)R) ( ( Q QQ)Q)( ( Q QR) R) A2A2A A5 5=( =( Q Q Q) Q) ( ( Q Q R) AR) A4 4=A=A3 3 A A5 5A A6 6= (= ( Q Q R) R) (R(RQ) Q) A 3A 3A A7 7=(=( Q QQ)Q)(R(RQ) AQ) A5 5, A, A6 6A A7 7计算机学院43计算机学院4343( ( Q QQ)Q)Q Q A A1 1=(=( Q QQ)Q)( ( Q QQ)Q)Q) Q) ( ( Q QQ)Q)(R(RQ)Q)A A2 2=(=( Q QQ)Q)( ( Q QQ)Q)Q)Q) ( Q QQ)Q)( ( Q QQ) Q) ( ( Q QQ)Q)Q) Q) A2A2A A3 3=(=( Q QQ)Q)( ( Q QQ)Q)( ( Q QQ)Q)Q) AQ) A2 2=A=A1 1 A A3 3A A4 4= (= ( Q QQ)Q) ( ( Q QQ) Q) A 1A 1A A5 5=(=( Q QQ)Q)Q AQ A3 3=A=A4 4 A A5 5计算机学院44计算机学院4444QRQA1= Q(RQ) A1A1 A2= QRQ QR=(QR)计算机学院45计算机学院4545 QR RQA1 1= =(Q Q)A2 2= =( Q R) (Q R)A3 3= = =(RQ) ( Q R) A4 4= =(RQ) (Q R)A5 5= = (QR) (RQ)A6 6= = QR RQ计算机学院46计算机学院4646 QR QA1 1= = Q (R Q)A2 2= = Q (Q R)A3 3= = (Q R) Q A4 4= = Q QA5 5= = (Q R) QA6 6= = QR Q QR RA1 1= = QR RQA2 2= = RQ RA3 3= = QR R计算机学院47计算机学院4747例：若例：若R，则则QR。A1=C1Ak-1=Ck-1Ak=R RAk+1= R (QR) A1Ak+2= QR Ak+1=Ak Ak+2 QR计算机学院48计算机学院4848例：若例：若 PQ ， P (QR) ，则则 PR。A1=D1Am-1=Dm-1Am= PQ PQ Am+1=Dm+1Am+n-1=Dm+n-1Am+n= P (QR) P (QR) Am+n+1=(P(QR) ) (PQ) (PR) A A2 2Am+n+2=(PQ) (PR) Am+n+1=Am+nAm+n+2Am+n+3=PR Am+n+2=AmAm+n+3计算机学院49计算机学院4949演绎定理演绎定理Q R 当且当且 仅当仅当 QR归纳基础：归纳基础：用关于用关于Q到到R的推演长度的推演长度n作归纳证明。作归纳证明。当当n=1时，时，R或为公理，或属于或为公理，或属于 ，或，或R是是Q。若若R是公理，则是公理，则A1=RA2= R(QR)A3= (QR)所以所以 QR，从而从而 QR若若 R ，则，则A1=RA2= R(QR)A3= (QR)有有 QR若若R=Q，则，则 Q Q所以所以 QQ计算机学院50计算机学院5050演绎定理演绎定理(2)(2)归纳假设：归纳假设：假设假设Q到到R的推演长度小于的推演长度小于n定理成立。定理成立。归纳证明：当归纳证明：当Q到到R的推演长度等于的推演长度等于n时，有时，有Q RA1=Q1A2=Q2Ai= PRAj=PAn=R从从的推演的推演A1=D1Am= QPAk= Q (PR) Ak+1= Q (PR) (QP) (Q R)Ak+2= (QP)(Q R)Ak+3= (Q R)因为因为i,jn,有所以有所以Q P QPQ PR Q (PR)计算机学院51计算机学院5151演绎定理演绎定理(3)(3) 到到QR 的推演的推演由由 QR可知，有推理序列可知，有推理序列A1, A2, Am， 使得使得Am= QR 。证明有证明有Q R 。因为。因为有推理序列有推理序列A1, A2, Am，其中，其中Am= QRAm+1= QAm+2= R计算机学院52计算机学院5252 (Q(QR) (QR)根据演绎规则根据演绎规则(Q (Q R) Q R(Q (Q R) ,Q RA1= Q (Q R)A2= QA3= Q RA4=R计算机学院53计算机学院5353 (P(QR) (Q(PR)根据演绎规则根据演绎规则P (Q R) Q (P R)P (Q R) ,Q P RP (Q R) ,Q, P RA1= P(Q R) A2= PA3= Q RA4=QA5=R计算机学院54计算机学院5454P,QP QP,Q, (P Q)Q， P,Q, (P Q) Q A1 1= PA2 2= Q A3 3= (P Q)A4 4= (P Q) (P Q) A5 5= P QA6 6= Q所以有所以有P,Q (P Q)，即，即P,Q P Q计算机学院55计算机学院5555再看传递律再看传递律PQ,QRPR(Q R) (P Q) (P R)(P Q) (Q R) (P R)计算机学院56计算机学院5656 (PQ) (PR) (PQ R)演绎定理：演绎定理：(PQ) (PR) ，P Q RA1 1= ( PQ) (PR)A2 2= PA3 3= ( PQ) (PR) ( PQ) A4 4= PQA5 5= QA6 6= ( PQ) (PR) ( PR)A7 7= PRA9 9= RA1010= Q R计算机学院57计算机学院5757反证律反证律如果如果, Q R, , Q R,则 QA1 1= = Q RA2 2= = Q RA3 3= (= ( QR)(R Q )A4 4= = RQ A5 5= = QQA6 6= = (Q Q)QA7 7= = Q 计算机学院58计算机学院5858归谬律归谬律如果如果, Q R, , Q R，则，则 QA1 1= = Q RA2 2= = Q RA3 3= = RQA4 4= = Q Q A5 5= = = QQA6 6= = = Q QA7 7= = ( Q Q) QA8 8= = Q 计算机学院59计算机学院5959可靠性可靠性可靠性定理：若可靠性定理：若 A ，则，则|= A。证明：设证明：设A A1 1,A,A2 2, ,A An n是是A A的从的从 的推演。归纳证明：对于的推演。归纳证明：对于 A Ai i ，有，有 |=|=A Ai i，i=1,2,i=1,2,n ,nn=1n=1时，若时，若Ai是公理，则是公理，则Ai是永真式。若是永真式。若Ai，则，则 Ai ，有，有 |=|=A Ai i公理模式公理模式A1v(Av(A (BA)v(A)(v(B)v(A)如果如果v(A)=1，则v(A)(v(B)v(A)=1。如果如果v(A)=0，则v(A)(v(B)v(A)=1。公理模式公理模式A2(A(A (BR) (AB) (AR)同理同理v(Av(A (BR) (AB) (AR)=1)=1公理模式公理模式A3( (A B) (BA)同理同理v(v(A B) (BA)=1)=1计算机学院60计算机学院6060可靠性定理可靠性定理若若Ai，则，则 Ai, , 对于对于v()=1， Ai有有v(Ai)=1，所以，所以 |= Ai假设假设inin时定理成立时定理成立证明证明i=ni=n时，时，设设Ai由由Aj, , Ak用用MPMP规则推出，其中规则推出，其中j,kij,ki， Ak为为AjAi。由归纳假设知，由归纳假设知， Aj且且 AjAi ， 所以所以|=Aj， |=AjAi |=Ai 。因此因此|=An 即即|= A。计算机学院61计算机学院6161协调协调定义定义3.3 3.3 如果对于每个公式如果对于每个公式A A， A A，则，则 称不协调，否称不协调，否则称则称 协调。协调。计算机学院62计算机学院6262定理定理3.3 3.3 若若 Q Q Q Q ，则，则 不协调。不协调。证明：证明： Q Q Q Q即为公式即为公式 (Q QQ Q)A A1 1= = (Q QQ Q)A A2 2= = (Q QQ Q) (R (Q QQ Q) )A A3 3= =R (Q QQ Q) A A4 4= (= (R (Q QQ Q) (Q QQ Q) R )A A5 5= = (Q QQ Q) R A A6 6= = (Q QQ Q) A A7 7= = R R计算机学院63计算机学院6363定理定理3.4 3.4 若若 协调，则协调，则 可满足。可满足。计算机学院64计算机学院6464完备性定理完备性定理完备性定理：若完备性定理：若|= Q |= Q ，则，则 Q Q。证明：证明：若真值赋值若真值赋值v v满足满足 ，则它必满足，则它必满足Q ,Q ,即不可满足即不可满足 Q Q，所以所以 Q Q 不可满足。不可满足。因此，因此， Q Q 不协调。不协调。所以有所以有 Q QQ Q。有演绎定理有有演绎定理有 Q QQ Q。由由( ( Q QQ)Q)Q Q，因此，因此，QQ计算机学院65计算机学院6565主要内容主要内容概述概述命题逻辑公理系统命题逻辑公理系统谓词逻辑公理系统谓词逻辑公理系统总结总结计算机学院66计算机学院6666谓词逻辑的公理系统谓词逻辑的公理系统定义定义3.4 3.4 谓词逻辑的公理系统定义如下：谓词逻辑的公理系统定义如下：(1) (1) 符号：符号：个体变元个体变元x x1 1,x ,x2 2 , , 个体常元个体常元a a1 1,a ,a2 2 , , 对每个正整数对每个正整数n n，n n元函数符号元函数符号f f1 1,f ,f2 2 , , 对每个正整数对每个正整数m m，m m元谓词符号元谓词符号P P1 1,P ,P2 2 , , 联结词符号联结词符号 ，量词符号量词符号逗号，逗号，括号括号(,)(,)计算机学院67计算机学院6767(2) (2) 项定义如下：项定义如下：个体常元是项；个体常元是项；个体变元是项；个体变元是项；若是若是t t1 1,t,tn n项，则是项，则是f fi i(t (t1 1,t,tn n) )项。项。(3) (3) 公式定义如下：公式定义如下：若是若是t t1 1,t,tn n项，则项，则P Pi i(t (t1 1,t,tn n) )是公式。是公式。若若A A是公式，则（是公式，则（A A）是公式；）是公式；若若A,BA,B是公式，则（是公式，则（A AB B）是公式；）是公式；若若A A是公式，则（是公式，则（xA A）是公式。）是公式。计算机学院68计算机学院6868公理公理公理模式公理模式A A1 1A A (BA)公理模式公理模式A A2 2(A(A (BR) (AB) (AR)公理模式公理模式A A3( (A B) (BA)公理模式公理模式A A4 4xAAtx 其中项其中项t t对于对于A A中的中的x x可代入可代入 公理模式公理模式A A5 5x( ( AB) (A xB)其中其中x不是不是A A中自由变元中自由变元 公理模式公理模式A A4 4说明说明如果公式如果公式A A对于一对于一切切x x成立，则公式成立，则公式A A对于任意对于任意t t成立。成立。但是，但是， t t不是约束不是约束变元变元在自然数论域在自然数论域xy(xy) y(yy)计算机学院69计算机学院69695) 5) 推理规则：推理规则：分离规则（简称分离规则（简称MPMP规则）：规则）：从从A A和和A AB B推出推出B B。概括规则（简称概括规则（简称UGUG规则）：规则）：从从A A推出（推出（x A A）。）。概括规则说明概括规则说明x x是自由出现是自由出现x不是常元不是常元x不是选择变元不是选择变元计算机学院70计算机学院7070缩写公式缩写公式AB=(AB)AB= (AB)AB=(AB) (BA)AB= (AB)xA(x)=xA(x)计算机学院71计算机学院7171公式复杂度公式复杂度公式公式A的复杂度表示为的复杂度表示为FC(A)命题变元复杂度为命题变元复杂度为0 0，如果，如果P P是谓词变元，则是谓词变元，则FC (P)=0FC (P)=0。如果公式如果公式A=A= B B，则，则FC (A)=FC(B)+1FC (A)=FC(B)+1。如果公式如果公式A=B1A=B1B2B2，则，则FC (A)=maxFC(B1), FC(B2)+1FC (A)=maxFC(B1), FC(B2)+1。如果公式如果公式A= A= x B B，则，则FC (A)= FC(B)+1FC (A)= FC(B)+1。计算机学院72计算机学院7272推演推演( (演绎演绎) )定义定义3.5 3.5 设设 是公式集。如果公式序列是公式集。如果公式序列A A1 1,A,A2 2,A,An n中的每中的每个公式个公式A Ai i满足以下条件之一，则称它为满足以下条件之一，则称它为A An n的从的从 的一个的一个推演推演( (演绎演绎) )。其中。其中 称为推演的称为推演的前提集前提集，称，称A An n为为结论结论，记为记为 A An n。(1) (1) A Ai i是公理；是公理；(2) (2) A Ai i ；(3) (3) 有有j,ki,Aj,ki,Ak k= =A Aj jA Ai i由由A Ak k, ,A Aj j用用MPMP规则推出。规则推出。(4) (4) 有有ji,ji,使使A Ai i= = x xA Aj j由用由用UGUG规则推出。规则推出。推理序列推理序列A A1 1,A,A2 2,A,An n是是推理序列推理序列, ,推理序列长度推理序列长度n n。推论：推论：如果如果A Ai i是公理或是公理或A Ai i ，则则 A Ai i(4)(4)说明说明X X是自由出现是自由出现x不是常元不是常元x不是选择变元不是选择变元计算机学院73计算机学院7373x(P(x)P(x)A1 1= = P(x) P(x)A2 2= = P(x)P(x)A3 3= = x(P(x)P(x)计算机学院74计算机学院7474 xP(x) xP(x)A1 1= xP(x) P(y)A2 2=(xP(x) P(y) (P(y) xP(x) )A3 3= P(y) xP(x)A4 4= P(y) P(y) A5 5= P(y) xP(x)A6 6= xP(x) P(y)A7 7= xP(x) xP(x)计算机学院75计算机学院7575主要性质主要性质xR(x) y R(y)xR(x) y R(y)xR(x) xR(x) xy R(x,y) yxR(x,y)xy R(x,y) yxR(x,y) xyR(x,y) yx R(x,y) xyR(x,y) xR(x,x)xR(x,x) xyR(x,y) x(P(x) Q(x) (xP(x) x Q(x) x(P(x) Q(x) (xP(x) x Q(x)x(P(x) Q(x) (xP(x) xQ(x) x(P(x) Q(x) (xP(x) xQ(x)x(P(x) Q(x) (xP(x) xQ(x) xP(x) xQ(x)x(P(x) Q(x) 计算机学院76计算机学院7676演绎定理演绎定理 A A B B 当且仅当当且仅当 A AB B因为因为A AxA不是有效公式，不是有效公式，A A 可证，可证， xA可证？变元变元约束变元约束变元自由变元自由变元出现出现约束出现约束出现自由出现自由出现计算机学院77计算机学院7777演绎定理演绎定理 A A B B，且且A A为闭公式为闭公式， 当且仅当当且仅当 A AB B归纳基础：归纳基础：用关于用关于 A A 到到B B的推演长度的推演长度n n作归纳证明。作归纳证明。当当n=1n=1时，时，B B或为公理，或属于或为公理，或属于 ，或，或B B是是A A。若若B B是公理，则是公理，则A A1 1=B=BA A2 2= B= B(AB)A A3 3= = (AB)所以所以 AB，从而从而 A AB B若若 B B ，则，则 若若B=AB=A，则，则 A A A AA A1 1=B =B 所以所以 A AA AA A2 2= B= B(AB)A A3 3= = (AB)有有 A AB B计算机学院78计算机学院7878演绎定理演绎定理(2)(2)归纳假设：归纳假设：假设假设 A A 到到B B的推演长度小于的推演长度小于n n定理成立。定理成立。归纳证明：当归纳证明：当 A A 到到B B的推演长度等于的推演长度等于n n时，并且时，并且B B由分离规由分离规则推出有则推出有 A A B BA A1 1=B=B1 1A A2 2=B=B2 2A An n=B=BA Ai i= = R R A Aj j= = R R B B从从 的推演的推演A A1 1=D=D1 1A Am m= A= AR RA Ak k= A= A (R (RB B) ) A Ak+1k+1=(=(A A (R (R B B) ) (A A R R) ) (A (A B B) )A Ak+2k+2= =(A A R R) ) (A (A B B) )A Ak+3k+3=A =A B B因为因为i,jn,i,jn,所以所以 A A R R A AR R A A R RB B A A (R (RB B) )计算机学院79计算机学院7979演绎定理演绎定理(3)(3)归纳证明：当归纳证明：当 A A 到到B B的推演长度等于的推演长度等于n n时，并且时，并且B B由综合规则推出，所以由综合规则推出，所以从从 的推演的推演A A1 1= =B B1 1. . A Am m= = A A R R A Am+1m+1= =x(A A R R )A Am+2m+2= = A A xRA A为闭公式为闭公式A BA1=B1A2=B2An-1= R An= xRAn=B因为因为 A RA R推演推演长度等于长度等于n-1n-1，所以，所以 A AR R计算机学院80计算机学院8080演绎定理演绎定理(4)(4) 到到A AB B 的推演的推演由由 A AB B可知，有推理序列可知，有推理序列A A1 1, A, A2 2, A, Am m，使得，使得A Am m= = A AB B 。证明有证明有 A A B B 。因为。因为有推理序列有推理序列A A1 1, A, A2 2, A, Am m，其中，其中A Am m= = A AB BA Am+1m+1= = A AA Am+2m+2= = B B计算机学院81计算机学院8181 x(P(x) Q(x) (xP(x) xQ(x) ) x(P(x) Q(x)，xP(x) xQ(x) A1 1= = x(P(x) Q(x)A2 2= = x(P(x) Q(x) (P(c) Q(c)A3 3= = P(c) Q(c)A4 4= = xP(x)A5 5= = xP(x) P(c)A6 6= = P(c)A7 7= = Q(c)A8 8= =Q(c) xQ(x)A9 9= = xQ(x)计算机学院82计算机学院8282可靠性定理可靠性定理(1 )(1 )公理公理1-31-3可靠性定理：若可靠性定理：若 A A ，则，则 |= |= A A。证明：设证明：设A A1 1,A,A2 2,A,An n是是A A的从的从 的推演。归纳证明：对于的推演。归纳证明：对于 A Ai i ，有，有 |=|=A Ai i，i=1,2,ni=1,2,n若若n=1n=1时，即时，即A Ai i是公理，则是公理，则A Ai i是永真式。是永真式。公理模式公理模式A A1 1v(Av(A (BA)v(A)(v(B)v(A)如果如果v(A)=1，则v(A)(v(B)v(A)=1。如果如果v(A)=0，则v(A)(v(B)v(A)=1。公理模式公理模式A A2 2(A(A (BR) (AB) (AR)同理同理v(Av(A (BR) (AB) (AR)=1)=1公理模式公理模式A A3 3( (A B) (BA)同理同理v(v(A B) (BA)=1)=1计算机学院83计算机学院8383可靠性定理可靠性定理(2 )(2 )公理公理4 4设设A Ai i 是公理是公理A A4 4 xA AA At tx x 。任取解释任取解释I I和赋值和赋值v v，若若I( I(xA)(v)=0A)(v)=0，则，则I( I(xA AA At tx x )(v)=1)(v)=1若若I( I(xA)(v)=1A)(v)=1，则对于每个，则对于每个d dD，I(A)(vx/d)=1I(A)(vx/d)=1所以所以 I(AI(At tx x)(v)= I(A)(vx/I(t)(v)=1)(v)= I(A)(vx/I(t)(v)=1，这表明这表明A Ai i 是永真式，即是永真式，即 |= |= A Ai i。计算机学院84计算机学院8484可靠性定理可靠性定理(3)(3)公理公理5 5设设A Ai i 是公理是公理A A5 5 x( A( AB) (A AxB)。其中其中x x不是公式不是公式A A的自由变元。的自由变元。若若I( I(x( A( AB) )(v)=0)(v)=0， 则则I( I(x( A( AB) (A A xB)(v)=1)(v)=1若若( (x( A( AB) )(v)=1)(v)=1，且，且I(A)(v)=0I(A)(v)=0， 则则I(AI(AxB)(v)=1)(v)=1， 所以所以I( I(x( A( AB) (A A xB)(v)=1)(v)=1若若( (x( A( AB) )(v)=1)(v)=1，且，且I(A)(v)=1I(A)(v)=1， 则对于任意则对于任意d dD， I( I(x( A( AB) )(vx/d)=1)(vx/d)=1。 因为因为I(A)(v)=1I(A)(v)=1，所以，所以 I(B)(vx/d)=1I(B)(vx/d)=1。从而。从而I( I(xB)(v)=1)(v)=1， 即即I( I(A AxB)(v)=1)(v)=1， 因此有因此有I( I(x( A( AB) (A AxB)(v)=1)(v)=1计算机学院85计算机学院8585可靠性定理可靠性定理(4)(4)MPMP规则规则若若A Ai i ，则，则 A Ai i, , 对于对于v( v( )=1)=1， A Ai i 有有v( v(A Ai i)=1)=1，所以，所以 |=|= A Ai i假设假设inin时定理成立时定理成立证明证明i=ni=n时，时，设设A Ai i由由A Aj j, , A Ak k用用MPMP规则推出，规则推出， 其中其中j,kij,ki，A Ak k为为A Aj jA Ai i。由归纳假设知，由归纳假设知， A Aj j且且 A Aj jA Ai i ， 所以所以 |=|=A Aj j， |=|=A Aj jA Ai i |=A|=Ai i 。因此因此 | |=A=A即即 | |= = A A计算机学院86计算机学院8686可靠性定理可靠性定理(5 )(5 )UGUG规则规则证明证明i=ni=n时，时，设设A Ai i由由A Ak k用用UGUG规则推出，其中规则推出，其中kiki， A Ai i= =xA Ak k由归纳假设知，由归纳假设知， A Ak k， 所以所以 |=|=A Ak k。因为因为A Ai i= =xA Ak k ，对于任意对于任意d dD，I( I(A Ak k)(vx/d)=1)(vx/d)=1， 所以，所以， I( I(xA Ak k )(vx/d)=1)(vx/d)=1因此因此 |=A|=An n 即即 |=|= A A。计算机学院87计算机学院8787协调协调定义定义3.6 3.6 如果对于每个公式如果对于每个公式A A， A A，则，则 称不协调，否称不协调，否则称则称 协调。协调。定理定理3.123.12若若 p p( (x x) ) p p( (x x) ) ，则，则 不协调。不协调。定理定理3.13 3.13 若若 协调，则协调，则 可满足。可满足。计算机学院88计算机学院8888完备性定理完备性定理命题命题若若 A A，则，则 A A证明：证明： 若真值赋值若真值赋值v v满足满足 A A， 则则v( v(A A)=1)=1且且v( v(A A)=1)=1，出现矛盾，出现矛盾 因此，因此， A A 不可满足不可满足 所以所以 A A不协调不协调，即即 A AA A A A A A 又因为又因为 ( (A A A A) ) A A 所以所以 A A推论：推论：若若 A A，则，则A A计算机学院89计算机学院8989完备性定理完备性定理谓词谓词若若 A A，则，则 A A证明证明 设设B B是是A A的闭包。的闭包。 若解释若解释I I满足满足 ，必然满足，必然满足B B，即不满足，即不满足 B B， 所以所以 B B 不可满足，不可满足， B B 不协调，不协调， B B B B 。 由演绎定理知，由演绎定理知， B B B B， 因为因为 ( ( B B B B) ) B B ，故，故 B B ， 因此，因此， A A。计算机学院90计算机学院9090带等词的一阶公理系统带等词的一阶公理系统 t t= =t t(t (t1111= =t t21 21 ) ) t t1n1n= =t t2n2nf( f(t t1111,t,t1n1n) )= =f( f(t t2121,t t2n2n) )t t1111= =t t2121 t t1n1n= =t t2n2nR(R(t t1111,t,t1n1n) )= =R(R(t t2121,t t2n2n) )可靠性定理可靠性定理若若 P P ，则，则|= P|= P完备性定理完备性定理若若 A A，则，则 A A计算机学院91计算机学院9191皮亚诺皮亚诺专用公理专用公理（不完全性与完全性）（不完全性与完全性）语言语言L =,+L =, 0，其中，其中+, +, 是二元运算符，是二元运算符，s s是一是一元函数符（后继运算符），元函数符（后继运算符），0 0为常元。为常元。理论（逻辑公理理论（逻辑公理+ +专用公理）专用公理） x x( (s s( (x x) ) x x) ) x x y y ( (x x y ys s( (x x) ) s s( (y y) ) x x( (x x+0=+0=x x) ) x x y y( (x x+ +s s( (y y)=)=s s( (x x+ +y y) ) x x( (x x 0=0)0=0) x x y y( (x x s s( (y y)=)=x x y y+x)+x)(p(0)(p(0)x x( (p p( (x x) )p p( (s s( (x x)xpxp( (x x) ) 其中其中p p( (x x) )是任意公式。是任意公式。计算机学院92计算机学院罗丹罗丹- -思想者思想者92计算机学院93计算机学院部分资料从网络收集整理而来，供大家参考，感谢您的关注！