和经典命题逻辑相似，经典谓词逻辑也包括不同的公理系统以及自然演算系统。

一、公理化谓词演算系统

公理化谓词演算系统是完全形式化的理论体系。它从若干条作为公理的普遍有效式出发，通过使用推理规则，建立起关于一系列另外的普遍有效式即定理的完整体系。

公理化谓词演算系统可以采取不同的方式构造，这里介绍的系统称为Q系统。

（一）初始符号

1.变项

（1）命题变项：用小写拉丁字母表示，如p，q，r，s，P₁，q₁，r₁……

（2）个体变项：用小写拉丁字母表示，如u，v，w，x，y，z……

（3）谓词变项：用大写拉丁字母F，G，H等表示性质，用R，S，T等表示关系。

2.常项

（1）命题联结词：┓（否定），V（析取）

（2）量词：∀…（全称量词），ヨ…（存在量词）

3.技术性符号

左括号“(”和右括号“)”；逗点“，”

（二）形成规则

在讨论谓词演算的形成规则之前，先介绍以下几个语法符号：

小写希腊字母π，表示任意命题变项；

大写希腊字母△，表示任意个体变项；

大写希腊字母Γ，表示任意谓词；

大写拉丁字母X，Y，Z，表示任意符号序列；

大写拉丁字母A，B，C，D，E等，表示任意合式公式。

谓词演算的形成规则：

1.任意命题变项π是合式公式。如：p，q，r是合式公式。

2.任意谓词变项Γ，后继有写在一对括号内并用逗点分开的适当数目的个体变项是合式公式。如：P(x)，R(x，y，z)是合式公式。

3.如果X是合式公式，那么，┓X也是合式公式。如：┓q，┓P(y)，┓R(x，y，z)是合式公式。

4.如果X和Y是合式公式，并且没有任何一个个体变项△，此△在二者之一中是约束的，但在另一个中是自由的，那么，XVY是合式公式。如：pVG(x)，∀xF(x)VG(y)是合式公式。

5.如果X为合式公式，并且△在其中是自由的，那么，∀△X和ヨ△X是合式公式如：∀xT(x，y)，ヨx(pΛF(x)）都是合式公式。

6.只有符合以上五条规则的符号序列才是合式公式。

（三）定义

1.A→B定义为┓AVB。

2.AΛB定义为┓(┓AV┓B)。

3.A↔B定义为(A→B)Λ(B→A)。

以上定义引入了否定和析取以外的三个联结词。这样，某些包含有→，Λ和↔这三个符号的符号序列也属于合式公式。

（四）公理

1.pVp→p

2.p→pVq

3.pVq→qVp

4.(q→r)→(pVq→pVr)

5.∀xF(x)→F(y)

6.F(y)→ヨxF(x)

以上六条公理中，前四条是命题演算公理系统P的公理，后两条是新增加的。

公理5的含义是：如果所有个体都是F，那么，某一个体是F。这体现了从一般到个别的推理过程。

公理6的含义是：如果某个体是F，那么，存在着一个个体，该个体是F。这体现了从个别到存在的推理过程。

（五）推理规则

1.代入规则

谓词逻辑公理系统有三种变项，因此，推导过程中的代入也就可能发生三种情况：命题变项代入、自由个体变项代入和谓词变项代入。

关于代入，谓词逻辑提出了两个总的要求：保持合式公式和普遍有效性不被破坏。

换言之，对任何一个合式公式，进行代入的结果必须仍然是一个合式公式；对任何一个普遍有效式，进行代入的结果必须仍然是一个普遍有效式。

为了实现上述两项根本要求，三种变项在具体代入时都要分别作出一些限制。

（1）命题变项代入规则

在公式A中出现的命题变项π，可由一个公式B代入。

代入必须在π出现的一切位置上进行。此外，关于B，还必须符合以下要求：

第一，如果某个体变项△在A中为自由变项，那么，B中不得包含约束变项△。

第二，如果某个体变项△在A中为约束变项，那么，在B中不得包含自由变项△。

第三，如果某个体变项△在A中为约束变项，并且π又在∀△或ヨ△的辖域之中，那么，B中不得包含约束变项△。

以下的代入情况是错误的：

例5-1 在qVG(y)中,用∀yG(y)代入q，

得：∀yG(y)VG(y)

例5-2 在∀xF(x)Vp中，用G(x)代入P，

得：∀xF(x)VG(x)

例5-3 在pVヨx(F(x)Vq)中，用∀xG(x)代入q，

得：pVヨx(F(x)V∀xG(x))

（2）自由个体变项代入规则

公式A中的某自由个体变项△₁，可用另一个体变项△₂代入。

代入必须在A中△₁的所有出现位置上进行。此外，△₂不得在A中作为约束变项出现。

以下的代入情况是错误的：

例5-4 在F(y)→∀xF(x)中，用x代入y，

得：F(x)→∀xF(x)

（3）谓词变项代人规则

在说明谓词变项代人规则之前，先介绍“复合谓词”这一概念。

一个包含有自由个体变项的合式公式，由于该公式的真值受到自由个体变项取值情况的制约，所以，可以把该公式看作其中所包含的某些自由个体变项的谓词。这种谓词，称为复合谓词。

例如，公式∀x(pVR(x，y，z))中包含有自由个体变项y、z，该公式的真值随y和z的取值情况而确定。所以，可以把该公式视为y、z的谓词。这样的谓词，就称之为复合谓词。

一般地，n元复合谓词可以表示为：

B(△₁，△₂，△₃…△n) (n>0)

其中，自由个体变项的值不必不相同，也不必按△₁，△₂，△₃…△n的次序出现。

谓词变项代入规则的内容是：公式A中的n元谓词变项Γ(△₁，△₂，△₃…△n)可以处处代之以另一复合谓词B(△₁，△₂，△₃…△n，△n₊₁，△n₊₂…△n+m)(m≥0)

谓词变项代入时，除了要在A的所有出现处进行外，还必须符合以下要求：

第一，代人后得到的符号序列必须是合式公式。

第二，A中的自由个体变项，在代入后不得被B中的量词约束。

第三，如果m>0，那么，B(△₁，△₂，△₃…△n，△n₊₁△n₊₂…△n+m)（m≥0)中的变项△n₊₁，△m₊₂…△n+m，在代入后不得被A中的原有量词约束。

