公理系统（推荐阅读）

第一篇：公理系统

公理化方法

所谓公理化方法，就是指从尽可能少的原始概念和不加证明的原始命题（即公理、公设）出发，按照逻辑规则推导出其他命题，建立起一个演绎系统的方法。

1简介

恩格斯曾说过：数学上的所谓公理，是数学需要用作自己出发点的少数思想上的规定。

公理化方法能系统的总结数学知识、清楚地揭示数学的理论基础，有利于比较各个数学分支的本质异同，促进新数学理论的建立和发展。现代科学发展的基本特点之一，就是科学理论的数学化，而公理化是科学理论成熟和数学化的一个主要特征。

公理化方法不仅在现代数学和数理逻辑中广泛应用，而且已经远远超出数学的范围，渗透到其它自然科学领域甚至某些社会科学部门，并在其中起着重要作用．

2历史发展

产生

公理化方法发展的第一阶段是由亚里士多德的完全三段论到欧几里得《几何原本》的问世．大约在公元前3世纪，希腊哲学家和逻辑学家亚里斯多德总结了几何学与逻辑学的丰富资料，系统地研究了三段论，以数学及其它演绎的学科为例，把完全三段论作为公理，由此推导出其它所有三段论法，从而使整个三段论体系成为一个公理系统．因此，亚里斯多德在历史上提出了第一个成文的公理系统． 亚里斯多德的思想方法深深地影响了当时的希腊数学家欧几里得．欧几里得把形式逻辑的公理演绎方法应用于几何学，从而完成了数学史上的重要著作《几何原本》．他从古代的量地术和关于几何形体的原始直观中，用抽象分析方法提炼出一系列基本概念和公理．他总结概括出14个基本命题，其中有5个公设和9条公理，然后由此出发，运用演绎方法将当时所知的全部几何学知识推演出来，整理成为演绎体系．《几何原本》一书把亚里斯多德初步总结出来的公理化方法应用于数学，整理、总结和发展了希腊古典时期的大量数学知识，在数学发展史上树立了一座不朽的丰碑．

公理学研究的对象、性质和关系称为“论域”，这些对象、性质和关系，由初始概念表示．例如欧氏《几何原本》中只需取“点”、“直线”、“平面”；“在„„之上”、“在„„之间”、“叠合”作为初始概念．前三个概念所表示的三类对象和后三个概念所表示的三种关系就是这种几何的论域．按照“一个公理系统只有一个论域”的观点建立起来的公理学，称为实质公理学．这种公理学是对经验知识的系统整理，公理一般具有自明性．因此，欧氏《几何原本》就是实质公理学的典范． 发展

公理化方法的发展大致经历了这样三个阶段：实质（或实体）公理化阶段、形式公理化阶段和纯形式公理化阶段，用它们建构起来的理论体系典范分别是《几何原本》、《几何基础》和ZFC公理系统。《几何原本》虽然开创了数学公理化方法的先河，然而它的公理系统还有许多不够完善的地方，其主要表现在以下几个方面：(1)有些定义使用了一些还未确定涵义的概念；(2)有些定义是多余的；(3)有些定理的证明过程往往依赖于图形的直观；(4)有的公理(即平行公理)是否可用其它公理来证明或代替．这些问题成为后来许多数学家研究的课题，并通过这些问题的研究，使公理化方法不断完善，并促进了数学科学的发展．

第五公设(即平行公设)内容复杂，陈述累赘，缺乏象其它公设和公理那样的说服力，并不自明．因此，它能否正确地反映空间形式的性质，引起了古代学者们的怀疑．从古希腊时代到公元18世纪，人们通过不同的途径和方法对这一问题进行了大量的研究工作，其中萨克里(Saccheri，1667—1733)和兰勃特(Lambert，1728-1777)等人考虑了两个可能的与平行公设相反的假设，试图证明出平行公设，但是他们的努力均归于失败．然而，在这些失败中却引出了一串与第五公设相等价的新命题和定理，即非欧几何的公理和定理，它预示了一种新的几何体系可能产生．

