nLab predicate logic

Idea

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, first-order logic admits variables in predicates bound by quantifiers (“for all” $\forall$ and “there exists $\exists$).

(This means that the categorical semantics of 1st order logic is given by hyperdoctrines.)

However, in contrast to higher-order logic, first-order logic does 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.

Typed predicate logic may be called first-order logic over type theory. Typed predicate intuitionistic logic is often identified with the internal logic of a Heyting category, while typed predicate classical logic is often identified with the internal logic of a Boolean category. Any untyped predicate logic could be thought of as a simply typed predicate logic with only one type $V$, known as the domain of discourse or the universe of discourse.

For many (perhaps most?) authors, predicate logic is really predicate logic with equality. That means that one predicate symbol with two arguments $=(x,y)$ (also written $x=y$) is distinguished, and has to satisfy reflexivity, symmetry, transitivity and the rule of substitution: $(x = y \wedge \phi(x))\implies \phi(y)$ for any predicate $\phi$ with one argument. 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.

In constructive mathematics, one could also have a predicate logic with apartness, which has one predicate symbol with two arguments $\#(x,y)$ (also written $x\#y$) is distinguished, and has to satisfy irreflexivity, symmetry, and comparison. By definition of an apartness relation, its negation is an equivalence relation, which we could take to be equality $x = y \coloneqq \neg(x \# y)$ satisfying the rule of substitution: $(\neg(x \# y) \wedge \phi(x))\implies \phi(y)$ for any predicate $\phi$ with one argument. This makes the domain of discourse into an apartness space.

Properties

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

Related concepts

• logic

  • propositional logic (0th order)

  • predicate logic (1st order)

  • second-order logic

  • higher-order logic

  • predicate logic as a dependent type theory

  • rule C

• first-order set theory

• type theory

• Lindström's theorem

References

General

Textbook accounts:

In view of the Curry-Howard correspondence:

• Morten Heine Sørensen, Pawel Urzyczyn, §9 of: Lectures on the Curry-Howard isomorphism, Studies in Logic 149, Elsevier (2006) [ISBN:9780444520777, pdf]

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

• Steve Awodey, Henrik Forssell, First-Order Logical Duality .(arXiv:1008.3145)

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

• Univalent Foundations Project, section 3 of Homotopy Type Theory – Univalent Foundations of Mathematics