What is predicativity?

Question

Type systems, and the proof assistants based on them, are frequently divided into predicative and impredicative.

What exactly does this mean? I've heard the slogan "impredicativity means you can't quantify over things you haven't defined yet", but I don't know how to apply this definition to a type system.

---

Predicativity is mentioned here in this answer to this question. I don't really understand predicativity and don't understand how the concept in a classical setting lines up with or doesn't line up with the concept in a proof assistant setting.

This question form the Mathematics Stack Exchange and its answer describe what predicativity is when applied to the axiom schema of separation in ZFC.

I'll do something a little nonstandard in the notation and always split the variable intepretations fed to $\varphi(\vec{p}; \vec{x})$ into parameters $\vec{p}$ and ordinary variables $\vec{x}$.

The impredicative version is the ordinary one, given below.

$$ \forall x \exists y \forall z \mathop. (z \in y) \leftrightarrow ((z \in x) \land \varphi(\vec{p}; z)) \;\; \text{is impredicative separation} $$

The predicative version is similar, but $\varphi(\vec{p}; z)$ is constrained to contain exclusively quantifiers bound by a parameter, i.e. $\forall x \in q \mathop. \square$ and $\exists x \in q \mathop. \square$ where $q$ is in $\vec{p}$ or is bound by an earlier quantifier.

Based on my understanding on the text quoted in the linked answer, this does not constitute a complete ban on impredicative quantification since the axiom schema of predicative separation itself contains unbound quantifiers $\forall x \exists y \forall z \mathop. \square$ in its prenex that cannot be paraphrased away.

So in this case, "predicativity" applies only to the value of the metavariable $\varphi(\cdots)$ and a set theory with this axiom would still be an "impredicative theory". (Maybe?)

Changing gears a little bit, if I look at the inference rules of the calculus of constructions, on which the proof assistant Coq is based, I'm not sure how to assess whether the formalism is predicative or not.

Here are the rules for convenience.

$K$ and $L$ range over $\{P, T\}$.

$$ \frac{}{\Gamma \vdash P : T} \;\; \text{$P$ is a large type} $$

$$ \frac{}{\Gamma, x: A, \Gamma' \vdash x : A} $$

$$ \frac{\Gamma \vdash A : K \;\;\text{and}\;\; \Gamma, x : A \vdash B:L}{\Gamma \vdash (\forall x : A \mathop. B) : L} \;\; \text{is universal introduction}$$

$$ \frac{\Gamma \vdash A : K \;\;\text{and}\;\; \Gamma, x: A \vdash N :B}{\Gamma \vdash (\lambda x: A \mathop. N):(\forall x : A \mathop. B)} \;\; \text{is function introdction} $$

$$ \frac{\Gamma \vdash M : (\forall x : A \mathop. B) \;\; \text{and}\;\; \Gamma \vdash N:A }{\Gamma \vdash M(N) : B[x:=N]} \;\; \text{is function elimination (but dependent!)} $$

$$ \frac{\Gamma \vdash M:A \;\;\text{and} \;\; A=_\beta B \;\;\text{and}\;\; \Gamma \vdash B:K}{\Gamma \vdash M : B } $$

In CoC, the "quantifiers" are always bound, but the text of the article implies that the calculus of inductive constructions is impredicative, perhaps suggesting that CoC itself is too.

Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity).

Answer 1

Impredicativity is one of those soft concepts that appears in many related forms, but it is difficult to explain what precisely they share. Let me try anyhow.

Impredicativity allows us to single out, construct, or characterize a particular entity $e$ of some totality (set, type, universe) $T$ by quantification over all of $T$. Such constructions are sometimes considered problematic, especially when $T$ is a "non-completed", "large" or otherwise mysterious collection, say the class of all sets, or the subsets of an infinite set.

If we ignore the fears that haunt predicative mathematicians, there still remains the technical observation that impredicativity often greatly increases the logical strength of a formal system. In fact, unbridled impredicativity was the culprit for the early paradoxes of set theory.