19世纪年轻的俄国数学家罗巴切夫斯基(Лобачевский1792-1856)产生了与前人完全不同的信念：首先，他认为第五公设不能以其余的公理作为定理来证明；其次，除掉第五公设成立的欧氏几何之外，还可能有第五公设不成立的新几何系统存在．于是，他在剔除第五公设而保留欧氏几何其余公理的前提下，引进与第五公设相反的公理，从而构造了一个全新的几何系统，它与欧氏几何系统相并列．后来人们又证明了这两个部分地相矛盾的几何系统竟是相对相容的，即假定其中之一无矛盾，则另一个必定无矛盾，这样以来，只要这两个系统是无矛盾的，第五公设与欧氏系统的其余公理就必定独立无关．现在人们就用罗巴切夫斯基的名字命名了这一新的几何学，并把一切不同于欧氏几何公理系统的几何系统统称为非欧几何．

非欧几何的建立在数学史上具有划时代的意义，标志着人们对空间形式的认识发生了飞跃，从直观空间上升到抽象空间．在建立非欧几何的过程中，公理化方法得到了进一步的发展和完善．

形式化

德国数学家帕斯(Moritz Pasch，1843-1930)通过对射影几何公理化基础的纯逻辑的探讨，第一次从理论上提出了形式公理学的思想．他认为，几何学如果要成为一门真正的演绎科学，最根本的是推导的进行必须完全独立于几何概念的涵义，同样地也必须不以图形为依据，而所考虑的只能是被命题或定义所确定的几何概念之间的关系．就是说，一个公理系统必然要有本系统里不定义的概念，通过这些概念就可以给其它概念下定义，而不定义概念的全部特征必须由公理表达出来．公理可以说是不定义概念的隐定义．有些公理虽然是由经验提出来的，但当选出一组公理之后，必须不再涉及经验及物理意义．公理决不是自明的真理，而是用以产生任一特殊几何的假定．帕斯的这些思想已经表达了形式公理系统的特征．

随着数学的深入研究和射影几何公理系统的建立，形式公理学的概念已经成熟．1899年希尔伯特《几何学基础》一书的发表，不仅给出了欧氏几何的一个形式公理系统，而且解决了公理化方法的一系列逻辑理论问题．这本著作成为形式公理学的奠基著作．

希尔伯特几何公理系统，除了有几何模型外，还可以有其它模型(如算术模型)，所以它是一个形式公理系统，可以把其初始概念和公理看成是没有数学内容的，数学内容是通过解释赋予它们的，初始概念和公理完全可以用形式语言来陈述．因此，自从《几何学基础》问世以后，不仅公理化方法进入了数学的其它各个分支，而且也把公理化方法本身推向了形式化的阶段．

3作用意义

分析、总结数学知识

当一门科学积累了相当丰富的经验知识，需要按照逻辑顺序加以综合整理，使之条理化、系统化，上升到理性认识的时候，公理化方法便是一种有效的手段．如近代数学中的群论，便经历了一个公理化的过程．当人们分别研究了许多具体的群结构以后，发现了它们具有基本的共同属性，就用一个满足一定条件的公理集合来定义群，形成一个群的公理系统，并在这个系统上展开群的理论，推导出一系列定理．

数学研究的基本方法

不但对建立科学理论体系，训练人的逻辑推理能力，系统地传授科学知识，以及推广科学理论的应用等方面起到有益的作用，而且对于进一步发展科学理论也有独特的作用．例如在代数方面，由于公理化方法的应用，在群论、域论、理想论等理论部门形成了一系列新的概念，建立了一系列新的联系并导致了一系列深远的结果；在几何方面，由于对平行公设的研究导致了非欧几何的创立．因此，公理化方法也是在理论上探索事物发展规律，作出新的发现和预见的一种重要方法．

科学研究的对象

介乎于逻辑学和数学之间的边缘学科—— 数理逻辑，用数学方法研究思维过程中的逻辑规律，也系统地研究数学中的逻辑方法．因此，数学中的公理方法是数理逻辑所研究的一个重要内容．由于数理逻辑是用数学方法研究推理过程的，它对公理化方法进行研究，一方面使公理化方法向着更加形式化和精确化的方向发展，一方面把人的某些思维形式，特别是逻辑推理形式加以公理化，符号化．这种研究使数学工作者增进了使用逻辑方法的自觉性． 示范作用

