Impredicative

Definition

A definition is impredicative if it refers to a collection or totality that includes the thing being defined. In other words, an impredicative definition defines an object by quantifying over a domain that contains that object itself.

The term comes from the Latin praedicere (to declare beforehand). An impredicative definition fails to “declare beforehand” because it presupposes the existence of the thing it defines.

Examples

Power Set

The Power Set $\mathcal{P}(A)$ of a set $A$ is defined as the set of all subsets of $A$:

$\mathcal{P}(A)=\{B\mid B\subseteq A\}$

This definition is impredicative because $\mathcal{P}(A)$ itself is a subset of some larger set, and the definition quantifies over “all subsets,” which includes $\mathcal{P}(A)$ in certain set-theoretic frameworks.

Real Numbers as Dedekind Cuts

Defining real numbers as Dedekind cuts involves quantifying over all subsets of rationals. Since the real numbers themselves can be viewed as living in a space constructed from such subsets, this definition has impredicative character.

Russell’s Paradox

The most famous example of problematic impredicativity is Russell’s Paradox. Consider:

$R=\{x\mid x\notin x\}$

The set of all sets that do not contain themselves. Asking whether $R\in R$ leads to contradiction, demonstrating that unrestricted impredicative definitions can be inconsistent.

Least Upper Bound

In analysis, the least upper bound (supremum) of a set $S\subseteq \mathbb{R}$ is defined as:

$\sup (S)=\min \{u\in \mathbb{R}\mid \forall s\in S.s\le u\}$

This definition quantifies over all real numbers, including the supremum itself, making it impredicative.

Impredicativity in Type Theory

In Type Theory, impredicativity typically appears in the treatment of universal quantification and polymorphism.

Impredicative Polymorphism

System F (polymorphic lambda calculus) features impredicative polymorphism. A term of type $\forall \alpha .\tau$ can be instantiated at any type, including types that themselves involve $\forall$. For example:

$(\Lambda \alpha .t):\forall \alpha .\alpha \to \alpha$

can be applied to $\forall \beta .\beta \to \beta$, creating an instance that refers to the very collection it belongs to.

Impredicative Prop

In the Calculus of Constructions and similar systems, the universe of propositions (Prop) is often impredicative. This means:

$\text{Prop}:\text{Type},\forall (P:\text{Prop}).Q:\text{Prop}$

A proposition can quantify over all propositions, including itself.

Predicative Type Theories

Predicative type theories (like Martin-Löf Type Theory without impredicative Prop) avoid impredicativity by stratifying universes:

${\text{Type}}_0:{\text{Type}}_1:{\text{Type}}_2:\cdots$

A type at level $n$ can only quantify over types at levels $<n$.

Historical Context

Poincaré and Russell

Henri Poincaré and Bertrand Russell identified impredicative definitions as a source of logical paradoxes in the early 20th century. They proposed the vicious circle principle: no object or property should be defined in terms of a totality to which it belongs.

Predicativism

The predicativist program, championed by Hermann Weyl and others, sought to rebuild mathematics using only predicative definitions. This proved too restrictive for much of classical mathematics, particularly analysis.

Ramified Type Theory

Russell’s ramified type theory introduced orders of quantification to eliminate impredicativity, but this made mathematics cumbersome. The axiom of reducibility was added to recover classical mathematics, essentially reintroducing impredicativity.

Constructive Mathematics

In Constructive Mathematics, opinions on impredicativity vary:

• Classical mathematics: Embraces impredicativity freely (e.g., in ZFC)
• Predicative mathematics: Rejects impredicativity entirely
• Semi-constructive approaches: Accept limited forms of impredicativity (e.g., impredicative Prop in Coq)

Some constructivists reject impredicativity on philosophical grounds: an impredicative definition seems to presuppose what it defines, violating constructive principles.

Practical Implications

In Proof Assistants

Different proof assistants make different choices:

• Coq: Has an impredicative Prop universe
• Agda: Fully predicative by default
• Lean: Offers both predicative and impredicative modes

The choice affects:

• Which definitions are expressible
• Computational behavior
• Consistency strength
• Proof relevance

Computational Content

Impredicative quantification often lacks computational content. In Coq, terms in Prop cannot be extracted to executable code, partly because impredicativity makes computation unclear.

Consistency Considerations

Impredicativity does not automatically lead to inconsistency:

• ZFC is impredicative but believed consistent
• System F is impredicative but strongly normalizing
• The Calculus of Constructions is impredicative but consistent

However, unrestricted impredicativity (as in naive set theory) combined with other powerful principles can lead to paradoxes.

Related Concepts

• Predicative: Definitions avoiding self-reference to totalities
• Russell’s Paradox: Famous inconsistency from unrestricted impredicativity
• Type Theory: Framework where predicativity choices matter
• System F: Type system with impredicative polymorphism
• Calculus of Constructions: Type theory with impredicative Prop
• Constructive Mathematics: Where impredicativity is often questioned
• Universe: Stratification mechanisms for controlling impredicativity
• Set Theory: Classical impredicative foundation of mathematics