北京航空航天大学离散数学课件3. 第三章 公理系统.pdf

离散数学(1): 数理逻辑 Discrete Mathematics (1): Mathematical Logic 第三章 公理系统 赵永望 zhaoyw@buaa.edu.cn 北京航空航天大学计算机学院 内容 • 3.0. 公理系统简介 • 3.1. 命题逻辑的公理系统 • 3.2. 谓词逻辑的公理系统 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 2 欧式几何：公理系统 • 欧式几何的传统描述是一个公理系统，通过有 限的公理来证明所有的“真命题”。 • 欧式几何的五条公理是： – 1、任意两个点可以通过一条直线连接。 – 2、任意线段能无限延长成一条直线。 – 3、给定任意线段，可以以其一个端点作为圆心， 该线段作为半径作一个圆。 – 4、所有直角都全等。 – 5、若两条直线都与第三条直线相交，并且在同一 边的内角之和小于两个直角和，则这两条直线在这 一边必定相交。 • 第五条公理称为平行公理（平行公设） 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 3 逻辑公理—表达思想的初始概念 • 自然数公理 – x (s(x)x) – xy (xy s(x)s(y )) – x (x+0=x) – xy (x+s(y )=s(x+y )) – x (x ∘0=0) – xy (x ∘s(y )=x ∘y +s(x) – (Q(0)x (Q(x)Q(s(x))))xQ (x) 皮亚诺 • 自然数公理是实质公理 （1858-1932） – 具体概念：后继(s)，0，+ ，∘，Q • 自然数公理是所有的自然数命题真值的依据。 • 从自然数公理能推导出所有的自然数命题真 值。 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 4 形式系统 • 一个形式系统应当包括以下几部分。 – (1)各种初始符号。初始符号是一个形式系统的 “字母”，经解释后 其中一部分是初始概念。 – (2)形成规则。规定初始符号组成各种合适符号序列的规则。经解释 后合式符号序列是一子句，称为系统里的合式公式或命题。 – (3)公理。把某些所要肯定的公式选出，作为推导其它所要肯定的公 式的出发点，这些作为出发点的公式称为公理。 – (4)变形规则。变形规则规定如何从公理和已经推导出的一个或几个 公式经过符号变换而推导出另一公式。经过解释，变形规则就是推 理规则。 – 应用变形规则进行推导可以得到一系列公式，这些公式经过解释是 系统的定理。 • 形式系统完全由一套表意符号建立，它能克服日常语言的歧 义性，使概念、判断、推理精确化。 《离散数学》课程 北京航空航天大学计算机学院赵永望(zhaoyw@buaa.edu.cn) 5 希尔伯特证明论 • 通过形式化第一次使证明本身成 为数学研究对象。 • 给出初始符号集合 • 构造合式公式规则