谓词，在谓词逻辑中，原子命题分解成个体词和谓词。 个体词是可以独立存在的事或物，包括现实物、精神物和精神事三种。谓词则是用来刻画个体词的性质的词，即刻画事和物之间的某种关系表现的词。如“苹果”是一个现实物个体词，”苹果可以吃”是一个原子命题，“可以吃”是谓词，刻画“苹果”的一个性质，即与动物或人的一个关系。

形式逻辑的最根本部分，也是最基本的逻辑系统或理论。在谓词逻辑中，除研究复合命题的命题形式、命题联结词的逻辑性质和规律外，还把命题分析成个体词、谓词和量词等非命题成分，研究由这些非命题成分组成的命题形式的逻辑性质和规律。谓词逻辑把命题逻辑作为子系统，但为了研究方便，同时也由于它具有某些重要的特殊性质，命题逻辑通常又作为一个独立的系统先研究，而在谓词逻辑部分则集中研究由非命题成分组成的命题形式和量词的逻辑性质与规律。只包含个体谓词和个体量词的谓词逻辑称为一阶谓词逻辑，简称一阶逻辑，又称狭义谓词逻辑。此外，还包含高阶量词和高阶谓词的称为高阶逻辑。谓词逻辑也分为经典的谓词逻辑和非经典的谓词逻辑，后者包括作为子系统的非经典的命题逻辑。经典的一阶谓词逻辑是谓词逻辑的基本部分。第一个完整的谓词逻辑系统是G.弗雷格在1879年建立的。K.哥德尔等人系统地研究了谓词逻辑的元逻辑问题，证明了重要的定理。

个体词分个体常项(用a,b,c,…表示)和个体变项(用x,y,z,…表示)；谓词分谓词常项(表示具体性质和关系)和谓词变项(表示抽象的或泛指的谓词)，用F,G,P,…表示.

注意，单独的个体词和谓词不能构成命题，将个体词和谓词分开不是命题.

量词，是在命题中表示数量的词，量词有两类：全称量词（∀），表示“所有的”或“每一个”；存在量词（∃），表示“存在某个”或“至少有一个”.

在谓词逻辑中，使用量词应注意以下几点：

(1) 在不同个体域中，命题符号化的形式可能不同，命题的真值也可能会改变.

(2) 在考虑命题符号化时，如果对个体域未作说明，一律使用全总个体域.

(3) 多个量词出现时，不能随意颠倒它们的顺序，否则可能会改变命题的含义.

谓词公式只是一个符号串，没有什么意义，但我们给这个符号串一个解释，使它具有真值，就变成一个命题. 所谓解释就是使公式中的每一个变项都有个体域中的元素相对应.

在谓词逻辑中，命题符号化必须明确个体域，无特别说明认为是全总个体域。一般地，使用全称量词”，特性谓词后用®；使用存在量词$，特性谓词后用Ù.

h谓词公式，由原子公式、联结词和量词可构成谓词公式(严格定义见教材). 命题的符号化结果都是谓词公式.

例如”x(F(x)®G(x))，(F(x)ÙG(x))，”x”y(F(x)ÙF(y)ÙL(x,y)®H(x,y))等都是谓词公式.

h变元与辖域，在谓词公式”xA和中，x是指导变元，A是相应量词的辖域. 在”x和的辖域A中，x的所有出现都是约束出现，即x是约束变元，不是约束出现的变元，就是自由变元. 也就是说，量词后面的式子是辖域. 量词只对辖域内的同一变元有效.

h换名规则，就是把公式中量词的指导变元及其辖域中的该变元换成该公式中没有出现的个体变元，公式的其余部分不变.

h代入规则，就是把公式中的某一自由变元，用该公式中没有出现的个体变元符号替代，且要把该公式中所有的该自由变元都换成新引入的这个符号.

h解释(赋值)，谓词公式A的个体域D是非空集合，则

(1) 每一个常项指定D中一个元素；

(2) 每一个n元函数指定Dn到D的一个函数；

(3) 每一个n元谓词指定Dn到{0,1}的一个谓词；

按这个规则做的一组指派，称为A的一个解释或赋值.

在有限个体域下，消除量词的规则为：如D={a1,a2,…,an}，则

