谓词公式与个体变元

2.2 谓词公式与解释谓词公式：谓词演算的合式公式。

2.2 谓词公式与解释定义2.8P(t1, t2, …,tn)称为谓词演算的原子谓词公式，其中，P是谓词，t1, t2, …, tn是个体变元、个体常元或任意的n元函数。定义2.91）原子谓词公式是谓词公式；2）若A是谓词公式，则(﹁A）也是谓词公式；

3）若A和B都是谓词公式，则(A∧B), (A∨B), (A?B), (A?B)都是谓词公式；4）若A是谓词公式，x是任何个体变元，则?xA和?xA都是谓词公式；

5）只有经过有限次地应用规则1），2），3），4）所得到的公式是谓词公式。

2.2.1 谓词公式的定义根据运算的优先级，有些括号可以适当的去掉如：

F(x)F(x)??G(x,y)?x(F(x)?G(x))?x?y(F(x)?G(y)?L(x,y))都是谓词公式。2.2.2 自由与约束定义2.１０对于谓词公式?xA或?xA来说，x称为量词?x或量词?x的指导变元或作用变元。A称为相应量词的辖域。在?x和?x的辖域中，x的所有出现都称为约束出现，所有约束出现的变元称为约束变元。A中不是约束出现的其他变元均称为是自由出现的，所有自由出现的变元为自由变元。

例2.5说明下列各式中量词的辖域与变元约束的情况：1）?xF(y)2）?x(F(x)?G(x))3）?x(F(x)??yG(x, y))4）?x?y(F(x, y)∧G(y, z))∧?xF(x, y)

5）?x(F(x)∧?xG(x, z)??yH(x, y))∨G(x, y)6）?x(F(x)?G(x))∧?xH(x)∧R(x)

2.2.2 自由与约束解：1）?xF(y)?x的辖域是F(y)，其中y为自由出现。2）?x(F(x)?G(x))?x的辖域是F(x)?G(x), x为约束出现。3）?x(F(x)??yG(x, y)) ?x的辖域是F(x)??yG(x, y), ?y的辖域是G(x, y)，其中x, y都为约束出现。4）?x?y(F(x, y)∧G(y, z))∧?xF(x, y)

?x的辖域是?y(F(x, y)∧G(y, z))，?y的辖域是F(x, y)∧G(y, z)，?x的辖域是F(x, y)，其中在?x?y(F(x, y)∧G(y, z))中，x，y都为约束出现，z为自由出现，在?xF(x, y)中，x为约束出现，y为自由出现。