## Impredicativity

I hope this question is not so elementary that it'll get me banned...

In mathematics we see a lot of impredicativity. Example of definitions involving impredicativity include: subgroup/ideal generated by a set, closure/interior of a set (in topology), topology generated by a family of sets, connected/path connected component of a point, sigma algebra generated by a family... And of course, the least upper bound property of real numbers. Impredicativity flood mathematics but there are people who don't like it. I think type theory was developed due the paradoxical and impredicative nature of "set of all sets that don't contain themselves".

I'm very ignorant on this and from what I read type theory is hopeless complicated to work this, so I ask the people who favor predicativism: all those people have fiddled with mathematics for all those years and no one ever found a contradiction (I mean in ZFC), so is it worth all that effort?

-
I think predicativism is just some pseudo theory that some philosophers like to play with because they want to talk about mathematics but don't really want to do mathematics. All these pseudo theories such as predicativism, contructivism, finitism, formalism anything else -ism are just a philosopher's caricatures of mathematics in some imaginary world of his own without taking into account the full complexity of mathematical objects and of mathematics itself. All these caricatures have become fashionable and subject of intense (and fruitless) debate while mathematics itself is for eternity – alephomega May 28 2010 at 5:50
continued: My point of view might itself be a caricature of this philosophical debate but that is the impression I got out of this debate by the time I finished my MA in phil of math. – alephomega May 28 2010 at 5:50
Not being a philosopher, I looked up "impredicativity" on Wikipedia, which gives: "More precisely, a definition is said to be impredicative if it invokes (mentions or quantifies over) the set being defined, or (more commonly) another set which contains the thing being defined." The definitions I know for all your examples do not fit Wikipedia's gloss. – Theo Johnson-Freyd May 28 2010 at 5:53
@alphaomega: What is the point of your comment, other than a display of your own ignorance? – Andrej Bauer May 28 2010 at 8:48
@Andrej Bauer: actually I must thank you, Mummert and Krishnaswami. After reading the posts, I realize that this is really useful for mathematics. Thank you for proving me wrong, I would otherwise have kept my disappointment. – alephomega May 28 2010 at 23:57

Yes, it is worth the effort. A predicative version of an impredicative construction is typically more explicit and informative than the impredicative one. For example, consider the construction of a subgroup $\langle S \rangle$ of a group $G$ generated by the set $S$:

• impredicative: $\langle S \rangle$ is the intersection of all subgroups of $G$ which contain $S$.
• predicative: $\langle S \rangle$ consists of all finite combinations of elements of $S$ and their inverses, i.e., a typical elements is $x_1 x_2 \cdots x_n$ where $x_i \in S \cup S^{-1}$.

This can be quite useful if you want to compute with groups (i.e., with a computer), as you will definitely prefer the second description, which tells you how exactly the elements of the subgroup can be represented.

Many examples of impredicative constructions are special cases of the following theorem.

Theorem (Knaster and Tarski): A monotone map on a complete lattice has a least fixed-point above every point.

To take two of your examples:

• Subgroup generated by a set: the complete lattice is the powerset $P(G)$ of the group $G$ in question, and the map $f : P(G) \to P(G)$ takes $S \subseteq G$ to $f(S) = S \cup S^{-1} \cup S \cdot S$.

• $\sigma$-algebra generated by a family of subsets: exercise.

There are two standard ways of proving the Knaster-Tarski theorem, one impredicative and one predicative. These exemplify the two general approaches of getting to desired objects "impredicatively from above" and "predicatively from below".

The impredicative proof goes as follows: call a point $x$ a prefixed point if $f(x) \leq x$. Consider the set $S$ of all prefixed points above a given point $y$ (which is not empty as it contains the top of the lattice). The least fixed-point above $y$ is the infimum $x = \inf S$ (exercise).

