35
$\begingroup$

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).

$\endgroup$
2
  • 2
    $\begingroup$ I don't think it's just a terminology question. It's not like someone is asking "what's a prime number?" and then someone else gives a short answer that closes the matter. Rather, what is being asked for is an explanation of an open-ended dea that goes under the name of "predicativity". A tag such as foundations might be appropriate, though. $\endgroup$ Feb 11 at 15:51
  • 2
    $\begingroup$ I added some tags, feel free to remove if you feel they're inappropriate. I'm always in favor of specific tags. $\endgroup$
    – Couchy
    Feb 11 at 18:15

3 Answers 3

31
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ In your mention of complete lattices, “ A poset (𝑃,≤) ( P , ≤ ) 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 ∈ P by quantifying over a subset 𝑆⊆𝑃 S ⊆ P of which 𝑥 x may be an element (“𝑥 x is supremum of 𝑆 S ” quantifies over 𝑆 S ).” $\endgroup$
    – ToucanIan
    Sep 21 at 15:43
  • $\begingroup$ When you say, “This is impredicative because…” are you saying the definition of a complete lattice is? Or something more subtle? $\endgroup$
    – ToucanIan
    Sep 21 at 15:44
  • $\begingroup$ Sorry about the butchering of that copy and paste… I did this from my phone. $\endgroup$
    – ToucanIan
    Sep 21 at 15:46
  • 1
    $\begingroup$ Having a non-trivial complete lattice is impredicative. One could also worry how completeness is expressed, as it seemingly quantifies over arbitrary subsets, or over arbitrary families. But it may well be the case that can define what a complete lattice is without recourse to impredicativity (say, by a suitable axiom-schema or some such), and then discover they are all trivial. $\endgroup$ Sep 21 at 16:06
10
$\begingroup$

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.

$\endgroup$
5
  • 2
    $\begingroup$ That impredicative definition of $\mathbb{N}$ is cool. Quick question about it though. It seems like $\Pi N : *$ is being used to select a type and the inner $\Pi A : * \cdots$ is being used for its "truth value" of asserting the presence of an eliminator. $\endgroup$ Feb 11 at 4:27
  • 1
    $\begingroup$ Yes, that's precisely it, though the precise definition I gave might be off. $\endgroup$
    – Couchy
    Feb 11 at 4:30
  • 2
    $\begingroup$ The definition looks ok. This is called a Church encoding of a datatype (and sometimes Church-Prawitz). The idea is to represent a dataype in terms of its elimnators. $\endgroup$ Feb 11 at 7:02
  • 3
    $\begingroup$ Side note about Cedille: along with impredicativity you also need implicit product and dependent intersection types, and what you get are encodings of inductives that "realize their own induction principles", so they say. I think in general you can't get the full (i.e. dependently-typed) induction principle with impredicativity alone in the calculus. $\endgroup$
    – ionchy
    Feb 12 at 2:40
  • 1
    $\begingroup$ I thought the impredicative encoding of $\mathbb{N}$ was $\Pi(A:\ast). A \to (A\to A) \to A$. Where does the $N$ come in? $\endgroup$ Feb 12 at 5:02
8
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ If "every intuition from set theory goes against [CoC]", and "slight modifications will jinx the consistency", why should we accept such a weird system? How do we even know it is consistent to begin with? $\endgroup$
    – user21820
    Mar 26 at 12:21
  • $\begingroup$ @user21820 Yes, and it is exactly my belief that we shouldn't accept such a system! $\endgroup$
    – Trebor
    Mar 26 at 14:30
  • $\begingroup$ Hold on, can I confirm that you believe that we should not accept CoC because it is impredicative? This is the first time I see someone on SE who is as familiar with CoC as you and who seems to reject it on grounds of impredicativity, so I'm kind of surprised. Do you also reject full ZFC (where unbounded specification and replacement are also impredicative)? Thanks for your reply! $\endgroup$
    – user21820
    Mar 26 at 14:42
  • $\begingroup$ @user21820 I'm not against impredicativity in general. And propositional inpredicativity is just fine. But CoC is impredicative ay both levels. As a side note: Coq does not use CoC. $\endgroup$
    – Trebor
    Mar 26 at 16:11
  • $\begingroup$ Oh. But I recall reading that CoC has a model in ZFC, and in fact CoC plus universes, which I also thought is the underlying type theory for Coq. If one believes ZFC is meaningful for any reason, then it must translate to a belief that CoC is meaningful as well. So now I'm not really sure how CoC is any worse than full ZFC. Am I missing something? $\endgroup$
    – user21820
    Mar 26 at 16:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.