第二章 谓词演算及其形式系统

2.1 个体谓词和量词

2.1.1 个体

个体常元(constants):确定的个体用$a,b,c$等小写字母或字符串表示，称为常元(constants)
个体变元(variables):不确定的个体常用字母$x,y,z,u,v,w$等表示，称为变元(variables)

个体域(domain of individuals)：谓词演算中把讨论对象–个体的全体称为个体域，常用字母$D$表示，并约定任何$D$中都至少含有一个成员。
全总域(universe)：当讨论对象遍及一切客体时，个体域特称为全总域，用字母$U$表示。

元数：通常把谓词所携空位的数目称为谓词的元数。
谓词命名式：含空位的写法有一个明显的缺点，可读性差。因此常用变元来代替空位，被称为谓词命名式，简称谓词。

谓词演算永真式

谓词公式的前束范式

一阶谓词演算形式系统

谓词逻辑的等值演算与推理