The predicative proof goes as follows: iterate $f$ starting with a given point $y$ to construct an increasing sequence $$y, f(y), f^2(y), \ldots, f^\omega(y), \ldots, f^\alpha(y), \ldots$$ where we have to iterate through ordinals until we're blue in the face. The iteration stops eventually, and that's the least fixed-point above $y$.

Of course, in such generality the predicative proof is hardly better than the impredicative one because we replaced one non-description with another. But in particular cases we might know something about $f$. For example, we might know that it preserves suprema of countable chains, as we do in the example of a subgroup generated by a set, in which case the iteration stops at $\omega$.

Your third example, namely the connected component of a point, can be dealt with also, but I am not sure it's any better than the impredicative construction:

• Connected components: the connected component of a point is a maximal connected subset containing it. You are probably thinking of the construction that says "just take the union of all connected subsets that contain the point". We could instead try the following: define $x \sim y$ to mean that for all continuous $f : X \to 2$, $f(x) = f(y)$. The connected components of $X$ are the equivalence classes of $\sim$. Therefore the connected component of a point is just its equivalence class. This is not entirely satisfactory as it replaces one bad description with another. Can we be more explicit? What if we have a nice basis for the space?

Sometime you have to reformulate the whole subject to get away from builtin impredicativity (and it is still worth doing because it gives computational meaning to theorems which are quite non-computational in the impredicative setting):

• Closure/interior of a set: under classical formulation of topology you can sometimes get away with predicative construction, for example if you can reduce your construction to manipulation of a countable topological basis, e.g. the interior of $S \subseteq \mathbb{R}$ is the union of all open intervals with rational endpoints that are contained in $S$. There are general formulations of topology, such as formal topology and Abstract Stone Duality, which avoid impredicative constructions altogether.

Lastly, you mention Dedekind completeness of reals. I am not sure this is impredicative. The supremum of a non-empty bounded family of left-sided Dedekind cuts is simply their union. What is impredicative about taking the union of a family of cuts?

Adendum: Note that in the typical case it is the construction, i.e., an existence proof, which is predicative or impredicative, not the definition. For example, the group generated by a set is defined as the least subgroup containing the generators, which has nothing to to with predicativity/impredicativity.

P.S. You need a better MO username.

-
 I have seen people write that completeness of the real line is impredicative because the definition of "least upper bound" can be written in a way that quantifies over all upper bounds. This does not stand up to scrutiny, of course, because one can construct least upper bounds in predicative systems such as ACA. But maybe it explains that part of the original question above. – Carl Mummert May 28 2010 at 13:41 Thanks, I guess it's best to give attention to both impredicative and predicative concepts/proofs, as the former is usually very "slick" as you said below and the latter gives further insight. Another side question: for the predicative proof of Knaster-Tarski theorem, why do you use all ordinals? Zorn's lemma (from axiom of choice) also uses all ordinals, but we can just use a well ordered set with cardinality greater than the partially ordered set in question. – dumb student May 29 2010 at 8:26 You don't have to use "all ordinals", that's more or less a manner of speaking: typically we know in advance that the iteration will stabilize, say at an ordinal whose cardinality exceeds the cardinality of everything in sight. But since it is just as easy to write down the definition of iteration for all ordinals as for ordinals up to some bound, people usually opt for the unbounded way. Mind you, I did not use "all ordinals, just enough of them to be blue in the face... – Andrej Bauer May 29 2010 at 18:49

Andrej's answer is great, but I want to elaborate on one point: often, there are multiple, incompatible, ways to strengthen a formalism. Developing a piece of mathematics using relatively weak techniques is a form of "insurance": it will be portable regardless of how you go about strengthening the formalism in the future.

In particular, there are actually multiple ways of formalizing the idea we call "impredicativity".

