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