谓词演算(predicate calculus)
现代符号逻辑学的一部分，系统化证明涉及量词（如「所有」、「有些」）的谓词之间的逻辑关系。谓词演算通常建立在一些命题演算之上，并采用量词、自变数与谓词字元。命题形式「F所有东西不是G的就是H的」，符号表示为(@8(logicAll.jpgx)[Fx（Gx@8(logicOr.jpgHx）]。「F有些东西是G的也是H的」符号表示为(@8(logicSome.jpgx)[Fx@8(logicAnd.jpg(Gx@8(logicAnd.jpgHx)]。一旦基本命题形式的真假情况决定，演算内的命题分为三种互斥的类别：一、谓词符号的意义每个可能的规范都为真，如「每件东西是F或者不是F」；二、每个规范都为假，如「有些东西是F且不是F」；三、有些为真，其余为假，如「有些是F而且是G」。分别称为永真命题、不相容命题与偶然命题。特定的永真命题可能当作公理或是推论的基础。一阶（或是较低）谓词演算存在多重完备的公理化（「一阶」的意义是量词组合自变数，而非范围超过个别谓词的变数）。亦请参阅logic。
English version：
predicate calculus
Part of modern symbolic logic which systematically exhibits the logical relations between propositions involving quantifiers such as “all” and “some.” The predicate calculus usually builds on some form of the propositional calculus and introduces quantifiers, individual variables, and predicate letters. A sentence of the form “All F's are either G's or H's” is symbolically rendered as (∀x)[Fx (Gx ∨ Hx)], and “Some F's are both G's and H's” is symbolically rendered as (∃x)[Fx ∧ (Gx ∧ Hx)]. Once conditions of truth and falsity for the basic types of propositions have been determined, the propositions formulable within the calculus are grouped into three mutually exclusive classes: (1) those that are true on every possible specification of the meaning of their predicate signs, such as “Everything is F or is not F”; (2) those false on every such specification, such as “Something is F and not F”; and (3) those true on some specifications and false on others, such as “Something is F and is G.” These are called, respectively, the valid, inconsistent, and contingent propositions. Certain valid proposition types may be selected as axioms or as the basis for rules of inference. There exist multiple complete axiomatizations of first-order (or lower) predicate calculus (“first-order” meaning that quantifiers bind individual variables but not variables ranging over predicates of individuals). See also logic.