§4 命题演算的形式证明 一个数学系统通常由一些描述系统特有性质的陈述句所确定，这些陈述句称为假设， 系统的其它性质的证明，由一组陈述句组成，其中最后的陈述句描述所期望的性质，而中间的陈述句总是由它前面的陈述句通过系统所允许的方法推得。
采用两个方法： 一些在任何数学证明中公认允许采用的陈述句，把它们形式化地表述成若干特殊的命题，这些命题可在证明的任何一步引入，这些命题被称为公理； 另一个采用的方法是由若干规则构成，这些规则规定：从某些陈述导出某些特定陈述是可接受的，这些规则在形式化之后，称为系统的推理规则。
对于集合X上的命题演算，称X上的自由命题代数P(X)的子集A=A1∪A2∪A3中的所有元素为系统的公理。其中： A1={p→(q→p)|p,qP(X)}； A2={(p→(q→r))→((p→q)→(p→r))|p,q,rP(X)}； A3={p→p|pP(X)}。 系统的推理规则采用MP规则(modus ponens)：由p和p→q可导出q。
定义20.13:设qP(X)，AP(X)，在集合X上的命题演算中，由假设A导出q的证明是一组有限序列 p1,…,pn，这里pi P(X)(i=1,…,n)，pn=q，并且对每个i，或者piA∪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:设qP(X)，AP(X)，如果存在一个由A导出q的证明，则称q是A的推导，或称q是从A可证明的，记为A┝q，且用Ded(A)表示A的推导全体。 {q}┝p→q 定义20.15:设pP(X)，如果存在一个由导出p的证明，则称p是X上的命题演算的定理。记为┝p，也简写为┝p。
例：{p→(q→r), q→(r→s),p}┝q→s 证明：p1=p A p2= p→(q→r) A p3=(q→r) p1,p2 MP p4= q→(r→s) A p5=(q→(r→s))→((q→r)→(q→s)) A2 p6=(q→r)→(q→s) p4,p5 MP p7=(q→s) p3,p6 MP 所以有{p→(q→r), q→(r→s),p}┝q→s
例：┝F→q 例：{p}┝p→q 引理20.2: (i)若qDed(A)，则必存在A的有限子集A'，使得qDed(A')。 (ii) Ded在P(X)满足 ADed(A) 若A1A2,则Ded(A1) Ded(A2) Ded(Ded(A))=Ded(A)
定理20.5(演绎定理):设AP(X), p,qP(X)，则A┝p→q 当且仅当A∪{p}┝q。 因为A┝p→q,，故存在A导出p→q的有限证明序列 p1,…,pn=p→q， 则对于A∪{p}有证明序列 p1,…,pn=p→q， pn+1=p，A∪{p} pn+2=q，pn+1,pn MP
2. A∪{p}┝q要证明A┝p→q 因为A∪{p}┝q，故存在A∪{p}导出q的有限证明序列 p1,…,pn=q，为了证明A┝p→q，对A∪{p}┝q的证明序列长度作归纳证明。 例：证明{p→q, q→r}┝p→r 证明： 先证{p→q, q→r,p}┝r 然后由演绎定理即可得
作业:P400 8,10,11