定义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