predicate logic



Predicate logic, also called first-order logic and sometimes abbreviated FOL, is the usual sort of logic used in the foundations of mathematics.

In contrast to 0th-order logic, we allow for variables in predicates bound by quantifiers. This means that the categorical semantics of 1st order logic is given by hyperdoctrines.

However, in contrast to higher-order logic, we do not allow variables that stand for predicates themselves. (This distinction can become somewhat confusing when the first-order theory in question is a material set theory, such as ZFC, in which the variables stand for “sets” which behave very much like predicates.)

A predicate calculus is simply a system for describing and working with predicate logic. The precise form of such a calculus (and hence of the logic itself) depends on whether one is using classical logic, intuitionistic logic, linear logic, etc; see those articles for details.

For many (perhaps most?) authors, predicate logic is really predicate logic with equality. However, some forms of predicate logic do not include an equality primitive, such as FOLDS (in whose name ‘FOL’ stands for ‘first-order logic’). In some first-order theories, such as ZFC, equality can be defined and so is not needed in the logic itself.


Lindström's theorems give important abstract characterizations of classical untyped first-order logic.



The syntax - semantics duality in first order logic is discussed in

On the historical development:

  • José Ferreirós, The Road to Modern Logic - An Interpretation , The Bulletin of Symbolic Logic 7 no. 4 (2001) pp.441-484. (draft)

From type theory

First order logic within type theory/homotopy type theory via propositions as types is discussed in

Last revised on November 1, 2014 at 21:38:41. See the history of this page for a list of all contributions to it.