h谓词公式分类，在任何解释下，谓词公式A取真值1，公式A为逻辑有效式(永真式)；在任何解释下谓词公式A取真值0，公式A为永假式；至少有一个解释使公式A取真值1，公式A称为可满足式.

最简单的命题，即所谓原子命题，都可以分析为个体词和谓词两类成分。例如，在“5是素数”、“7大于3”这两个命题中，5、7和 3是个体词，“是素数”、“大于”是谓词。在逻辑中，一个论域中的元素称为个体，个体词是表示个体的符号；表示某个论域中的一个特定个体的符号称为个体常项或个体常元，个体常项也就是它所表示或指称的那个个体的名字；不表示某一确定论域中的特定个体的个体词，称为个体变项或个体变元，用符号x,y,z和x1,y1,z1,…表示；个体变项取任一论域中的任一个体为值。谓词是表示个体的性质和个体之间关系的符号。个体的性质也称一元关系，表示个体的性质即一元关系的称为一元谓词。两个个体之间的关系称为二元关系，n个个体之间的关系称为n元关系。表示二元关系的为二元谓词，表示 n元关系的为 n元谓词。如“是素数”就是一元谓词，“大于”是二元谓词,“在…之间”是三元谓词。表示某一论域中的特定的性质或关系的称为谓词常项或谓词常元,“是素数”等都是谓词常项。不表示某一确定论域中的特定性质或关系的称为谓词变项或谓词变元。谓词变项用符号F,G,H和F1，G1，H1，…表示。谓词变项也分为一元的、二元的、…,n元的，等等。谓词变项的元数可以明晰地标示出来，如F1表示F是一元的，G2表示G是二元的，但也可以不这样做。在一公式中，一个谓词变项后面跟的个体变项的个数,就表示这个谓词变项的元数。例如，F(x)中F是一元的，G(x,y)中G是二元的，H(x1,x2,…,xn)中H是n元的。同一个符号，比如F，在不同的公式中可以表示不同元数，但在一个复杂的公式中，同一符号的几处出现是同一个谓词变项。应用个体变项和谓词变项,“5是素数”、“7大于3”这两个原子命题的形式可分别表示为F(x)和G(x,y)这两个公式。一般地陈述n个个体间有某关系的原子命题的形式，用一个 n元谓词变项后面跟n个个体变项的公式表示,该公式为: F(x1,x2,…,xn)。表示原子命题的形式的公式称为原子公式。

除了个体词和谓词，组成命题的成分还有量词。量词是命题中表示数量的词，它分为全称量词和存在量词。例如，在“所有阔叶植物是落叶植物”、“有的水生动物是肺呼吸的”这两个命题中的“所有”、“有的”都是量词,其中前者是全称量词,后者为存在量词。在汉语中,“所有”、“一切”、“凡”等表示全称量词,“有的”、“有”、“至少有一”等表示存在量词。全称量词是在符号∀后跟一个个体变项(比如x),表示为(∀x)，读作：“对任一x”，“所有x”。存在量词在符号ヨ后跟一个个体变项（比如x），表示为(ヨx)，读作：“有一x”，“存在一x”。在一个公式前面加上量词，称为量化式,如(∀x)F(x)和(ヨx)F(x)，就分别称为全称量化式和存在量化式。(∀x)F(x)表示“所有x，x是F,即一切事物都是F”；(ヨx)F(x)表示“有一x,x是F,即有一事物是F”。

从原子公式出发，应用量词和命题联结词┓、∧、∨、→和↔就可以构造出表示各种复杂的命题形式的公式。

