谓词演算
书籍：方法大辞典
出处：按学科分类—自然科学总论 山东人民出版社《方法大辞典》第95页（1437字）
是谓词逻辑的形式化。
由于使用了量词，谓词演算的推理能力比命题演算有很大的加强。事实上，它已成为许多公理系统的组成部分，起着基本的逻辑工具的作用。
谓词演算所使用的语言LR含有如下几类符号：
(1)个体变元：x1、x2、……；
(2)命题联接词：
，∧，∨，→，
；
(3)量词：
，
；
(4)等词：=；
(5)辅助符号：)，(；
(6)对每个n≥1，一个n元关系符号集(可以为空)；
(7)对每个n≥1，一个n元函数符号集(可以为空)；
(8)一个常元符号集(可以为空)。
LR中的项可递归定义如下：
(1)个体变元是项；
(2)常元是项；
(3)如果f是n元函数符号，x1，…xn是项，则f(x1…xn)是项。
(4)只有从(1)——(3)生成的表达式才是项。
谓词演算中的公式可递归定义如下：
(1)如果t1、t2是项，则t1=t2是公式；
(2)如果R是n元关系符号，t1，…tn是项，则Rt1…tn是公式；
(3)若φ是公式，则(＞φ)是公式；
(4)若φ，ψ是公式，则(φ∧ψ)，(φ∨ψ)，(φ→ψ)，
也是公式；
(5)若φ是公式，x是变元，则
和
也是公式；
(6)只有从(1)－(5)生成的表达式才是公式。
谓词演算的形式推理系统有多种，现介绍其中的一种。
公理：
(1)命题演算的公理都是谓词演算的公理，
(2)
，
，其中t是一个项；
推理规则：
(1)由A和A→B可推出B；
(2)由C→A(x)可推出
；其中C中没有x的自由出现
(3)由A(x)→C，可推出
，其中C中没有x的自由出现。
可以证明，此公理系统是完全的，即如果一谓词演算的公式是永真的，则可由上述系统推出该公式。