Here are some examples.

The axiom schema of separation

In set theory we may define an element of the class $\mathsf{Set}$, i.e. a set, by quantifying over the entire class $\mathsf{Set}$ using unbounded quantifiers. For example, $$\{x \in P(\emptyset) \mid \forall y . y \times x \cong y\}$$ is a silly way of constructing the set $\{\{\emptyset\}\}$ (sorry, I cannot think of a real example right now, but I am sure set theorists can come up with essential uses of unbounded separation). This is considered impredicative because $y$ ranges over all of $\mathsf{Set}$, including the set that is being defined.

It should be clear that bounded separation $\{x \in A \mid \phi\}$ in which all quantifiers appearing in $\phi$ are bounded (of the form $\forall y \in S$ and $\exists y \in S$) may be considered predicative since the sets over which the quantifiers range have been constructed already (or else we could not mention them).

The related principle of unbounded comprehension, stating that for any predicate $\phi$ there is a set $\{x \mid \phi\}$ is of course a form of impredicativity. In fact, this form of impredicativity is too strong, as it leads to Russell's paradox. It shows that impredicativity is not to be trifled with.

Complete lattices

A poset $(P, {\leq})$ is a complete lattice when it is closed under arbitrary suprema (in which case it is also closed under arbitrary infima). This is impredicative because it allows us to obtain an element $x \in P$ by quantifying over a subset $S \subseteq P$ of which $x$ may be an element (“$x$ is supremum of $S$” quantifies over $S$). The prime example is Tarski's fixed-point theorem: given a monotone map $f : P \to P$, the least fixed-point $x$ of $f$ is defined as $$x \mathbin{{:}{=}} \sup \{ y \in P \mid y \leq f(y) \}.$$ This definition of $x$ is impredicative because $x = f(x)$ and so $x$ is the element of the set that was used to specify $x$.

Powersets are complete lattices and thus may be considered a source of impredicativity. It should be noted that as soon as the powerset of the singleton $\{\star\}$ exists, all powersets exist because $P(A) \cong P(\{\star\})^A$. So the haunting is already done by the smallest non-trivial powerset. This is why topos theory is impredicative at its core: the subobject classifier $\Omega$ is precisely $P(\{\star\})$.

Impredicativity in type theory

In type theory quantification is carried out by products. An impredicative universe $U$ is thus one that is closed under quantification over $U$: $$ \frac{\vdash F : U \to U}{\vdash (\Pi (A {:} U) \,.\, F A) : U} $$ An example is the universe of propositions $\mathsf{Prop}$ which is closed under arbitrary products: $$ \frac{\vdash A \, \mathsf{type} \quad x {:} A \vdash P(x) : \mathsf{Prop} }{\vdash \forall x {:} A . P(x) : \mathsf{Prop}} $$ The universe $\mathsf{Prop}$ is impredicative because as a special case of the above we may quantify over $\mathsf{Prop}$ itself. This is very useful, of course, as it allows us to define logical connectives by Church encodings, e.g., $$p \lor q = \forall r {:} \mathsf{Prop} \,.\, (p \to r) \to (q \to r) \to r.$$ The above definition is impredicative because the meaning of $p \lor q$ is given by quantification over all propositions, one of which is $p \lor q$ itself.

System F is impredicative because it allows a type to be defined by quantification over all types, in much the same way as the impredicative encodings in $\mathsf{Prop}$. For related reasons second-order Peano arithmetic is considered impredicative (a predicate may be defined by quantification over all predicates).

A universe $U$ that contains itself and is closed under products is impredicative – and this is the case of impredicativity having gone too far because it leads to an inconsistency.

Predicativity

Those who feel uneasy about impredicativity, and those who want to carefully callibrate the logical strength of their formal systems, look for ways of avoiding impredicativity. In general this works by replacing self-referential constructions with iterative and inductive constructions which "build the object from below".

