谓词演算

　　谓词演算（predicate calculus），数理逻辑最基本的形式系统。又称一阶逻辑。一个可以回答真假的命题，不仅可以分析到简单命题，还可以分析到其中的个体、量词和谓词。个体表示某一个物体或元素，量词表示数量，谓词表示个体的一种属性。除了一元谓词，也可以有二元，三元，甚至多元谓词。事实上，数学中的关系，函数都可以看成谓词。

　　谓词可以在一定的个体集合中给出解释，谓词公式可以在这样的个体集合中取到真假值。谓词公式在个体集合中取值的严格定义称为基本语义定义，这个定义是波兰籍数学家A.塔尔斯基在20世纪30年代给出的。给定了谓词解释的个体集合称为模型。基本语义定义使谓词公式和模型都可以被当作数学对象加以研究。一个谓词公式在任意一个模型中都取真值，就称之谓恒真式。两个谓词公式A，B在任意模型的任何一种解释下都取相同的值，就称A，B逻辑等价。命题演算中的恒真式和等价式所反映的规律在谓词演算中仍成立。谓词演算中还有一些有关量词的等价式。

　　谓词演算也研究谓词公式的推演。谓词演算也可以公理化。从符号到公式的定义，从公理到推演都严格形式化，构成完全的公理系统，使系统所推演出的都是恒真式，且每个恒真式都能从公理推演出来。与命题演算不同的是，谓词演算是一个不可判定的系统，即不存在一个算法来判定谓词公式是否恒真式。