设个体域A=，公式在A上消去量词后应该为怎样的谓词公式

设个体域A=，公式在A上消去量词后应该为怎样的谓词公式

在屈婉岭编的《离散数学》里p75对于存在量词消去规则的解释是3.存在量词消去规则 存在量词消去规则a(x)→b→∴存在xa(x)→b其中x是个体变项符号,且不在γ的任何公式和b中自由出现

Skolem标准形的定义： 前束范式中消去所有的存在量词，则称这种形式的谓词公式为Skolem标准形，任何一个谓词公式都可以化为与之对应的Skolem标准形。但是，Skolem标准形不唯一。 前束范式：A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。 Skolem标准形的转化过程为，依据约束变量换名规则，首先把公式变型为前束范式，然后依照量词消去原则消去或者略去所有量词。具体步骤如下： 将谓词公式G转换成为前束范式 前束范式的形式为： (Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn) 即： 把所有的量词都提到前面去。 注意：由于所有的量词的辖域都延伸到公式的末端，即，最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。 约束变量换名规则： (Qx ) M（x） （Qy ） M（y） (Qx ) M（x,z） （Qy ） M（y,z） 量词否定等值式： ～(x ) M（x） （y ） ～ M（y） ～(x ) M（x） （y ） ～ M（y） 量词分配等值式： (x )( P（x） ∧Q（x）) (x ) P（x） ∧ (x ) Q（x） (x )( P（x） ∨ Q（x）) (x ) P（x） ∨ (x ) Q（x） 消去量词等值式：设个体域为有穷集合（a1, a2, …an） (x ) P（x） P（a1） ∧ P（a2） ∧ …∧ P（an） (x ) P（x） P（a1） ∨ P（a2） ∨ … ∨ P（an） 量词辖域收缩与扩张等值式： ( x )( P（x） ∨ Q) ( x ) P（x） ∨ Q (x )( P（x） ∧ Q) ( x ) P（x） ∧ Q (x )( P（x） → Q) (x ) P（x） → Q (x )( Q → P（x） ) Q → (x ) P（x） (x )( P（x） ∨ Q) (x ) P（x） ∨ Q (x )( P（x） ∧ Q) (x ) P（x） ∧ Q (x )( P（x） → Q) (x ) P（x） → Q (x )( Q → P（x） ) Q → (x ) P（x）