谓词逻辑

又称“量词逻辑”。在命题逻辑的基础上，把原子命题进一步分析为个体词（相当于主词）、谓词和量词，以此研究命题的逻辑特征，命题间的逻辑关系特别是推导关系的逻辑演算理论。有狭义和广义之分。前者量词仅用于个体变元；后者量词也用于命题变元和谓词变元。

谓词逻辑

亦称量词逻辑。数理逻辑的基础部分。它是以命题逻辑为前提，进一步将简单命题分析为个体词、谓词和量词所组成，由此研究命题的形式结构、推理规则的逻辑演算理论。命题逻辑研究了一些有效的推理形式，但远远没有包括所有的有效推理式。例如，最古老的三段论推理，“凡人皆有死，苏格拉底是人，所以，苏格拉底有死”，它的两个前提和结论是三个不同的简单命题，用命题逻辑的手段只能将此推理形式处理为：p∧q→r。但这并不是命题逻辑的重言式。可见三段论的正确性在命题逻辑里得不到反映，更不说那些形式更为复杂的推理了，它们的正确性决定于谓词和量词的特征。谓词逻辑首先把命题中的个体和个体的性质以及个体间的关系区分开来，引进个体变项元如x,y,z等表示任意的不确定的个体，引进谓词变元如F,G,H等，用一元谓词如Fx、G(y)等表示个体的性质，用多元谓词如F(_x,y)、H(x,y,_z)等表示个体间的关系。然后，引进量词限定个体的数量和范围。量词共分二种：全称量词和存在量词，分别用∀和∃表示。使用量词、个体变元和谓词变元，就可以刻化简单命题的结构，如∀ xFx, ∀ x∃ y(x,y)等等。最后，再使用命题逻辑的联结词和命题变元，就可以表示复杂命题的结构，如∀_x (F(x)∨乛F(_x)),∀ xF(_x)∨p,∀ y∃ xF(x,y)→∃_x∀ yF(x,y)等等，像这样的公式通称为谓词表达式。
谓词逻辑把谓词表达式分为三种类型：普遍有效式，这类表达式反映了谓词逻辑的规律，它在每个符号的所有可能的规定意义下皆为真，例如，∀ x(F(_x)∨乛F(_x))，即对每一个事物来说或者具有F性质或者不具有F性质；不可满足式，这类表达式和普遍有效式相对立，反映了谓词逻辑中的逻辑矛盾，它在每个符号的所有可能的规定意义下皆为假，例如，∃_x(F(x)∧乛F(x))，即存在一事物既具有F性质又不具有F性质；可满足式是指对公式中每个符号至少在一种可能的规定意义下为真，例如，∃_xF(_x)∧∃_x乛F(x)，即存在一事物具有F性质同时又存在一事物不具有F性质。
谓词逻辑把所有的普遍有效式作为一个整体来研究。它构造一个公理系统，从公理出发，依据一定的推演规则，将所有的普遍有效式推演出来，并对这个公理系统的基本性质作出考查。这个公理系统以命题公理系统为前提，增加了两条形成规则：
（一）一谓词变元后继有写在一对括号内并用逗点分开的适当数目的个体变元是良构式。如F(x),G(_xy), H(x,y,z)。
（二）如x为一良构式，并且个体变元X在其中是自由变元，则∀xX和∃xX是良构式。如∀_xR(_x,z),∃_y (p∨ G(y))。增加了二条公理：
（一） ∀_xF(_x)→F(_y) 这条公理反映了从一般到个别的推理形式。
（二） F(_y)→∃_xF(_x) 这条公理反映了从个别到存在的推理形式。
对推演规则中的代入规则作了扩充和说明，使之适用于个体变元和谓词变元，并增加三条推演规则：
（一）后件概括规则，如果个体变元在A中不出现，从推出A→B(_x)可得A→∀_xB(x)。
（二）前件存在规则，如果个体变元在B中不出现，从推出A(_x)→B可得∃_xA(_x)→B。
（三）约束个体变元易字规则，一公式中的约束个体变元x可由另一个体变元y替换，替换必须在一特定量词及其辖域内到处实现。
从公理出发，借助上面的推演规则，谓词逻辑可以进行一系列的推导。推导的过程纯粹是符号序列的变换，而不涉及符号的任何意义。凡推导出来的定理都反映了逻辑的规律，都表现为普遍有效式。
谓词演算公理系统满足一致性的要求，在这个系统里不可能有一表达式A, A和乛A都在系统里可证。由此可知，谓词演算的定理都是普遍有效式。但这个有效性定理的证明却不是能行的，因为谓词表达式所涉及的个体的数目是无穷的，没有一种能行的方法可以确定其赋值系。但对于有穷域，对任一给定的整数K (K≥1)，可以通过赋值的方法，能行地证明谓词演算的定理都是K普遍有效的。
谓词演算公理系统满足完全性的要求，即凡是普遍有效式在这个系统中都是可证的，这又等于说，对任一谓词表达式A，或者A在系统中可证，或者乛A是可满足的。在证明过程中，以斯科伦范式为中介，通过全能赋值系和数学归纳的方法，证明了对任一斯科伦范式，或者它本身在系统中可证，或者它的否定可满足，而每一谓词表达式与它的斯科伦范式是可以互推的。这个完全性定理的证明，是哥德尔于1929年完成的。
谓词逻辑在以下几个问题上是不能判定的：
（一）任一谓词表达式是否可证，是否为一定理。
（二）任一谓词表达式是否普遍有效。
（三）任一谓词表达式是否可满足。
谓词逻辑没有一种能行的方法，不能用事先给定的规则决定应该引用哪些推演规则，如何用法以及引用的机械次序来解决这几个问题。因此，从总体上说谓词逻辑是不能判定的，尽管它也解决了一些具体的判定问题。
上述的谓词演算系统称为一阶谓词逻辑或狭谓词逻辑，因为它只对个体变元使用量词，而不对谓词变元和命题变元使用量词。如果也对谓词变元和命题变元使用量词，由此构成的逻辑系统称为高阶谓词逻辑或广义谓词逻辑。