23.10 Impredicativity

---

23.10 Impredicativity

The polymorphism of System F is often called impredicative. In general, a definition (of a set, a type, etc.) is called "impredicative" if it involves a quantifier whose domain includes the very thing being defined. For example, in System F, the type variable X in the type T = "X.X→X ranges over all types, including T itself (so that, for example, we can instantiate a term of type T at type T, yielding a function from T to T). The polymorphism found in ML, on the other hand, is often called predicative (or stratified), because the range of type variables is restricted to monotypes, which do not contain quantifiers.

The terms "predicative" and "impredicative" originate in logic. Quine (1987) offers a lucid summary of their history:

In exchanges with Henri Poincaré...Russell attributed [Russell's] paradox tentatively to what he called a vicious-circle fallacy. The "fallacy" consisted in specifying a class by a membership condition that makes reference directly or indirectly to a range of classes one of which is the very class that is being specified. For instance the membership condition behind Russell's Paradox is non-self-membership: x not a member of x. The paradox comes of letting the x of the membership condition be, among other things, the very class that is being defined by the membership condition. Russell and Poincaré came to call such a membership condition impredicative, and disqualified it as a means of specifying a class. The paradoxes of set theory, Russell's and others, were thus dismantled...

Speaking of terminology, whence "predicative" and "impredicative"? Our tattered platitude about classes and membership conditions was, in Russell's phrase, that every predicate determines a class; and then he accommodates the tattering of the platitude by withdrawing the title of predicate from such membership conditions as were no longer to be seen as determining classes. "Predicative" thus did not connote the hierarchical approach in particular, or the metaphor of progressive construction; that was just Russell and Poincaré's particular proposal of what membership conditions to accept as class-productive, or "predicative." But the tail soon came to wag the dog. Today predicative set theory is constructive set theory, and impredicative definition is strictly as explained in the foregoing paragraph, regardless of what membership conditions one may choose to regard as determining classes.

---