谓词演算

---

是谓词逻辑的形式化。

由于使用了量词，谓词演算的推理能力比命题演算有很大的加强。事实上，它已成为许多公理系统的组成部分，起著基本的逻辑工具的作用。

谓词演算所使用的语言L_R含有如下几类符号：

(1)个体变元：x₁、x₂、……；

(2)命题联接词：，∧，∨，→，；

(3)量词：，；

(4)等词：=；

(5)辅助符号：)，(；

(6)对每个n≥1，一个n元关系符号集(可以为空)；

(7)对每个n≥1，一个n元函数符号集(可以为空)；

(8)一个常元符号集(可以为空)。

L_R中的项可递归定义如下：

(1)个体变元是项；

(2)常元是项；

(3)如果f是n元函数符号，x₁，…x_n是项，则f(x₁…x_n)是项。

(4)只有从(1)——(3)生成的表达式才是项。

谓词演算中的公式可递归定义如下：

(1)如果t₁、t₂是项，则t₁=t₂是公式；

(2)如果R是n元关系符号，t₁，…t_n是项，则Rt₁…t_n是公式；

(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的自由出现。

可以证明，此公理系统是完全的，即如果一谓词演算的公式是永真的，则可由上述系统推出该公式。