《离散数学》PPT课件-命题演算的形式证明

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

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

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

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

对于集合X上的命题演算，称X上的自由命题代数P(X)的子集A=A,U A,U A,中的所有元素为系统的公理。其中：A,=(p→(q-→p)lp,qeP(X)) ;A2={(p-→(q→r)-→(p→q)(p→r)lp,q,rEP(X)) ;A={--p→plpeP(X))。系统的推理规则采用MP规则（modusponens)：由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

定义20.13:设qeP(X)，AcP(X)，在集合X上的命题演算中，由假设A导出的证明是一组有限序列 P1,..,Pn，这里p;EP(X)(i=l,...,n)，Pn=q，并且对每个i,或者p;EAU A，或者存在j,k(j,k<i)，有Pk=(P;→p:)。例：A={qi,由A导出p一→q的证明为：A证明：Pi=qA1p2=q→(p→q)P3=(p→q)P1,P2MP

 定义20.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

定义20.14:设eP(X)，AcP(X)，如果存在一个由A导出q的证明，则称q是A的推导，或称q是从A可证明的，记为A 卜q，且用Ded(A)表示A的推导全体。(q) Fp-q定义20.15:设peP(X)，如果存在一个由①导出p的证明，则称p是X上的命题演算的定理。记为の 卜p，也简写为 p

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