For example, Tarski's theorem (see above) may be proved as follows: give a monotone map $f : L \to L$, its least fixed point is the limit of the ordinal-indexed chain \begin{align*} x_{\beta} &\mathrel{{:}{=}} \sup \{ f(\alpha) \mid \alpha < \beta \} \end{align*} We have replaced impredicativity with transfinite recursion on ordinals – and in any specific case only a set-sized amount of such recursion is required.

In type theory impredicativity is typically avoided by introduction of universe levels, so that quantification over a universe $U_k$ yields a type in the next universe $U_{k+1}$.

One might still wonder whether some impredicativity is involved even in the most innocuous looking constructions. For example, when we replace the Church encoding of $p \lor q$ with direct-style inference rules, we might write the elimination rule as $$ \frac{p \vdash r \qquad q \vdash r}{p \lor q \vdash r} $$ Is this not quantification over all propositions $r$, just as before? No, there is an important difference: in the case of the Church encoding of $p \lor q$ the quantification was internal to the formal system (we used a quantifier that is one of the constructors of type theory), whereas the above rules use external or meta-level or schematic quantification. The latter has much less of a punch.

Answer 2

As I understand it, impredicativity in type theory is unrelated (at least in a formal way) from impredicativity in set theory.

The single rule in a type system which makes it impredicative is the following (here $*$ and $\square$ respectively denote your $P$ and $T$): $$\frac{\Gamma\vdash A : \square\quad \Gamma,x:A\vdash B : *}{\Gamma\vdash \Pi(x:A).B : *}$$ which corresponds to the $\lambda2$ axis in the lambda cube (I wrote an answer on this which might be helpful), and is present in both System F ($\lambda2$) and the calculus of constructions $(\lambda C)$. In Coq, $\square = \texttt{Type}_0$ and $* = \texttt{Prop}$.

Impredicativity is significant in computational power because it allows us to define inductive types in a self-referential way (hence impredicatively). For example, in an impredicative system, the natural numbers may be defined $$\mathbb N := \Pi (N:*).\Pi(A : *).A\to(N\to A\to A)\to(N\to A) : *$$ intuitively, this reads "$N$ is the smallest type in $*$ having an eliminator corresponding to that of the natural numbers". Indeed, we can define $$\texttt{zero} := \lambda N.\lambda A.\lambda z.\lambda s.\lambda n. z\\ \texttt{succ}(m):=\lambda N.\lambda A.\lambda z.\lambda s.\lambda n. (s\ n\ (m\ N\ A\ z\ s\ n))\\ \\ \texttt{rec}(A,z,s,n) := (n\ \mathbb N\ A\ z\ s\ n)$$

The calculus of inductive constructions (CIC) is an extension of the calculus of constructions with additional axioms for constructing (not impredicative) inductive types. So in CIC we have two very different ways of constructing inductive types.

It is my understanding that the Cedille proof assistant fully exploits impredicativity to define its inductive types.

Answer 3

System F allows for function types like $T=\Pi X. X \to X$, where $X$ ranges through all the types. In particular, $T$ is one of them! This means that the usual set-theoretic interpretation of $\Pi (a:A). B(a)$ as an infinite set product is no longer valid, since the components $B(a)$ are not defined yet! This is why we gave it the name impredicativity.

In some predicative systems, you may still form that $\Pi$ type, but it is no longer a "type". It lies in a higher level, and therefore goes out of the range of $X$.

Impredicative systems are useful for constructing recursive (i.e. self-referential but not vicious) things, such as Philip Wadler's famous Recursive types for free! paper. However, it is also "unstable", in a sense. In fact, it's a miracle that CoC is actually consistent, because every intuition from set theory goes against it: You can form a type $X \cong 2^{2^X}$ and so on. And slight modifications will jinx the consistency, as commented by Girard (which I cannot find the reference right now). System U is such an example.