例如，“所有阔叶植物是落叶植物”这一命题形式的公式为：(∀x)(F(x)→G(x))； “有的水生动物是肺呼吸的”这一命题形式的公式为：(ヨx)(F(x)∧G(x))。 “一切自然数有大于它的自然数”、“每人都有一个父亲”这类命题，具有更复杂的公式，即：(∀x)(F(x)→(ヨy)(F(y)∧G(x,y))) 谓词逻辑中的这种命题形式比命题逻辑更为复杂，其数量也非常多，相应的公式的数目是无穷的。公式的解释 　谓词逻辑的公式可以分为普遍有效的、可满足的和不可满足的三类。普遍有效的公式表达谓词逻辑的规律。为了刻划公式的普遍有效性和可满足性，首先需要说明对公式的解释。一个解释由一个非空个体域D和一个赋值υ组成，对每一个体变元x,υ都赋与D中的一个个体为值，如果对个体变元 x1,x2,…,xn,υ分别赋以D中的个体 a1,a2，…,an为值，υ对个体变元的n元组（x1,x2,…,xn）所赋之值即为(a1,a2,…,an)；对n元谓词变元 F，υ赋与F的值是D中的一个n元关系。令A为一个原子公式 F(x1,x2,…,xn)，υ(A)即υ【F(x1,x2,…,xn)】的值可以为1(即真)，也可以为0（即假）。如果 (x1,x2,…,xn)所赋之值 (a1,…,an)属于F所赋之值，υ(A)的值为1,否则为0。υ(A)的值为 1，也就是公式A在此解释下是D中的真命题。每一赋值 υ也给出一个真值赋值。令A、B是任意的公式。υ(┓A)的值为1,当且仅当υ(A)的值为0。υ(A∧B)的值为1,当且仅当υ(A)和υ(B)的值都为1。υ(A∨B)的值为1,当且仅当υ(A)或υ(B)的值为1。υ(A→B)的值为1, 当且仅当υ(A)的值为0或υ(B)的值为1。υ(A↔B)的值为1，当且仅当υ(A)和υ(B)的值相同。 υ(∀x)A(x)的值为1，当且仅当，设A的赋值已经给定, 对每一D中的个体a，A(a)的值为1，即(∀x)A(x)是真的，当且仅当, 设A的赋值已给定，对于D中的每一个体 a，A(a)真。υ(ヨx)A(x)的值为1, 当且仅当, 设A的赋值已给定, 有 D中的个体a，使得A(a)的值为1。 　一个公式 A称为可满足的，如果有一不空的个体域D和赋值υ，在此解释下，A为真。

一个公式 A称为普遍有效的，如果对任一解释，也就是对任一不空的个体域和任一赋值，A都真。A普遍有效也就是A常真，记为FA。 　显然，一个公式 A是普遍有效的，当且仅当，它的否定┓ A是不可满足的。一个不可满足的公式是常假的，也称为矛盾的。 　这里所说的个体域、解释、赋值、真假、普遍有效性和可满足性等概念，都是语义概念。

谓词逻辑的普遍有效的公式为数无穷，在一定意义上它们都是逻辑规律。为了系统地研究这类规律,需要对它们作整体的考虑，将它们总括在一个系统之中。谓词演算或者一阶谓词演算就是这样的系统。谓词演算是把谓词逻辑公理化和形式化而建立的形式系统。按照对作为演算出发点的初始符号、公理和变形规则的不同挑选，可以建立不同的谓词演算系统。在初始符号中有符号=的，称为带等词的一阶谓词演算，等词=是一个谓词常元；不带等词的系统就称为（一阶）谓词演算。构成一个谓词逻辑的公理系统的基本要素有：初始符号、形成规则、公理和变形规则等。对此，可以从一个不带等词的系统 F得到说明。 F的初始符号，包括个体变元、谓词变元、联结词和量词以及技术性符号四类。个体变元符号的小写拉丁字母为： x,y,z,x1,y1,z1,x2,…；谓词变元符号为大写拉丁字母，即：F,G,H,F1,G1,…。在原则上,对每一n≥1，应分别列出n元谓词变元，如：F1,G1,H1,…;F 2,G 2,H 2,…；等等。不过,省去上标1,2,…,n，在实践上不会产生混乱。联结词和量词符号为：┓、→、∀；技术性符号为括弧（，）和逗号，。

形成规则规定怎样的符号序列或符号的组合是 F中的合式公式。合式公式经解释后是有意义的。用来描述和讨论 F系统的语言即元语言的符号有：小写希腊字母α，α1，…,αn，δ表示任意的个体变元；fn表示任意的n元谓词变元;大写拉丁字母X,Y表示任意的符号序列。这些符号称为语法变元。F的形成规则有4条：①如果fn是一n元谓词变元,α1,…,αn是个体变元，则fn(α1,…,αn)是一合式公式；

②　如果 X是合式公式，则┓X是合式公式。如果X、Y 是合式公式，则(X→Y)是合式公式；

③　如果X是合式公式，α是个体变元，则(∀α)X是合式公式；

