定理2010宏备性定到设 AcP(X,peP(X,若在Prop(X)中有AFp, 则在Prop(X)中有AFp 引理206:设w=w(x1…,xn)∈P(X,则Hw 当且仅当w的真值函数f是常值函数1。 定理2011Prop(X)的有效性是可判定的 推论204Prop(X是可证明性可判定的。 定理20.10(完备性定理):设 AP(X),pP(X)，若在Prop(X)中有A╞p， 则在 Prop(X)中有A┣p。  引理20.6:设w=w(x1 ,…,xn )P(X)，则╞w 当且仅当w的真值函数fw是常值函数1。  定理20.11:Prop(X)的有效性是可判定的  推论20.4:Prop(X)是可证明性可判定的