如果α,βX,γ 　　那么α,X,βγ 　　∧ 如果X, Y,α,βγ 　　那么α, X∧Y,βγ。 　　∨ 如果X,α,βγ而且Y,α,βγ 　　那么α, X∨Y,βγ 　　→ 如果Y,α,βγ而且α,β X,γ 　　那么α, X→Y,βγ 　　 如果X, Y,α,βγ而且α,βX, Y,γ 　　那么α, XY,βγ 　　后件规则 　　 如果X,αβ,γ 　　那么αβ,X,γ 　　∧ 如果αX,β,γ而且αY,β,γ 　　那么αβ, X∧Y,γ 　　∨ 如果αX, Y,β,γ 　　那么αβ, X∨Y,γ 　　→ 如果X,αY,β,γ 　　那么αβ, X→Y,γ 　　如果X,αY,β,γ而且Y,αX,β,γ 　　那么αβ, XY,γ 　　为理解这些规则的正确性, 我们举其中两条为例加以说明。规则中的X, Y表示公式，α,β,γ表示公式串, 为说明方便也将α,β,γ认为是公式。 　　规则说，只要将公式X加否定, 便可由的右端移到左端。这是个增加联结词的过程。如果反向使用就是消除联结词的规则。依定义α,βX,γ就是 　　α∧βX∨γ 　　或写成 α∧βX→γ 　　自然有 α∧β∧Xγ 　　这就是 α,β,Xγ。 　　规则∨，是增加联结词∨的规则，证明定理时是反向使用的，所以是消除联结词∨的规则了。依定义，∨中的条件就是 　　X∧α∧βγ 而且 　　Y∧α∧βγ 　　自然有 (X∧α∧β)∨(Y∧α∧β)γ 　　即 α∧(X∨Y)∧βγ 　　也就是α, X∨Y,βγ 　　6. 定理的推演 　　定理证明的算法: 　　(1) 将所要证明的定理 A1∧A2∧…∧An→B(其中Ai, B是可能含有其他联结词的公式), 写成相继式形式 　　A1∧A2∧…∧AnB 　　从这相继式出发。 　　(2) 反复(反向)使用变形规则, 消去全部联结词以得到一个或多个无联结词的相继式。 　　(3) 若所有无联结词的相继式都是公理, 则定理得证, 否则定理不成立。