11
$\begingroup$

Most type theories that I'm aware of are predicative by which I mean that

Void : Prop
Void = (x : Prop) -> 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.

$\endgroup$
  • $\begingroup$ Are type theorists predicative, or their theories? $\endgroup$ – Andrej Bauer Mar 23 '15 at 0:42
  • 2
    $\begingroup$ I suppose Coq is not "most theorem provers" to you, because it accepts the above definition. $\endgroup$ – Andrej Bauer Mar 23 '15 at 0:44
  • $\begingroup$ @AndrejBauer Why not both? :) I guess coq has an impredicative universe as well as a predictive one. I suppose my question is. "Why is set not impredicative as well?" in the context of coq $\endgroup$ – Daniel Gratzer Mar 23 '15 at 0:57
  • 1
    $\begingroup$ Why is Type not impredicative? > Check Type. Type : Type. Well darn :) $\endgroup$ – cody Mar 23 '15 at 20:40
  • 1
    $\begingroup$ No need to bother the developers! Impredicative Set is quite nasty, and in particular, it conflicts with some rather natural choice principles and the so-called "informative excluded middle" forall P : Type, {P} + {~P}, as this + impredicative set implies proof irrelevance (and nat is not proof irrelevant). See e.g. coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html and coq.inria.fr/library/Coq.Logic.Berardi.html $\endgroup$ – cody Mar 24 '15 at 21:49
12
$\begingroup$

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:

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

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

$\endgroup$
  • 1
    $\begingroup$ Your nice post contains a very interesting side-remark: "is pretty much agreed to be impredicative by most standards". It points to something subtle, namely that it's not clear where exactly the boundary between predicative and impredicative should be drawn. $\endgroup$ – Martin Berger Mar 24 '15 at 11:39
  • 4
    $\begingroup$ That's true, but the point I somewhat failed to make is that the line, if there is one, should be drawn before $\mathrm{PA}_2$. $\endgroup$ – cody Mar 24 '15 at 13:48
10
$\begingroup$

One dimension is type inference. System F's type inference for example is not decidable, but some its predicative fragments have decidable (partial) type inference.

Another dimension is consistency as a logic. Distinguished thinkers have historically felt a bit queasy about having impredicative foundations of mathematics. After all, it's a form of circular reasoning. I think H. Weyl might have been the first or, one of the first, who tried to reconstruct as much of mathematics as possible in a predicative way ... just to be on the safe side. We have learned that the circularities of impredicativity are not problematic in classical mathematics, in the sense that no contradictions have ever been derived from 'tame' impredicative definitions. Over time, we learned to trust them. Note that this (absence of paradoxa) is an empirical observation! However, much of the development of proof theory, with its weird ordinal constructions has as ultimate goal the wish to build up all of mathematics 'from below', i.e. without impredicative definitions. This programme is not completed. In recent years, interest in predicative foundations of mathematics has shifted from worries about paradoxa to the computational content of proofs, which interesting for various reasons. Turns out that impredicative definitions make it difficult to extract computational content. Another angle in the worry about consistency comes from the Curry-Howard tradition. Martin-Löf's original type theory was impredicative ... and unsound. Following that shock, he proposed only predicative systems, but combined with inductive data types to regain much of impredicativity's power.

$\endgroup$
  • 1
    $\begingroup$ To be fair, Russel was one of the first to try. He kind of admitted defeat (with the axiom of reducibility), though. $\endgroup$ – cody Mar 23 '15 at 20:41
  • $\begingroup$ @cody I'm not too familiar with the history of these attempts. How successful has Weyl (and S. Feferman) been in their attempts? MLTT / HOTT certainly work, I'd say. $\endgroup$ – Martin Berger Mar 23 '15 at 21:23
  • 2
    $\begingroup$ Basically, Weyl was extremely successful, i.e. most of the corpus of analysis can be formalized without appeal to 2nd order (impredicative) mathematics. The body of work has become part of Reverse Mathematics which precisely quantifies how much "impredicativity" you need. $\endgroup$ – cody Mar 23 '15 at 21:57
  • $\begingroup$ It's not true that proof theory can "with its weird ordinal constructions" build up all of mathematics without impredicative definitions. The issue is that proof theory is not done within a vacuum, but in a formal system, which would itself have some proof-theoretic ordinal that it is incapable of proving well-founded. So this pursuit definitely can never reach the 'bottom'. Some logicians think that Γ[0] is the first impredicative ordinal, and if so then you are stuck at and cannot predicatively justify ATR0. If not, then you need to justify that Γ[0] is predicative. How would you? $\endgroup$ – user21820 Oct 11 '17 at 13:37
  • $\begingroup$ @user21820 I did not say that all mathematics can be built up without impredicative definitions, that's an open question. $\endgroup$ – Martin Berger Oct 11 '17 at 23:32
8
$\begingroup$

Type theories tend towards predicativity mainly socio-technical reasons.

First, the informal concept of impredicativity can be formalized in (at least) two different ways. First, we say that a type theory like System F is impredicative because type quantification can range over all types (including the type the quantifier belongs to). So we can define generic identity and composition operators:

$$ \begin{array}{lclll} \mathit{id} & : & \forall a.\; a \to a & = & \Lambda a.\;\lambda x.\;x\\ \mathit{compose} & : & \forall a, b, c.\; (a \to b) \to (b \to c) \to (a \to c) & = & \Lambda a,b,c.\lambda f, g. \lambda x. g(f\;x) \end{array} $$

However, note that in standard (eg, ZFC) set theory, these operations are not definable as objects. There is no such thing as "the identity function" in set theory, because a function is a relation between a domain set and a codomain set, and if a single function could be the identity function, then you could use it to construct a set of all sets. (This is basically how John Reynolds showed that System-F style polymorphism had no set-theoretic models.)

However, set theory is impredicative in another way, via the powerset axiom. Power sets are impredicative because you can say things like "let $X$ be the intersection of all subsets of $S$ with property $P$" and then proceed to prove that $X$ itself has property $P$. As a result, $X$ has been defined "impredicatively", in terms of a set of which it is a member. This notion of impredicativity is incompatible with F-style quantification; see Andy Pitts's paper Non-trivial Power Types Can't Be Subtypes of Polymorphic Types.

So F-style impredicativity is incompatible with a naive view of types as sets. If you are using type theory as a proof assistant, it's nice to be able to port standard math easily to your tool, and so most people implementing such systems simply remove impredicativity. This way everything has both a set-theoretic and type-theoretic reading, and you can interpret types in whatever fashion is most convenient for you.

$\endgroup$
  • 3
    $\begingroup$ In an excellent paper by Wadler (The Girard-Reynolds isomorphism), it is shown how the tight correspondence between system F and 2nd order arithmetic works. In that setting, system F impredicativity and set theoretic impredicativity (subsets of $\mathbb{N}$ can be defined by quantification over all subsets of $\mathbb{N}$) are identical. I think it would be misleading to say that they are fundamentally different. $\endgroup$ – cody Mar 24 '15 at 13:55

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.