冷推论191:(协调性定理)F不是 Pred(Y的定理。 冷引理194设A是P(Y的协调子集。如果 日xp(x)∈A, svar((A,且y不在p(x)中出现, 则 FADed(AUp(y) 冷反证:若F∈ Ded(AUp(y),设法证明F∈Ded(A) 冷由演绎定理和G规则得y_p(y)eDed(A), 冷再由约束变元可替换性得xp(x)∈Ded(A) 冷利用MP规则可得F∈Ded(A),与A协调矛盾❖ 推论19.1:(协调性定理):F不是Pred(Y)的定理。 ❖ 引理19.4:设A是P(Y)的协调子集。如果 xp(x)A，yvar(A)，且y不在p(x)中出现， 则FDed(A∪p(y))。 ❖ 反证:若FDed(A∪p(y)),设法证明FDed(A) ❖ 由演绎定理和G规则得yp(y)Ded(A), ❖ 再由约束变元可替换性得xp(x)Ded(A), ❖ 利用MP规则可得FDed(A),与A协调矛盾