在以下列举的每组谓词变项代入情况中，第一种是正确的，第二种是错误的：

2.分离规则

由公式A→B和A，可以推出公式B。(这里的A和B，可以是谓词逻辑中的任一合式公式)

3.后件概括规则

如果△在A中不自由出现，那么，从A→B(△）可以推出A→∀△B(△）。

4.前件存在规则

如果△在B中不自由出现，那么，从A（△）→B可以推出ヨ△A(△)→B。

5.约束个体变项易字规则

公式A中的一个约束个体变项△₁，可以用另一个体变项△₂进行替换。

替换必须在某特定量词及其辖域内处处进行。如果△₁在几个量词中都出现，那么，替换可以只在一个量词及其辖域中进行。

替换必须满足以下要求：

第一，△₂在A中不能是自由个体变项。

第二，如果△₂在A中约束出现，那么，被替换的△₁不能在以△₂为变项的量词之辖域中出现。

下例中列举的约束变项易字情况是正确的：

下例中列举的约束变项易字情况不正确：

6.定义置换规则

定义的左右两边可以互相置换。

（六）定理

谓词逻辑公理系统的推演方法和步骤，基本上与命题逻辑公理系统相同。

在现代逻辑中，人们常常把命题逻辑公理系统视为谓词逻辑公理系统的子系统。这样，前者中的所有定理也就都是后者中的定理。

所以，在构造谓词逻辑公理系统的过程中，可以把命题逻辑公理系统中的定理当作推演的依据。

以下介绍Q系统的部分定理及有关证明。其中，引用命题逻辑公理系统P的定理时仅注明“已证定理”。

定理1 ∀x(F(x)V┓F(x))

证明：

1 PVㄱP 已证定理

2 F(x)V┓F(x) 1，代入p/F(x)

3 q→(p→q) 已证定理

4 F(x)V┓F(x)→(pV┓p→F(x)V┓F(x))

3，代入q/F(x)V┓F(x)，p/pV┓p

5 pV┓p→F(x)V┓F(x) 4，2，分离规则

6 pV┓p→∀x(F(x)V┓F(x)) 5，后件概括规则

7 ∀x(F(x)V┓F(x)) 6，1，分离规则

导出规则1（概括规则）

在公式A(x)中，如果x自由出现，那么，可以推出∀xA(x)。

根据这条导出规则，可以把一个公式里的自由个体变项用全称量词约束起来。

定理2 ∀xF(x)→ヨxF（×)

证明：

1 ∀xF(x)→f(y) 公理

2 F(y)→ヨxf(x) 公理

3 ∀xF(x)→ヨxF(x) 2，1，已证定理

定理3 ∀x(F(x)ΛG(x))→∀xF(x)Λ∀xG(x)

证明：

1 ∀xF(x)→F(y) 公理

2 ∀x(F(x)ΛG(x))→F(y)ΛG(y)

1，代入F(△)/F(△)ΛG(△)

3 F(y)ΛG(y)→F(y) 已证定理

4 ∀x(F (x)ΛG (x)→F (y) 3，2，已证定理

5 ∀x(F(x)ΛG(x))→∀yF(y) 4，后件概括规则

6 ∀x(F(x)ΛG(x))→∀xF(x) 5，约束变项易字规则

7 F(y)ΛG(y)→G(y) 已证定理

8 ∀x(F(x)ΛG(x))→G(y) 7，2，已证定理

9 ∀x(F(x)ΛG(x))→∀yG(y) 8，后件概括规则

10 ∀x(F(x)ΛG(x))→∀xG(x)

9，约束变项易字规则

11 ∀x(F (x)ΛG (x))→∀xF(x)Λ∀xG(x)

6，10，已证定理

定理4 ∀xF(x)Λ∀xG(x)→∀x(F(x)ΛG(x))

证明：

1 ∀xF(x)→F(y) 公理

2 ∀xG(x)→G(y) 公理

3 ∀xF(x)Λ∀xG(x)→F(y)ΛG(y) 1，2，已证定理

4 ∀xF(x)Λ∀xG(x)→∀y(F(y)ΛG(y)) 3，后件概括规则

5 ∀xF(x)Λ∀xG(x)→∀x(F(x)ΛG(x)) 4，约束变项易字规则

定理5 ∀x(F(x)ΛG(x))↔∀xF(x)Λ∀xG(x)

该定理可以根据定理3、定理4的结果而得到。

定理6 ∀x(F(x)→G(x))→(∀xF(x)→∀xG(x))

此定理的逆命题不成立。

定理7 ∀x(F(x)↔G(x))→(∀xF(x)↔∀xG(x))

定理8 ∀xF(x)V∀xG(x)→∀x(F(x)VG(x))

此定理的逆命题不成立。

定理9 ヨxF(x)↔┓∀x┓F（x)

定理10 ヨx┓F(x)↔┓∀xF(x)

定理11 ┓ヨx┓F(x)↔∀xF(×)

定理12 ┓ヨxF(×)↔∀x┓F(×)

定理13 ∀x(F(x)→G(x))→(ヨxF(x)→ヨxG(x))

定理14 ∀x(F(x)↔G(x))→(ヨxF(x)↔ヨxG(x))

定理14的含义是：对于任何一个x而言，如果x是F等值于x是G，那么，存在x是F等值于存在x是G。

导出规则2（谓词演算基本置换规则）

谓词演算基本置换规则简称基本置换规则，它是定义置换规则的推广。其基本内容是：

假设A、B、A'和B'都是谓词演算的公式，并且，A'是A的子公式，即A公式包含A'。用公式B'取代A'在公式A中的一次或多次出现，得到公式B。如果

A'↔ B'

是可证公式，那么

A↔B

也是可证公式。

上述内容也可以粗略地表述为：在推导过程中，如果两个谓词演算的公式彼此等值，那么，可以把它们互相替换。

公理系统中引进谓词演算基本置换规则，可以使一些定理的证明过程明显得到简化。

定理15 ∀x(pVF(x))→pV∀xF(x)

定理16 pV∀xF（x)→∀x(pVF(x))