Concretely, there are type theories (such as System F) which support what we can call "impredicative indexing" -- that is, we can define types by indexing over all types, such as the type $\forall \alpha:\mathrm{Type}. \alpha \to \alpha$, which is the type of endofunctions which work at arbitrary types. For obvious size reasons, such a construction in Set is not possible. However, such types (and their formation and elimination rules) formalize an idea of Carnap's, which is that even apparently circular impredicative definitions can't possibly get you into logical trouble if you use the totality you quantify over in a purely schematic way.[1]

On the other hand, set theory has the powerset axiom, which gives you a different form of impredicativity (which Andrej used in his sketch of the proof of the Knaster-Tarski theorem). These two forms of impredicativity are incompatible with each other[2], but they both embody natural formalizations of the idea of impredicativity.[3]

Predicative arguments are ported easily to both type theory (say, for verification in a proof assistant) and to set theory (say, for verification by a grad student) -- but the excessive use of powerset or parametricity axioms will make the porting job a lot harder!

1. See Fruchhart and Longo's "Carnap's Remarks on Impredicative Definitions and the Genericity Theorem"
2. See Andrew Pitts' "Non-trivial Power Types Can't be Subtypes of Polymorphic Types"
3. As an aside, I find this one of the major annoyances of programming language research; we frequently need F-style impredicativity, but models of F in ordinary mathematics require building structures sufficiently exotic that F's functions in that model "differ enough" from Set's functions. This calls for techniques that feel rather more high-powered than ought to be necessary...
-

Andrej Bauer points out that predicative constructions are more explicit, and give more useful computational information, than impredicative ones. This has two further consequences that are of interest. I want to point these out as an answer to the implicit question asked by "alephomega".

1. If a theorem about reasonable objects can be proven predicatively, this gives important information on the consistency strength (i.e. the proof-theoretic ordinal) associated with the theorem. Conversely, we know that some theorems such as Kruskal's theorem cannot be proven predicatively because these theorems lead to proof-theoretic ordinals that are too large. Thus the mathematical analysis of predicativity reveals the full complexity of results such as Kruskal's theorem, rather than obscuring it. This is separate from the philosophical analysis of predicativity.

2. The "computability" consequences of a predicative proof can be extremely important. In the context of a countable group $G$, a "top-down" construction such as "intersect all subgroups of $G$ that contain the set $X$" will only naively give that the constructed object is $\Pi^1_1$ over $G\oplus X$. A bottom-up construction will usually show that the constructed object is actually arithmetical in $G\oplus X$. Examination of the bottom-up proof can then give explicit bounds in the arithmetical hierarchy on the complexity of the constructed object. For example, in the case of a subgroup of a group $G$ generated by a subset $X$, the degree of the subgroup is no more than the Turing jump of $G \oplus X$; this is an enormously better bound than the naive $\Pi^1_1$ result.

-
 Your answer is nice. My comments were probably rude but I am implicitly asking to be "re-convinced" about the importance of these philosophical questions. Somehow I had lost faith... – alephomega May 28 2010 at 19:18

Type Theory is worthwile alone for its practical applications. So if you dont like it as a foundation of mathematics, accept it as applied mathematics.

On the other hand, predicative definitions are a mostly clearer and easier to understand, and if you look at most algebra-books, whenever there is a short impredicative definition given, you will have at least three lemmata or theorems proving the equivalence with some predicative property. Its questionable why to have this impredicative definitions at first sight then.

-
 Because sometimes (often?) impredicative constructions are slicker than the predicative ones. – Andrej Bauer May 28 2010 at 22:10 Even internally to type theory, impredicative formation rules for inductive types are (imo) clearer and more flexible than syntactic positivity conditions. Eg, replace syntactic positivity with a condition that you can take the fixed point of a type operator $F$ when $\Pi \alpha,beta.\; (\alpha \to \beta) \to F(\alpha) \to F(\beta)$ is derivable. (Externally, this condition amounts to saying $F$ is monotone on the provability lattice of types, but requires impredicative quantification to internalize.) – Neel Krishnaswami May 29 2010 at 9:42