§3 命题演算的形式证明 一个数学系统通常由一些描述系统特有性质的陈述句所确定，这些陈述句称为假设， 系统的其它性质的证明，由一组陈述句组成，其中最后的陈述句描述所期望的性质，而中间的陈述句总是由它前面的陈述句通过系统所允许的方法推得。
采用两个方法： 一些在任何数学证明中公认允许采用的陈述句，把它们形式化地表述成若干特殊的命题，这些命题可在证明的任何一步引入，这些命题被称为公理； 另一个采用的方法是由若干规则构成，这些规则规定：从某些陈述导出某些特定陈述是可接受的，这些规则在形式化之后，称为系统的推理规则。
对于集合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。
定义18.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
定义18.14:设qP(X)，AP(X)，如果存在一个由A导出q的证明，则称q是A的推导，或称q是从A可证明的，记为A┝q，且用Ded(A)表示A的推导全体。 {q}┝p→q 定义18.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 引理18.2: (i)若qDed(A)，则必存在A的有限子集A'，使得qDed(A')。 (ii) Ded在P(X)满足 ADed(A) 若A1A2,则Ded(A1) Ded(A2) Ded(Ded(A))=Ded(A)
定理18.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 然后由演绎定理即可得
定理18.6(代换定理):设X,Y是两个集合，是P(X)→P(Y)的同态映射，这里P(X)和P(Y)分别是X,Y上的(自由)命题代数。设w=w(x1,,xn)是P(X)的元素，A是P(X)的子集，令qi=(xi),qiP(Y)， (1)如果A┝w，则(A)┝(w)(=w(q1,,qn)) (2)如果A╞w，则 (A)╞(w)(=w(q1,,qn))
证明:(1)设p1,,pm为由A证明w的序列. ①piA,则(pi)(A) ②piA ③pi是由pj和pk=(pj→pi)得到(j,k<I)。 (2)设A╞w,v是P(Y)的赋值,即为P(Y)到Z2的同态映射,并使v((A)){1} 关键证明v((w))是否为1.
推论18.2:设P(Xn)为Xn上的命题代数，piP(Xn)(i=1, ,n), w=w(x1,,xn)P(Xn)，则有： (1)如果┝w，则┝w(p1,,pn)。 (2)如果╞w，则╞w(p1,,pn)。 定义18.16:设p,wP(X)，若p在w中出现，则称p为w的子公式。
定理18.7(子公式替换定理):设w,p,p'P(X)，p为w的子公式，把p在w中的某些出现替换为p'得到的公式记为w'。 (1)若┝pp'，则有┝ww'。 (2)若╞pp'，则有╞ww'。
作业:P241 8,10,11