④　只有适合以上①～③的是合式公式。合式公式简称公式。用字母A,B,C表示任意的公式。A,B,C也是语法变元，属于元语言。

量词的辖域指一量词后的最短公式，表示一个量词在一个公式中的作用范围。例如，在公式 (∨y)【(∀x)F(x)→G(y)】中，(∀x)的辖域是公式F(x)，(∀y)的辖域是公式【(∀x)F(x)→G(y)】。 变元α在一个公式A中的某次出现是约束出现，如果α的这次出现是在(∀α)中或（∀α）的辖域中；α在一公式 A中的某次出现是自由出现，如果α在A中的这次出现不是约束的。例如，在公式(∀y)【∀(x)F(x)→G(y)】中， x和y的两次出现都是约束的；在公式【(∀x)F(x)→G(y)】中,x的两次出现是约束的，y的一次出现是自由的。个体变元α可以在A中既有约束出现又有自由出现， 例如， (∀α)F(x)→G(x)。如果个体变元α在A中自由或约束出现，它在A中就是自由或约束出现的。δ对A(α)中的α是自由的， 如果在A(α)中α的自由出现不在(∀δ)的辖域中。

F的公理有无穷多条，并由5个公理图式给出，每个图式都代表无穷多条公理。公理图式用语法变元陈述这5个公理图式是：

① A→(B→A);

② 【A→(B→C)】→【(A→B)→(A→C)】;

③ (┓A→┓B)→(C┓A→B→A);

④ (∀α)(A→B)→【A→(∀α)B】，如果α在A中没有自由出现。

⑤ (∀α)A(α)→A(δ)，如果δ对A(α)中的α是自由的。

该图式的A(α)是一合式公式，α是在其中有自由出现的个体变元，A(δ)则是用δ代替α在A(α)中的每处自由出现而得的公式。

根据④以下的公式都是公理：

(∀x)【F(y)→G(x,y)】→【F(y)→(∀x)G(x,y)】;

(∀x)【(∀x)F(x)→F(y)】→【(∀x)F(x)→(∀y)F(y)】。

但公式(∀x)【F(x)→G(x,y)】→【F(x)→(∀x)G(x,y)】却不是公理，因为它不符合图式④中关于 x在F(x)中没有自由出现的规定。

根据图式⑤，以下的公式都是公理：

(∀x)F(x)→F(y);

(∀y)G(y)→G(y);

(∀x)F(x,y)→F(y,y);

(∀y)【F(y)→G(x,y)】→【F(y)→(∀y)G(y,y)】。

但 (∀x) 【F(x)→(∀y)G(x,y)】→【F(y)→(∀y)G(y,y)】不是公理。因为该公式的y对F(x)→(∀y)G(x,y)中的x不是自由的，不符合图式⑤的条件。

变形规则也称推理规则。变形规则的陈述，除使用语法变元，还使用语法符号├。符号├在一个公式的前面，表示紧接在├后面的公式是定理。例如，├A,表示A是定理。F的变形规则有两条，即：①分离规则，从A和A→B，可以推出B；②概括规则，从A，可以推出(∀α)A。

F中的一个证明，指一有穷公式序列A1,A2, …, An，其中的每一Ak(k=1,2,…,n)或者是一个公理，或者是由公式Ai和 Aj（i,j＜k，且j=Ai→Ak）应用分离规则而得，或者是由公式Aj(j＜k)应用概括规则而得，即Ak=(∀α)Aj。一个证明也可以说是此证明的最后一个公式的证明。 F中的一个公式 B是F的定理，如果B有一个证明，或者说，存在一个证明 A1,A2,…，An，这个证明的最后一个公式An即是 B。根据这个定义，每一公理都是定理，即单独一个公理构成自身的一个证明。一个公式 B，如果存在它的一个证明,就说B是可证明的。一个公式是定理，当且仅当它是可证明的。 一个公式B是由公式A1,A2,…,Am可推演的，记作：A1,A2,…,Am├B。如果存在一个公式的有穷序列 C1,C2,…,Cn，其中每一 Ck(k=1,…,n)或者是一公理, 或者是A1,…,Am中的一个，或者是由Ci、Cj(i、j＜k，且j=Ci→Ck)应用分离规则而得，或者是由Cj(j＜k)应用概括规则而得，并且Cn是B。如m=0，则├B当且仅当B是一定理。

