Comprehension

Idea

Comprehension is the general principle that a predicate $\varphi$ determines a collection of all objects satisfying $\varphi$. It is one of the most natural ideas in mathematics — one constantly forms sets such as “the set of all even numbers” or “the set of all groups of order $p$” — but its naive formulation leads directly to contradiction.

The history of set theory is largely the history of finding principled restrictions on comprehension that avoid paradox while retaining enough expressive power for mathematics.

Unrestricted Comprehension

The unrestricted comprehension scheme asserts that for any predicate $\varphi$, there is a set of all objects satisfying it: $\forall \varphi .\exists S.\forall x.(x\in S⟺\varphi (x)).$

This is the principle underlying Frege’s logical system. It is maximally expressive: any definable collection is a set. However, it is inconsistent.

Setting $\varphi (x)\equiv x\notin x$ yields the Russell set $R=\{x\mid x\notin x\}$, from which one derives $R\in R⟺R\notin R$, a contradiction. This is Russell’s Paradox.

Restricted Comprehension (Separation)

The most common resolution, adopted in Zermelo-Fraenkel set theory, is to permit comprehension only within an existing set. The axiom schema of separation (also called restricted comprehension or Aussonderung) states: $\forall X.\forall \varphi .\exists S.\forall x.(x\in S⟺x\in X\wedge \varphi (x)).$

The set $S$ is written $\{x\in X\mid \varphi (x)\}$. Separation is safe because it never produces a set larger than $X$: one cannot form the Russell set, since that would require ranging over all sets.

Separation alone does not construct new large sets; it only carves out subsets of existing ones. The other axioms of ZF (pairing, union, power set, infinity, replacement) supply the sets from which separation draws.

The Role of Replacement

Separation allows the formation of subsets defined by a predicate. The axiom schema of replacement extends this: if $\varphi (x,y)$ defines a class function on a set $A$ (each $x\in A$ maps to a unique $y$), then the image $\{y\mid \exists x\in A.\varphi (x,y)\}$ is a set. Replacement is strictly stronger than separation: it can produce sets not obtainable by separation alone (e.g. $\omega +\omega$, $V_{\omega +\omega }$).

Comprehension in NBG

In von Neumann–Bernays–Gödel (NBG) set theory, classes are first-class objects alongside sets. NBG retains a comprehension principle for classes: $\forall \varphi .\exists C.\forall x.(x\in C⟺\varphi (x)),$ where $C$ is a class (which may or may not be a set). The paradox is avoided because classes, unlike sets, may not be elements of other classes. The Russell class $\{x\mid x\notin x\}$ exists in NBG as a proper class, but the derivation of the paradox requires forming $R\in R$, which is not permitted since $R$ is not a set.

NBG thus restores something close to the original comprehension principle, but stratified: predicates determine classes, and classes that are “too big” to be sets are proper classes.

Comprehension in Type Theory

In type theory, an analogue of comprehension is available via subset types or $\Sigma$-types: $\Sigma x:A.P(x)$ is the type of pairs $(x,p)$ where $x:A$ and $p:P(x)$. This is always well-formed and does not lead to paradox, because the domain $A$ must be specified in advance. The type-theoretic analogue of unrestricted comprehension — forming a type of all types satisfying a predicate — is avoided; a universe $\mathcal{U}$ is never a member of itself, ruling out the analogue of Russell’s paradox (Girard’s Paradox).

In Category Theory

Fixing a there is a functor from Pred to Set:

$$\{-\}:\mathbf{Pred}\Rightarrow \mathbf{Set}$$

Related Concepts

• Russell’s Paradox
• Set Theory
• Replacement (Set Theory)
• Axiom of Foundation
• Class (Set Theory)
• Subset
• Predicate
• Tarski Universe