在数理逻辑中，谓词逻辑（Predicate logic）是符号形式系统的通用术语，比如一阶逻辑，二阶逻辑，多类逻辑或无穷逻辑等等。

In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic, or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified. Two common quantifiers are the existential ∃ ("there exists") and universal ∀ ("for all") quantifiers. The variables could be elements in the universe under discussion, or perhaps relations or functions over that universe. For instance, an existential quantifier over a function symbol would be interpreted as modifier "there is a function". The foundations of predicate logic were developed independently by Gottlob Frege and Charles Sanders Peirce.