F 的初始符号中不包括∧、∨、↔、ヨ这几个符号,但它们可以通过定义引入，即：

(A∨B)定义为(┓A→B)；

(A∧B)定义为┓(A→┓B)；

(A↔B)定义为(A→B)∧(B→A)；

(ヨα)A定义为┓(∀α)┓A。

关于谓词演算F，只涉及符号、符号序列、符号序列的变换等等，完全没有涉及符号、公式等的意义。这种不涉及符号、公式等的意义的研究，是语法的研究。定理、可证明性等概念，都是语法概念。而对符号、公式的解释，以及关于公式和它的意义的关系等等，都属于语义的研究。关于 F的解释称为标准解释或标准语义。在这个标准解释下，F的公理图式以及公理本身都是普遍有效的，而变形规则具有保持普遍有效性的性质，即从普遍有效的公式经应用变形规则而得到的公式也是普遍有效的。所以，F的定理都是普遍有效的。

F有许多元逻辑定理或称元定理。不过元定理并不是F中的定理，而是关于F的定理，是对F这个系统的某些重要性质的研究的结果。重要的元定理有 3个：

①可靠性定理，表述为：如果├A，则╞A。这条定理表明F的定理都是普遍有效的。

②　一致性定理。这条定理表明 F是一致的，即不存在一个公式A，A和┓A都是定理。

③　完全性定理，它表述为：如果╞A，则├A。该定理表明，F在凡普遍有效的公式都是定理这一意义上是完全的。

可靠性定理表明，谓词演算 F对演绎推理形式的反映是可靠的。设A是一个推理的前提的命题形式，B是结论的命题形式，这个推理的形式就是 A→B。F的定理都是普遍有效的，这就意味着F只反映有效的推理形式。而完全性定理则表明，F对有效推理的形式的反映是完全的。设A→B是一个有效的推理的形式,当A真时B一定真,A→B是普遍有效的，因而是F的定理。这两个定理也表明，对F来说，语法和语义是一致的、相符合的。也就是说,可证明性和普遍有效性是相符合的，一个公式是可证明的或是定理，当且仅当它是普遍有效的。

除了 F这样的形式系统，谓词逻辑还可用另一种方式系统化，即建立自然推理系统。例如，有一个与 F相应的自然推理系统，其初始符号和形成规则与F相同。在该系统的规则中，A、B是任意公式，A(α)、A(δ)也和F中所说明的一样，它所使用的大写希腊字母Γ、△表示公式的集合，语法符号├表示前提和结论之间的推理关系，├左边的公式（公式集合）是前提，右边的公式是结论。这个自然推理系统有7条推演规则，它们分别是：

(ε)A1,…,An├Ai(i=1,…,n)。这是肯定前提规则；

(τ)如果Γ├Δ├（Δ不空），则Γ├A。这是演绎推理传递规则；

(┓-)如果Γ，┓A├B，并且Γ，┓A├┓B，则Γ├A。这是否定词消去规则；

(→-)A→ B，A├B。这是蕴涵词消去规则；

(→+)如果Γ，A├B，则Γ├A→B。它是蕴涵词引入规则；

(∀-)(∀α)A(α)├A(δ)，这是全称量词消去规则；

(∀+)如果Γ├A(α)，α在 Γ中的公式中没有自由出现，则Γ├(∀α)A(α )。这是全称最词引入规则。

规则(τ)表示，从Γ能推出Δ，从Δ能推出A，则从Γ能推出A，推出关系是传递的。规则(┓-)也称反证律。在这一自然推理系统中，符号∨、∧、↔和ヨ也可以通过定义引入，并导出相应的规则。

关于这个自然推理系统，有如下的结果：如果 A普遍有效，即╞A，则├A；并且，如果├A，则A普遍有效。在 F和这个自然推理系统之间，有如下关系：对任一公式A，如果A在F中可证，即├A，则├A；反之，如果A在自然推理中不需任何前提就能推出，即├A，则 A在F中可证。这个自然推理系统也和 F一样具有可靠性、一致性和完全性。

胡世华、陆钟万：《数理逻辑基础》,科学出版社,北京，1981（上册），1982（下册）。 　莫绍揆：《数理逻辑教程》，华中工学院出版社，武汉，1983。