Ramification of An Impredicative Type Theory Most type theories that I'm aware of are predicative by which I mean that

Void : Prop
Void = (x : Prop) -&gt; x


isn't well-typed in most theorem provers as this pi type belongs to the same universe as Prop and it isn't the case that Prop : Prop. This makes them predicative and disallows impredicative definitions like the above. However, an awful lot of "blackboard languages" such as System F or CoC are in fact impredicative. In fact, this impredicativity is vital to defining most of the constructs not included primitively in the language.

My question is why would one wish to give up impredicativity given it's power in defining logical constructs? I've heard a couple people remark that impredicativity screws up "computation" or "induction" but I'm having trouble finding a concrete explanation.
I'm going to elaborate my comments into an answer. The origins of predicative type theory are almost as old as type theory itself, since one of Russel's motivations was to ban "circular" definitions which were identified as part of the source of the XIXth century inconsistencies and paradoxes. Thierry Coquand gives an enlightened overview here. In this theory, predicates over a "level" or type, belong to the types of the "next" level, where there is an infinite (countable) number of levels.

While Russel's predicative hierarchy was (apparently) sufficient to dismiss the known paradoxes, it turned out to be very difficult to use as a foundational system. In particular, defining even something as simple as the real number system was extremely difficult, and so Russel postulated an axiom, the Axiom of Reducibility which postulated that all levels were "reduced" to one. Needless to say, this was not a satisfactory development.

However, contrary to the "harmful" impredicative statements (like unrestricted comprehension), this axiom did not seem to introduce any inconsistencies. The subsequent formulations of foundational theories (simple type theory, Zermelo's theory of sets) accepted them wholesale, making families of predicates (quantifying over possibly the whole universe of sets), predicates at the same level.

Circa 1971, Martin-Löf introduced dependent type theory in which both this principle and the further axiom Type : Type hold. This system turned out to be inconsistent for subtle reasons: the naive Russel paradox can not be played out (in a straightforward manner), but a clever encoding nevertheless allows a contradiction to be found. This prompted a crisis of faith similar to that of Russel, resulting in the predicative type theory with universes we know and love.

There is a way to repair the theory to allow "innocent" impredicativity a la Zermelo set theory, resulting in type theories like the Calculus of Constructions, but the damage was done, and the "Swedish school" of type theory tends to reject impredicativity.

Several points:


What does this have to do with intuitionistic mathematics? The answer is not much. At the turn of the XXth century, mathematicians tended to conflate the use of circular/impredicative principles with non-constructive reasoning (the intuition being that impredicative reasoning seems to assume a pre-existing mathematical universe, as does uses of the excluded middle). However, there are perfectly intuitionistic impredicative theories (like IZF). People interested in intuitionism still tend to be interested in predicativism for some reason (I'm guilty of this, of course).
What can you do in predicative mathematics? As Martin points out in his answer, Hermann Weyl (not to be confused with Andre Weil) started a program which tried to explore the expressive power of predicative systems, taking as starting point that predicative systems were of expressive strength between Peano Arithmetic and Second Order Arithmetic, which is pretty much agreed to be impredicative by most standards (and is comparable to System F on the type theory side). The program was later dubbed "reverse mathematics" as it tried to classify the strength of known mathematical theorems in terms of the axioms required to prove them (the reverse of the usual approach). The wikipedia page give a good overview; the program was quite successful, in that most of XIXth century mathematics can easily be accommodated in very weak systems. It is still an open question whether this program can scale to more recent results in, say, higher category theory (the suspicion is that the answer is "yes, with great effort").