定理17 ∀x(pVF(x))↔pV∀xF(x)

定理18 ∀x(PΛF(x))→pΛ∀xF(x)

定理19 pΛ∀xF(x)→∀x(pΛF(x))

定理20 ∀x(pΛF(x))↔pΛ∀xF(x)

定理21 ∀x(p→F(x))↔(P→∀xF(x))

定理22 ∀x(F(x)→P)↔ヨxF(x)→P)

定理23 ∀x∀yR(x，y)↔∀y∀xR(x，y)

定理24 ヨx∀yR(x，y)→∀yヨxR(x，y)

证明：

1 F(y)→ヨxF(x) 公理

2 F(u)→ヨxF(x) 1，代入y/u

3 R(u，y)→ヨxR(x，y) 2，代入F(△)/R(△，y)

4 ∀y(R(u，y)→ヨxR(x，y)) 3，概括规则

5 ∀yR(u，y)→∀yヨxR(x，y) 4，定理6

6 ヨu∀yR(u，y)→∀yヨxR(x，y) 5，前件存在规则

7ヨx∀yR(x，y)→∀yヨxR(x，y) 6，约束变项易字规则

此定理的逆命题不成立。它表明：两个互相连接的不同量词不能任意交换。

定理25 ∀x∀yR(x，y)→∀xR(x，x)

以上，我们简略地介绍了谓词演算公理系统Q。从元逻辑的角度看，这一系统具有一致性和语义的完全性。

关于一致性，前面曾提过三种定义，即古典的、语法的和语义的。

Q系统是在古典的意义下一致的，即，不可能存在一个公式A，A和┓A都在该系统中可以被证明。

Q系统是语法一致的，即存在一个公式A，A在该系统中是不可证明的。

Q系统是语义一致的，即该系统的定理都是普遍有效式。

关于完全性，前面也曾提过三种定义，即古典的、语法的和语义的。

公理化谓词演算系统Q是语义完全的，即谓词逻辑中一切普遍有效的公式都是可以在Q系统中被证明的。

至于古典的完全性，即对任一公式A而言，或者A可证，或者┓A可证，这种完全性是针对着不包含自由变项的公式而言的，命题演算系统和谓词演算系统都不具有。

至于语法的完全性，即，如果把一个不可证的公式作为公理增加到已有公理之中，那么，相应系统就将是不一致的。这种完全性，命题演算公理系统P具有，而谓词演算公理系统Q不具有。