任何一门科学都不仅仅是搜集资料，也决不是一大堆事实及材料的简单积累，而都是有其自身的出发点和符合一定规则的逻辑体系．公理化方法对现代理论力学及各门自然科学理论的表述方法都起到了积极的借鉴作用．例如牛顿在他的《自然哲学的数学原理》巨著中，系统地运用公理化方法表述了经典力学理论体系；本世纪40年代波兰的巴拿赫完成了理论力学的公理化；爱因斯坦运用公理化方法创立了相对论理论体系．狭义相对论的出发点是两个基本假设：相对性原理和光速不变原理．爱因斯坦以此为前提，逻辑地演绎出四个推论：“尺缩效应”、“钟慢效应”、“质量增大效应”和“关系式”．这些就是爱因斯坦运用公理化方法，创立的狭义相对论完整理论体系的精髓．

4基本要求

公理是对诸基本概念相互关系的规定，这些规定必须是必要的而且是合理的．因此，一个严格完善的公理系统，对于公理的选取和设置，必须具备如下三个基本要求： 相容性

这一要求是指在一个公理系统中，不允许同时能证明某一定理及其否定理．反之，如果能从该公理系统中导出命题A和否命题非A(记作-A)，从A与-A并存就说明出现了矛盾，而矛盾的出现归根到底是由于公理系统本身存在着矛盾的认识，这是思维规律所不容许的．因此，公理系统的无矛盾性要求是一个基本要求，任何学科，理论体系都必须满足这个要求． 独立性

这一要求是指在一个公理系统中的每一条公理都独立存在，不允许有一条公理能用其它公理把它推导出来，同时使公理的数目减少到最低限度． 完备性

这就是要求确保从公理系统中能推出所研究的数学分支的全部命题，也就是说，必要的公理不能减少，否则这个数学分支的许多真实命题将得不到理论的证明或者造成一些命题的证明没有充足的理由．

从理论上讲，一个公理系统的上述三条要求是必要的，同时也是合理的．至于某个所讨论的公理系统是否满足或能否满足上述要求，甚至能否在理论上证明满足上述要求的公理系统确实存在等，则是另外一回事了．应该指出的是，对于一个较复杂的公理体系来说，要逐一验证这三条要求相当困难，甚至至今不能彻底实现．

5方法运用

1．要积累大量的经验、数据和资料，对这些经验资料进行分析归纳，使之系统化，最后上升为理论．因为公理系统的建立是以大量的事实为基础，以丰富的经验和已有的科学知识为前提的，设此无彼． 2．数学公理化的目的是要把一门数学整理成为一个演绎系统，而这一系统的出发点就是一组基本概念和公理．因此，要建立一门数学的演绎系统，就要在第一步的基础上，从原有的资料、数据和经验中选择一些基本概念和确定一组公理，然后由此来定义其它有关概念并证明有关命题．选取的基本概念是不定义概念，必须是无法用更原始、更简单的概念去确定其涵义的，也就是说，它是高度纯化的抽象，是最原始最简单的思想规定．

3．在确定了基本概念和公理之后，就要由此出发，经过演绎推理，将一门数学展开成一个严格的理论系统．也就是说，对系统中的每一概念予以定义，而每一个定义中引用的概念必须是基本概念或已定义过的概念；对其它每一命题都给予证明，而在证明中作为论据的命题必须是公理或者已经证明为真实的定理．因此，一门数学的演绎系统就是这门数学的基本概念、公理和定理所构成的逻辑的链条．

在上述过程中，从认识论的角度来看，任何公理系统的原始概念和公理的选取必须反映现实对象的本质和关系．就是说，应该有它真实的直观背景而不是凭空臆造．其次，从逻辑的角度看，则不能认为一些概念和公理的任意罗列就能构成一个合理的公理系统，而一个有意义的公理系统必须是一个逻辑相容的体系．

6公理证明编辑

公理系统一个公理系统的相容性是至关重要的，因为一个理论体系不能矛盾百出．而独立性和完备性的要求则是次要的．因为在一个理论体系中，如果有多余的公理，对于理论的展开没什么妨碍；如果独立的公理不够用，数学史上常常补充一些公理，逐步使之完备．下面仅就公理系统的相容性证明作一介绍．

产生背景

