复旦大学：《离散数学——代数结构与数理逻辑》PPT课件_23/29

§3命题演算的形式证明 个数学系统通常由一些描述系统特 有性质的陈述句所确定,这些陈述句 称为/没 系统的其它性质的证明,由一组陈述 句组成,其中最后的陈述句描述所期 望的性质,而中间的陈述句总是由它 前面的陈述句通过系统所允许的方法 推得

§3 命题演算的形式证明 一个数学系统通常由一些描述系统特 有性质的陈述句所确定，这些陈述句 称为假设， 系统的其它性质的证明，由一组陈述 句组成，其中最后的陈述句描述所期 望的性质，而中间的陈述句总是由它 前面的陈述句通过系统所允许的方法 推得

◆采用两个方法 些在任何数学证明中公认允许采用 的陈述句,把它们形式化地表述成若 干特殊的命题,这些命题可在证明的 任何一步引入,这些命题被称为公理; ◆另一个采用的方法是由若干规则构成, 这些规则规定:从某些陈述导出某些 特定陈述是可接受的,这些规则在形 式化之后,称为系统的推理规则

 采用两个方法：  一些在任何数学证明中公认允许采用 的陈述句，把它们形式化地表述成若 干特殊的命题，这些命题可在证明的 任何一步引入，这些命题被称为公理；  另一个采用的方法是由若干规则构成， 这些规则规定：从某些陈述导出某些 特定陈述是可接受的，这些规则在形 式化之后，称为系统的推理规则

对于集合X上的命题演算,称X上的自 由命题代数P(X)的子集A=A1UA2UA3 中的所有元素为系统的公理。其中: A1={p→(q→p)p,q∈P(X)} A2={(p→(q→r)→(p→q)→(p→r)|p,qr ∈P(X} ◆A3={-p→pp∈P(X} 系统的推理规则采用MP规则( modus ponens):由p和p>q可导出q

 对于集合X上的命题演算，称X上的自 由命题代数P(X)的子集A=A1∪A2∪A3 中的所有元素为系统的公理。其中：  A1={p→(q→p)|p,qP(X)}；  A2={(p→(q→r))→((p→q)→(p→r))|p,q,r P(X)}；  A3={p→p|pP(X)}。  系统的推理规则采用MP规则(modus ponens)：由p和p→q可导出q

定义1813:设q∈P(X),AcP(X),在集 合X上的命题演算中,由假设A导出q的 证明是一组有限序列p,Pn,这里p∈ P(X)(i=1,…,n),pn=q,并且对每个i, 或者p∈AUA,或者存在jk(k<i),有 ◆例:A={q},由A导出p>q的证明为: 证明 PIg p2=q→(p→q)A1 p3=(p-q pup2MP

 定义18.13:设qP(X)，AP(X)，在集 合X上的命题演算中，由假设A导出q的 证明是一组有限序列 p1 ,…,pn，这里pi P(X)(i=1,…,n)，pn=q，并且对每个i， 或者piA∪A，或者存在j,k(j,k<i)，有 pk=(pj →pi )。  例：A={q},由A导出p→q的证明为：  证明：p1=q A  p2=q→(p→q) A1  p3 =(p→q) p1 ,p2MP

定义18.14设q∈PX),A∈P(X),如果存 在一个由A导出q的证明,则称q是A的 推导,或称q是从A可证明的,记为 Aq,且用Ded(A)表示A的推导全体。 {q}卜p→q 定义1815:设p∈PX),如果存在一个由 O导出p的证明,则称p是X上的命题演 算的定理。记为②卜p,也简写为卜p

 定义18.14:设qP(X)，AP(X)，如果存 在一个由A导出q的证明，则称q是A的 推导，或称q是从A可证明的，记为 A┝q，且用Ded(A)表示A的推导全体。  {q}┝p→q  定义18.15:设pP(X)，如果存在一个由 导出p的证明，则称p是X上的命题演 算的定理。记为┝p，也简写为┝p