Predicate Logic

Overview

Predicate logic is a logical system that uses quantified variables over non-logical objects. A predicate is a sentence with some number of free variables.

A predicate with free variables "plugged in" is a proposition.

Quantification

A quantifier refers to an operator that specifies how many members of a set satisfy some formula. The most common quantifiers are $\mathrm{\exists }$ and $\mathrm{\forall }$, though others (such as the counting quantifier) are also used.

Existentials

Existential quantification ($\mathrm{\exists }$) asserts the existence of at least one member in a set satisfying a property.

Uniqueness

We can also denote existence and uniqueness using $\mathrm{\exists }!$. For example, $\mathrm{\exists }!x,P(x)$ indicates there exists a unique $x$ satisfying $P(x)$, i.e. there is exactly one $x$ such that $P(x)$ holds:

The first conjunct denotes existence while the second denotes uniqueness.

Counting

Counting quantification (${\mathrm{\exists }}^{=k}$ or ${\mathrm{\exists }}^{\ge k}$) asserts that (at least) $k$ (say) members of a set satisfy a property.

Universals

Universal quantification ($\mathrm{\forall }$) asserts that every member of a set satisfies a property.

Identifiers

Identifiers are said to be bound if they are parameters to a quantifier. Identifiers that are not bound are said to be free. A first-order logic formula is said to be in prenex normal form (PNF) if written in two parts: the first consisting of quantifiers and bound variables (the prefix), and the second consisting of no quantifiers (the matrix).