不明白谓词公式　　h谓词公式，由原子公式、联结词和量词可构成谓词公式(严格定义见教材). 命题的符号化结果都是谓词公式. 　　例如"x(F(x)®G(x))，$x(F(x)ÙG(x))，"x"y(F(x)ÙF(y)ÙL(x,y)®H(x,y))等都是谓词公式. 　　h变元与辖域，在谓词公式"xA和$xA中，x是指导变元，A是相应量词的辖域. 在"x和$x的辖域A中，x的所有出现都是约束出现，即x是约束变元，不是约束出现的变元，就是自由变元. 也就是说，量词后面的式子是辖域. 量词只对辖域内的同一变元有效. 　　h换名规则，就是把公式中量词的指导变元及其辖域中的该变元换成该公式中没有出现的个体变元，公式的其余部分不变. 　　h代入规则，就是把公式中的某一自由变元，用该公式中没有出现的个体变元符号替代，且要把该公式中所有的该自由变元都换成新引入的这个符号.解释(赋值)　　h解释(赋值)，谓词公式A的个体域D是非空集合，则 　　(1) 每一个常项指定D中一个元素； 　　(2) 每一个n元函数指定Dn到D的一个函数； 　　(3) 每一个n元谓词指定Dn到{0,1}的一个谓词； 　　按这个规则做的一组指派，称为A的一个解释或赋值. 　　在有限个体域下，消除量词的规则为：如D={a1,a2,…,an}，则 　　h谓词公式分类，在任何解释下，谓词公式A取真值1，公式A为逻辑有效式(永真式)；在任何解释下谓词公式A取真值0，公式A为永假式；至少有一个解释使公式A取真值1，公式A称为可满足式.