关于相容性征明这一概念的产生和历史发展的背景是这样的：自从罗巴切夫斯基几何诞生后，由于罗氏平行公理(过平面上一已知直线外的一点至少可以引两条直线与该已知直线平行)如此地为常识所不容，这才真正激起了人们对于数学系统的无矛盾性证明的兴趣和重视．后来，庞卡莱(Poincare`，1854-1912)在欧氏半平面上构造了罗氏几何的模型，把罗氏系统的相容性证明通过一个模型化归为欧氏系统的相容性证明，但却由此导致了人们对欧氏系统相容性的重重疑虑．幸亏那时已经有了解析几何，这就等于在实数系统中构造了一个欧氏几何的模型．这就把欧氏几何的无矛盾性归结到了实数论的相容性．那么实数论的相容性如何？戴德金(Dedekind，1831-1916)把实数定义为有理数的分划，也即有理数的无穷集合，因而把这个无矛盾性归结到了自然数系统的无矛盾性．又由于弗雷格(Frege，1848-1925)的自然数的概念是借助集合的概念加以定义的，因此，归来归去还是把矛盾集中到集合论那里去了．那么集合论的相容性如何？事实上，集合论的相容性正处于严重的“危机”之中，以致这种相容性的证明至今还未解决． 庞卡莱模型

庞卡莱为证明罗氏几何的相容性，在欧氏系统中构造了一个罗氏几何的模型．即在欧氏平面上划一条直线a将其分成上、下两个半平面，把不包括这条直线在内的上半平面作为罗氏平面，其上的欧氏点当作罗氏几何的点，把以该直线上任一点为中心，任一长为半径的半圆周作为罗氏几何的直线，然后对如此规定的罗氏几何元素一一验证罗氏平行公理是成立的．

如图4—3所示，过罗氏平面上任一罗氏直线l外的一点P，确实可以作出两条罗氏直线与l平行．因为欧氏直线a上的点不是罗氏几何系统的元素，所以两个半圆相交于直线a上某一点则应看作相交于无穷远点，从而在有穷范围内永不相交．

这样以来，如果罗氏系统在今后的展开中出现了正、反两个互相矛盾的命题的话，则只要按上述规定之几何元素间的对应关系进行翻译，立即成为互相矛盾的两个欧氏几何定理．从而欧氏系统就矛盾了．因此，只要承认欧氏系统是无矛盾的，那么罗氏系统一定也是相容的．这就把罗氏系统的相容性证明通过上述庞卡莱模型化归为欧氏系统的相容性证明．这种把一个公理系统的相容性证明化归为另一个看上去比较可靠的公理系统的相容性证明，或者说依靠一个数学系统的无矛盾性来保证另一个数学系统的协调性叫做数学系统的相对相容性证明．

对数学发展的影响

由于相对相容性的出现，使人们对欧氏系统的相容性也忧心重重．而更糟的是，在罗氏系统的展开中人们又发现，罗氏几何空间的极限球面上也可构造欧氏模型，即欧氏几何的全部公理能在罗氏的极限球上实现，于是欧氏几何的相容性又可由罗氏几何的相容性来保证！这说明欧氏与罗氏的公理系统虽然不同，但却是互为相容的．人们当然不满足于两者互相之间的相对相容性证明，因为看上去较为合理的欧氏系统的无矛盾性竟要由看上去很不合理的罗氏系统来保证，这是难以令人满意的．于是人们开始寻求直接的相容性证明，本世纪初数学基础论就诞生了．由于在这一工作中所持的基本观点不同，在数学基础论的研究中形成了诸如逻辑主义派、直觉主义派和形式公理学派三大流派．这些流派虽然并未最后解决相容性证明问题，但在方法论上却各有贡献，他们的方法论、思想方法对于数学的研究与发展都具有重要的意义，有些还值得进一步分析、探讨、继承和发展．

第二篇：armstrong公理系统证明

 Armstrong公理系统的证明

① A1自反律：若Y X U，则X→Y为F所蕴含

证明1

设Y X U。

对R的任一关系r中的任意两个元组t,s：

若t[X]=s[X]，由于Y X，则有t[Y]=s[Y]，所以X→Y成立，自反律得证。

② A2增广律：若X→Y为F所蕴含，且Z U，则XZ→YZ为F所蕴含

证明2

设X→Y为F所蕴含，且Z U。

对R的任一关系r中的任意两个元组t,s：

若t[XZ]=s[XZ]，由于X XZ，Z XZ，根据自反律，则有t[X]=s[X]和t[Z]=s[Z]；

由于X→Y，于是t[Y]=s[Y]，所以t[YZ]=s[YZ]；所以XZ→YZ成立，增广律得证。

③ A3传递律：若X→Y，Y→Z为F所蕴含，则X→Z为F所蕴含

证明3

设X→Y及Y→Z为F所蕴含。

对R的任一关系r中的任意两个元组t,s：

若t[X]=s[X]，由于X→Y，有t[Y]=s[Y]；

再由于Y→Z，有t[Z]=s[Z]，所以X→Z为F所蕴含，传递律得证。

④ 合并规则：若X→Y，X→Z，则X→YZ为F所蕴含

证明4

因X→Y（已知）

故X→XY（增广律），XX→XY即X→XY

因X→Z（已知）

故XY→YZ（增广律）

因X→XY，XY→YZ（从上面得知）

故X→YZ（传递律）

⑤ 伪传递规则：若X→Y，WY→Z，则XW→Z为F所蕴含

证明5

因X→Y（已知）

故WX→WY（增广律）

因WY→Z（已知）

故XW→Z（传递律）

⑥ 分解规则：若X→Y，Z Y，则X→Z为F所蕴含

证明6

因Z Y（已知）

故Y→Z（自反律）

因X→Y（已知）

故X→Z（传递律）

第三篇：数学公理

过两点有且只有一条直线两点之间线段最短同角或等角的补角相等同角或等角的余角相等过一点有且只有一条直线和已知直线垂直直线外一点与直线上各点连接的所有线段中，垂线段最短平行公理 经过直线外一点，有且只有一条直线与这条直线平行如果两条直线都和第三条直线平行，这两条直线也互相平行同位角相等，两直线平行内错角相等，两直线平行同旁内角互补，两直线平行

12两直线平行，同位角相等两直线平行，内错角相等两直线平行，同旁内角互补定理 三角形两边的和大于第三边推论 三角形两边的差小于第三边三角形内角和定理 三角形三个内角的和等于180°推论1 直角三角形的两个锐角互余推论2 三角形的一个外角等于和它不相邻的两个内角的和推论3 三角形的一个外角大于任何一个和它不相邻的内角全等三角形的对应边、对应角相等

22边角边公理(SAS)有两边和它们的夹角对应相等的两个三角形全等角边角公理(ASA)有两角和它们的夹边对应相等的两个三角形全等推论(AAS)有两角和其中一角的对边对应相等的两个三角形全等边边边公理(SSS)有三边对应相等的两个三角形全等斜边、直角边公理(HL)有斜边和一条直角边对应相等的两个直角三角形全等27 定理1 在角的平分线上的点到这个角的两边的距离相等定理2 到一个角的两边的距离相同的点，在这个角的平分线上角的平分线是到角的两边距离相等的所有点的集合等腰三角形的性质定理 等腰三角形的两个底角相等(即等边对等角）

推论1 等腰三角形顶角的平分线平分底边并且垂直于底边

等腰三角形的顶角平分线、底边上的中线和底边上的高互相重合33 推论3 等边三角形的各角都相等，并且每一个角都等于60°

等腰三角形的判定定理 如果一个三角形有两个角相等，那么这两个角所对的边也相等（等角对等边）

推论1 三个角都相等的三角形是等边三角形

推论 2 有一个角等于60°的等腰三角形是等边三角形

在直角三角形中，如果一个锐角等于30°那么它所对的直角边等于斜边的一半38 直角三角形斜边上的中线等于斜边上的一半

定理 线段垂直平分线上的点和这条线段两个端点的距离相等

逆定理 和一条线段两个端点距离相等的点，在这条线段的垂直平分线上41 线段的垂直平分线可看作和线段两端点距离相等的所有点的集合

第四篇：经典命题逻辑公理系统定理证明算法设计

Http://logic.zsu.edu.cn/journal.htm 逻辑与认知 Vol.2, No.4, 200

4---

收稿日期：2004-11-25；

作者简介：杜国平，1965 年生，男，汉族，江苏盱眙人，南京大学副教授。

基金项目：国家社科基金项目（02CZX008）；南京大学引进人才基金项目；南京大学笹川青年教育基金项 目。

联系方式：210093 南京大学哲学系 Email: dgpnju@126.com 电话：025-8359716

1经典命题逻辑公理系统定理证明算法设计

杜国平1，2（1.南京大学哲学系 210093；2.南京航空航天大学计算机系 210016）

内容提要：本文利用演绎定理的证明思路给出了一个由演绎证明构造公理证明的一般程序，并增加了一条 简化命令，使该程序既严格又具有实际可操作性。

关键词： 演绎证明 公理证明 程序

中图分类号：B81 文献标识码：A

在经典命题逻辑常见的公理系统中，仅仅从公理和推理规则出发进行定理的形式证明一 般没有能行的程序，对于初学者而言是比较困难的。但是，在经典命题逻辑公理系统中，演 绎定理成立，而使用演绎定理来构造定理的形式证明是比较简单的。实际上，演绎定理的证 明过程已经表明：有了一个使用演绎定理的形式证明（简称为演绎证明），就可以构造出仅 仅从公理和推理规则出发的形式证明（简称为公理证明）。本文拟对由演绎证明构造公理证 明的具体算法和技巧进行一些探讨。

为了说明的方便，我们取如下的命题逻辑公理系统PC 来进行讨论。

系统 PC 由如下三条公理模式和一条推理规则构成：

公理模式为：

(Ax1)A(B A)

(Ax2)(A (B C))((AB)(B C))

(Ax3)(AB)((AB)A)

推理规则即分离规则（Modus ponens）：由A和AB可以推出B。简记为MP。

在系统 PC 中显然可以证明：

演绎定理(DT)：如果，A + B，那么+ AB。

因为任一证明序列都是有限长的，因此，演绎证明中需要引入的假设也是有限的。所以 我们只考虑假设集为有限集的情况，令1 2 1 , , , , m m A A A A L。

假设有一个 0 U A + B的演绎证明，该证明的公式序列为： 1 2 , , , n C C L C B。那么我们可按照下述程序构造出一个+ 0A B的演绎证明。

经典命题逻辑公理系统定理证明算法设计

2[1] 如果A0 Cn是公理或者0 n A C ，则执行如下子程序[1']，即直接写入：

0 n A C

[2] 如果n C 是公理，则执行如下子程序[2'] ：

C

0()n n C A C n

0 n A C

[3] 如果n C 是0 A，则执行如下子程序[3'] ：

A ((B A)A)

0 0 0 0 0 0 0(A ((BA)A))((A (B A))(A A))

0 0 0 0(A (BA))(A A)

0 0 A (BA)

0 0 A A 0 0 0

[4] 如果n k C A ，k 1, 2, L , m，则执行如下子程序[4'] ：

A

0()k k A A A

0 k A A k

[5] 如果n C 是由i C，()(, 1, 2, , 1)j i n C C C i jL n 经使用分离规则而得 到，则对j C 执行如下子程序[5'] ：

(())(()())i n i n A C C A C A C

0 0()()i n A C A C

0 n A C

[6] 对[4]中出现的i C，j C 重复执行程序[1]～[6]。

[7] 若程序全部进入[1]～[4]，则执行完[1'] ～[4']，程序终止。

对 + 0A B 反复使用上述程序m 次之后，就可以得到一个

+ 1 1 0((()))m m A A A A B L L 的公理证明。

例 1 在系统PC中构造定理+((AB)C)(BC)的公理证明。

首先，我们构造一个((AB)C), B + C的演绎证明。

证明1' ：(AB)C 假设B 假设B(AB)(Ax1)AB 2、3 MPC 1、4 MP

其次，由(AB)C，B + C的演绎证明构造(AB)C+ BC的演绎证明。

1、这可以通过回溯检查逐步完成。证明1'的第5 行为C，进入程序[1]检查BC，0 0 0

发现它既不是公理也不属于假设集((AB)C)；进入程序[2]～[5]发现C由第1、4 行(AB)C和AB分离而得。因此，执行子程序[5']：

逻辑与认知 Vol.2, No.4, 200

4(B ((AB)C))((B(AB))(B C))

(B (AB))(BC)

BC2、进入程序[6]，对(AB)C和AB执行程序[1]～[6]。

3、进入程序[1]，检查B((AB)C)，发现它既不是公理也不属于假设集

((AB)C)；进入程序[2]～[5]发现(AB)C属于假设集((AB)C)。

因此，执行子程序[4'] ：

(AB)C

((AB)C)(B ((AB)C))

B((AB)C)

4、进入程序[1]，检查B(AB)，发现它是公理。因此，执行子程序[1']：

B(AB)

5、程序已经全部进入[1]～[4]，并且已经执行完子程序[1'] ～[4']，因此程序终止。所以我们得到一个(AB)C+ BC的演绎证明。

证明1'' ：(AB)C 假设((AB)C)(B ((AB)C))(Ax1)B((AB)C)1、2 MPB(AB)(Ax1)(B ((AB)C))

((B(AB))(B C))(Ax2)(B (AB))(BC)3、5 MPBC 4、6 MP

再次，由(AB)C+ BC的演绎证明构造+((AB)C)(BC)的公

理证明。

1、进入程序[1] 检查((AB)C)(BC)，发现它不是公理（此时，因为假

设集是空集，所以它也当然不属于假设集）；进入程序[2]～[5]发现BC由第4、6 行 B(AB)和(B (AB))(BC)分离而得。因此，执行子程序[5']：

(((AB)C)((B(AB))(B C)))

((((AB)C)(B(AB)))

(((AB)C)(B C)))

(((AB)C)(B(AB)))

(((AB)C)(BC))

((AB)C)(BC)

2、进入程序[6]，对B(AB)和(B (AB))(BC)执行程序[1]～[6]。

3、进入程序[1]，检查((AB)C)(B(AB))，发现它不是公理；进入程 序[2]～[5]发现B(AB)是公理。因此，执行子程序[2'] ：

B(AB)

经典命题逻辑公理系统定理证明算法设计

(B (AB))(((AB)C)(B(AB)))

((AB)C)(B(AB))

4、进入程序[1] 检查((AB)C)((B(AB))(B C))，发现它不是 公理；进入程序[2]～[5]发现(B (AB))(BC)由第3、5行B((AB)C)和(B ((AB)C))((B(AB))(B C))分离而得。因此，执行子程序

[5'] ：

(((AB)C)((B((AB)C))((B(AB))(B C))))

((((AB)C))(B ((AB)C)))

(((AB)C)((B(AB))(B C))))

(((AB)C))(B ((AB)C)))

(((AB)C)((B(AB))(B C))))

((AB)C)((B(AB))(B C)))、进入程序[6]，对B((AB)C)和(B ((AB)C))

((B(AB))(B C))执行程序[1]～[6]。

6、进入程序[1]，检查((AB)C)(B ((AB)C))，发现它是公理。因 此，执行子程序[1'] ：

((AB)C)(B ((AB)C))、进入程序[1]，检 查((AB)C)((B((AB)C))

((B(AB))(BC)))，发现它不是公理； 进入程序[2] ～ [5] 发现

(B ((AB)C))((B(AB))(B C))是公理。因此，执行子程序[2'] ：

(B ((AB)C))((B(AB))(B C))

((B((AB)C))((B(AB))(B C)))

(((AB)C)((B((AB)C))

((B(AB))(BC))))

((AB)C)((B((AB)C))

((B(AB))(BC)))

8、程序已经全部进入[1]～[4]，并且已经执行完子程序[1'] ～[4']，因此程序终止。这样我们就得到一个+((AB)C)(BC)的公理证明。

证明1''' ：((AB)C))(B((AB)C))(Ax1)(B ((AB)C))((B(AB))(B C))(Ax2)((B((AB)C))((B(AB))(B C)))

(((AB)C)((B((AB)C))

((B(AB))(BC))))(Ax1)((AB)C)((B((AB)C))

((B(AB))(BC)))2、3 MP(((AB)C)((B((AB)C))((B(AB))(B C))))

((((AB)C))(B ((AB)C)))

(((AB)C)((B(AB))(B C))))(Ax2)

逻辑与认知 Vol.2, No.4, 200

46(((AB)C))(B ((AB)C)))

(((AB)C)((B(AB))(B C))))4、5 MP((AB)C)((B(AB))(B C)))1、6 MP(((AB)C)((B (AB))(BC))))

((((AB)C)(B(AB)))

(((AB)C)(B C)))(Ax2)(((AB)C)(B(AB)))

(((AB)C)(BC))7、8 MPB (AB))(Ax1)(B (AB)))

(((AB)C)(B(AB)))(Ax1)((AB)C)(B(AB))10、11 MP((AB)C)(BC)9、12 MP

构造程序的[2]~[7]也可以构成一个独立的公理证明构造程序，这是演绎定理的证明中显 示出来的，但该程序很繁琐。程序[1]是一个简化程序，它的加入，可以使构造程序大为简 化，尽管它多了一条程序命令。但是这样就增加了该程序的实际可操作性。

参考文献：

[1] 宋文坚.逻辑学[M].人民出版社,1998.P86-92.[2] 陆钟万.面向计算机科学的数理逻辑[M].科学出版社,2002.P86-92.[3] 周礼全.逻辑百科辞典[M].四川教育出版社,1994.P685.[4] A.G.Hamilton.Logic for Mathematicians[M].清华大学出版社,2003.P32-34.[5] 张清宇 郭世铭 李小五.哲学逻辑研究[M].社会科学文献出版社,1997.The Arithmetic Design for Theorem Proving

in the Axiom System of Classical Propositional Logic

Du Guo-ping1,2

(1.Nanjing University.Nanjing 210093,China;2.Nanjing University of Aeronautics and Astronautics, Nanjing 210016,China)

Abstract: The article uses the proving of deduction theorem to give general program of construction theorem proving, and adding a piece of simplification command.The program is gotten strict and exercisable.Key words: deduction prove;axiom prove;program

第五篇：平行公理

1．平行线的判定公理：两条直线被第三条直线所截，如果同位角相等，那么两条直线平行。

简单说成：同位角相等，两直线平行。

2．平行线的判定定理：两条直线被第三条直线所截，如果内错角相等，那么两条直线平行。

简单说成：内错角相等，两直线平行。

3．平行线的判定定理：两条直线被第三条直线所截，如果同旁内角互补，那么这两条直线平行。简单说成：同旁内角互补，两直线平行。

4．在同一平面内，如果两条直线同时垂直于同一条直线，那么这两条直线平行。

平行线的性质

重点：平行线的三个性质定理。难点：性质定理的应用。

热点：应用平行线性质定理进行角度大小的换算。

1．平行线的性质

（1）公理：两条平行线被第三条直线所截，同位角相等。可以简述为：两直线平行，同位角相等。

（2）定理：两条平行线被第三条直线所截，内错角相等。可以简述为：两直线平行，内错角相等。

（3）定理：两条直线被第三条直线所截，同旁内角互补。可以简述为：两直线平行，同旁内角互补。

2．平行线的性质小结：

（1）两直线平行，同位角相等、内错角相等、同旁内角互补。

（2）垂直于两平行线之一的直线，必垂直于另一条直线。

（2）对顶角和邻补角的概念

1,对顶角的概念① 两条直线相交成四个角，其中有公共顶点而没有公共边的两个角叫做对顶角；② 一个角的两边分别是另一个角的两边的反向延长线，这两个角叫做对顶角.实际上，两条直线相交，其中不相邻的两个角就是对顶角，相邻的角就是邻补角.○2 对顶角的性质；对顶角相等.○3 互为邻补角的两个角一定互补，但两个角互补不一定是互为邻补角；

○4 对顶角有一个公共顶点，没有公共边；邻补角有一个公共顶点，有一个公共边.垂线的性质：

○1过直线外一点有且只有一条直线与已知直线垂直；

○2直线外一点与直线上各点连结的所有线段中，垂线段最短，简单说成：垂线段最短.点到直线的距离定义：从直线外一点到这条直线的垂线段的长度叫做点到直线的距离.相交线是同一平面内两条直线的一种位置关系;

平行线的判定.同位角相等

内错角相等

同旁内角互补

在同一平面内两条直线只有两种位置关系[1]相交[2]平行