# 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.^{}

In informal usage, the term "predicate logic" occasionally refers to first-order logic. Some authors consider the **predicate calculus** to be an axiomatized form of predicate logic, and the predicate logic to be derived from an informal, more intuitive development.^{}

Predicate logics also include logics mixing modal operators and quantifiers. See Modal logic, Saul Kripke, Barcan Marcus formulae, A. N. Prior, and Nicholas Rescher.