<p>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.</p>

<p>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 <strong>empirical</strong> 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&ouml;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. </p>

CC BY-SA 3.0
2015-03-23T20:41:21.883Z
To be fair, Russel was one of the first to *try*. He kind of admitted defeat (with the axiom of reducibility), though.
cody
CC BY-SA 3.0
2015-03-23T21:23:46.273Z
@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.
Martin Berger
CC BY-SA 3.0
2015-03-23T21:57:23.987Z
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](http://en.wikipedia.org/wiki/Reverse_mathematics) which precisely quantifies how much "impredicativity" you need.
cody
CC BY-SA 3.0
2017-10-11T13:37:54.350Z
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?
user21820
CC BY-SA 3.0
2017-10-11T23:32:04.077Z
@user21820 I did not say that all mathematics can be built up without impredicative definitions, that's an open question.
Martin Berger
CC BY-SA 3.0
2017-10-12T09:16:49.083Z
Hmm it's not an open question, since the incompleteness theorems show that you absolutely cannot computably capture all true facts of arithmetic, and hence no computable formal system can prove the computability of all computable ordinals. If that doesn't count as "all mathematics", then what counts? If you say what has been counted historically as mathematics, then it's also not an open question that some theorems are equivalent to Π[1,1]-CA which nearly everyone considers to be impredicative. So I don't understand your point.
user21820
CC BY-SA 3.0
2017-10-12T16:13:36.940Z
@user21820 Computability and impredicativity are (or seem to be) orthogonal. A
predicative foundation of mathematics might be non computable.  One
may think of ordinal analysis as started by Gentzen as a way to rescue
Hilbert's program from Gödel's incompleteness theorems.  Gentzen's
proof that Peano arithmetic is consistent uses transfinite induction
up to the ordinal ϵ0. Your "nearly everyone considers to be impredicative" points to something important: it's not totally clear what the boundary between predicative and impredicative is.
Martin Berger
CC BY-SA 3.0
2017-10-12T17:07:13.540Z
Well okay if you say that one cannot describe the boundary, then you can presumably escape one problem by accepting only what can be justified to be predicative constructions. If you cannot construct the least impredicative ordinal, you might be fine. But then you certainly can't escape the other problem, namely Zermelo set theory can't be counted as part of "mathematics". Do you count it?
user21820
CC BY-SA 3.0
2017-10-13T09:42:06.103Z
@user21820 I didn't say one cannot describe the boundary, I expressed it as an open problem. Maybe one
day there is a breakthrough like capturing computation with Turing
machines, who knows. The boundaries of mathematics itself are not
clear, pace Goedel's 2nd: You can add ever stronger axioms and it
becomes every more unclear whether the resulting system is consistent,
see Alan Turing's PhD dissertation.  (1 of 2)
Martin Berger
CC BY-SA 3.0
2017-10-13T09:42:21.677Z
@user21820 
Apart from all foundational questions, predicative mathematics is a
highly interesting research programme simply because of its
connections with computer science and programming language design (my
field of research), via the Curry-Howard correspondence, which has
been a highly fertile source of problems and ideas. (2 of 2)
Martin Berger
CC BY-SA 3.0
2017-10-13T12:25:21.337Z
Well you're still not answering my question: Do you consider Zermelo set theory as predicative? And consistency is a rather useless guide to meaning. Presumably you believe PA is consistent, so PA+¬Con(PA) is consistent too, but you don't consider that to be a valid foundation for mathematics! Why? Nothing to do with consistency. So one can't say that (the boundaries of) mathematics just involves consistency of the foundations. That is why it is crucial to have non-circular justification as far as is possible. Predicativity is one notion towards that goal, and it clearly excludes Z.
user21820
CC BY-SA 3.0
2017-10-13T12:29:33.503Z
Also, I'm very well aware of the BHK interpretation of intuitionistic logic, but intuitionism is very distinct from predicativism. That said, I agree that computability is closely related to various constructivist notions such as these.
user21820
CC BY-SA 3.0
2017-10-14T11:36:57.867Z
@user21820 ZF(C) set theory is paradigmatically impredicative, for example the
construction of the natural numbers as intersection of all inductive
sets, see Neel Krishnaswami's answer.
Martin Berger
CC BY-SA 3.0
2017-10-14T11:37:33.867Z
@user21820 Consistency is the *sine qua non* of foundations of mathematics
(FOMs). Any FOM *must* be consistent in the following sense: *there is                                                 
currently no known way of proving inconsistency*. Note that this a
*empirical* and *socio-temporal* property, hence may change over
time. (Aside: this is quite similar to cryptographic algorithms used
to secure the internet (e.g. RSA, DH, AES, SHA256) all of which
are not known (2017) to have exploitable flaws, but this may change.) Lack of consistency *immediately* kills a purported FOM.
Martin Berger
CC BY-SA 3.0
2017-10-14T11:37:45.103Z
@user21820 Other considerations apply when choosing a FOM to work with: e.g. is
it expressive enough to do the mathematics I am interested in? Do I
understand it? Is it convenient for humans?  Is it convenient for
computer verification? PA+¬Con(PA) fails on several of those: e.g. do
you understand models of PA+¬Con(PA)? I don't and by Tennenbaum's
theorem, their multiplication or addition can't be computable. That's
not helpful for day-to-day mathematical work. But maybe some weird person finds non-computable multiplication useful who know?
Martin Berger
CC BY-SA 3.0
2017-10-14T11:50:46.750Z
So you finally admit that ZF[C] is impredicative. Then you know very well that the construction of ordinals in ZF is impredicative, so ordinal analysis (as it currently refers to) is **not predicative**. I am not sure whether you actually understand enough of mathematical logic, since your response about PA+¬Con(PA) doesn't make philosophical sense. Choose any formal system S that **you think** is viable for foundations. Then by your criteria you believe that S is consistent and can perform basic arithmetic. But your criterion **doesn't exclude** the possibility that S proves ¬Con(S). [cont]
user21820
CC BY-SA 3.0
2017-10-14T11:53:30.570Z
[cont] So your criteria are not at all strong enough to be philosophically reasonable. The point is that we want arithmetical **soundness**, not simply consistency, as considering PA+¬Con(PA) or S+¬Con(S) would demonstrate. The issue is not about computable models, but about the fact that S+¬Con(S) proves all the theorems of S, and yet we reject it, not because of consistency but because of soundness.
user21820
CC BY-SA 3.0
2017-10-14T11:53:56.893Z
Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/67112/discussion-between-user21820-and-martin-berger).
user21820
CC BY-SA 3.0
2017-10-17T18:33:56.767Z
@user21820 Statements like "you finally admit that ZF[C] ..."  when I have never said such a thing make me wonder how I will benefit from a continuation of the discussion.  I'm not sure what you mean by "soundness" and "arithmetical soundness" in this context.  I'm not sure the original reason for ordinal analysis was for "justifying mathematics".  The original reason for analysing and removing impredicativity has been to remove one source of worry: as circularity has historically often been found to lead to inconsistency. Computational interpretations have added urgency to this task. (1/2)
Martin Berger
CC BY-SA 3.0
2017-10-17T18:34:07.397Z
As I said, there are many other reasons for choosing a FOM, one of them being aesthetic. But they are of a different nature than consistency: once a FOM is proven inconsistent, it's dead forever, unlike with e.g. philosophical considerations.  PA+¬Con(PA) is not typically chosen as a FOM, because (a) it's not well understood (cf Tenenbaum's theorem), and (b) because one feels queasy about something that -- prima facie -- screams "I'm inconsistent". As of Oct
2017, this feeling is not backed up by anything. (2/2)
Martin Berger
CC BY-SA 3.0
2017-10-18T07:42:30.427Z
@MartinBerger: You literally said "ZF(C) set theory is paradigmatically impredicative", so I've no idea why you now say you never admitted it. [Arithmetical soundness](https://en.wikipedia.org/wiki/Soundness#Arithmetic_soundness) is a standard concept in proof theory. The point which you don't seem to be getting is that ZF[C] may very well prove its own inconsistency, **even if** it is consistent. Or it may prove some other unsound arithmetical sentence, such as totality of some program that isn't actually total. And you can't use ZF[C] to do ordinal analysis since ZF[C] is impredicative.
user21820
CC BY-SA 3.0
2017-10-18T07:52:17.543Z
If you look at "original reason" for ordinal analysis, it **was indeed** to justify (finitary) mathematics; Gentzen showed that PRA plus well-ordering of ε[0] proves consistency of PA, and hence it provides an alternative way of justifying PA via ordinal analysis. The answer to (b) is the same as in my prior comment; you are still only concerned with consistency when that is far too weak to be philosophically useful, and that's why you can't seem to pinpoint why you are queasy with PA+¬Con(PA). It is arithmetically unsound and hence to be rejected. Every expert logician agrees on this...
user21820
CC BY-SA 3.0
2017-10-26T19:02:25.013Z
@user21820 I can only admit to something if I denied it beforehand. But I have never denied that
ZF is impredicative, I have always held ZF to be impredicative.  As to
"ZF[C] may very well prove its own inconsistency" can you show me such
a proof? If not and the formal theory models the things you want to
model, then it's currently a reasonable formal system.
Martin Berger
CC BY-SA 3.0
2017-10-27T09:41:36.333Z
@MartinBerger: We know that we can't justify non-circularly that ZF[C] does not prove its own inconsistency. Set theorists of course believe so, and even I believe it, but I'm quite doubtful that it is arithmetically sound. I don't agree that ZFC being capable of capturing what I want to model is sufficient to consider it reasonable. See [this](https://math.stackexchange.com/q/1843972/21820). As for "admit", I think it was miscommunication. Notice I never said you claimed contrary, but I was wondering why you appeared to keep avoiding my question about impredicativity of ZF. That's all.
user21820
CC BY-SA 3.0
2015-03-22T21:04:30.833Z
2015-03-24T21:25:02.150Z
2015-03-24T21:25:02.150Z
Martin Berger
<p>Type theories tend towards predicativity mainly socio-technical reasons. </p>

<p>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:</p>

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

<p>However, note that in standard (eg, ZFC) set theory, these operations <em>are not definable as objects</em>. There is <em>no such thing</em> 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.) </p>

<p>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 <a href="http://www.cl.cam.ac.uk/~amp12/papers/nontpt/nontpt.pdf"><em>Non-trivial Power Types Can't Be Subtypes of Polymorphic Types</em></a>. </p>

<p>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. </p>

CC BY-SA 3.0
2015-03-24T13:55:17.993Z
In an excellent paper by Wadler ([The Girard-Reynolds isomorphism](http://homepages.inf.ed.ac.uk/wadler/papers/gr/gr-TACS-FINAL.pdf)), 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.
cody
CC BY-SA 3.0
2015-03-24T13:38:24.047Z
2015-03-24T13:38:24.047Z
Neel Krishnaswami
<p>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 <a href="http://plato.stanford.edu/entries/type-theory/#3">here</a>. 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.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/Axiom_of_reducibility">Axiom of Reducibility</a> which postulated that all levels were "reduced" to one. Needless to say, this was not a satisfactory development.</p>

<p>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 (<a href="http://plato.stanford.edu/entries/type-theory-church/">simple type theory</a>, <a href="http://en.wikipedia.org/wiki/Zermelo_set_theory">Zermelo's theory of sets</a>) accepted them wholesale, making families of predicates (quantifying over possibly the whole universe of sets), predicates at the same level.</p>

<p>Circa 1971, Martin-Löf introduced dependent type theory in which both this principle and the further axiom <code>Type : Type</code> 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.</p>

<p>There is a way to repair the theory to allow "innocent" impredicativity <em>a la</em> 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.</p>

<p>Several points:</p>

<ol>
<li><p>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 <em>pre-existing</em> mathematical universe, as does uses of the excluded middle). However, there are perfectly intuitionistic impredicative theories (like <a href="http://plato.stanford.edu/entries/set-theory-constructive/">IZF</a>). People interested in intuitionism still tend to be interested in predicativism for some reason (I'm guilty of this, of course).</p></li>
<li><p>What <em>can</em> you do in predicative mathematics? As Martin points out in his answer, <a href="http://en.wikipedia.org/wiki/Hermann_Weyl#Foundations_of_mathematics">Hermann Weyl</a> (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 <a href="http://en.wikipedia.org/wiki/Peano_axioms">Peano Arithmetic</a> and <a href="http://en.wikipedia.org/wiki/Second-order_arithmetic">Second Order Arithmetic</a>, 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 <em>known</em> mathematical theorems in terms of the axioms <em>required</em> to prove them (the reverse of the usual approach). The <a href="http://en.wikipedia.org/wiki/Reverse_mathematics">wikipedia page</a> 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").</p></li>
</ol>

CC BY-SA 3.0
2015-03-24T11:39:32.770Z
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.
Martin Berger
CC BY-SA 3.0
2015-03-24T13:48:30.837Z
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$.
cody
CC BY-SA 3.0
2015-03-23T22:26:25.967Z
2015-03-23T22:26:25.967Z
cody
<p>Most type theories that I'm aware of are predicative by which I mean that</p>

<pre><code>Void : Prop
Void = (x : Prop) -&gt; x
</code></pre>

<p>isn't well-typed in most theorem provers as this pi type belongs to the same universe as <code>Prop</code> and it isn't the case that <code>Prop : Prop</code>. 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.</p>

<p>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.</p>

CC BY-SA 3.0
2015-03-23T00:42:19.817Z
Are type theorists predicative, or their theories?
Andrej Bauer
CC BY-SA 3.0
2015-03-23T00:44:12.483Z
I suppose Coq is not "most theorem provers" to you, because it accepts the above definition.
Andrej Bauer
CC BY-SA 3.0
2015-03-23T00:57:02.733Z
@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
daniel gratzer
CC BY-SA 3.0
2015-03-23T19:59:55.827Z
Ha! There is an `-impredicative-set` command-line option in Coq... Keep trying.
Andrej Bauer
CC BY-SA 3.0
2015-03-23T20:40:19.027Z
Why is Type not impredicative? > Check Type.  Type : Type. Well darn :)
cody
CC BY-SA 3.0
2015-03-23T20:50:49.797Z
@AndrejBauer "Why is it off by default?". I guess I'm not grasping if there is any reason *not* to define an impredicative system other than "it feels logically frightening". Sorry if I seem like I'm moving the goal posts a bit :)
daniel gratzer
CC BY-SA 3.0
2015-03-24T12:48:54.310Z
It's not just logically frightening but also set-theoretically frightening. You'll have to ask the Coq developers why it's off be default.
Andrej Bauer
CC BY-SA 3.0
2015-03-24T21:49:02.410Z
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. https://coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html and https://coq.inria.fr/library/Coq.Logic.Berardi.html
cody
CC BY-SA 3.0
2015-03-24T21:50:58.920Z
In fact it is not even clear that Coq + impredicative set is consistent without even any additional axioms! Werner's PhD work seems to suggest that it is, but for the full theory with universes this is a very open problem.
cody
<lo.logic><type-theory>
Ramification of An Impredicative Type Theory
daniel gratzer
# Ramification of An Impredicative Type Theory

(Asked by: username_0 on 2015-03-22)

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.

**Tags:** lo.logic, type-theory
> **Comments:**
> **username_1**: Are type theorists predicative, or their theories?  
> **username_1**: I suppose Coq is not "most theorem provers" to you, because it accepts the above definition.  
> **username_0**: @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  
> **username_1**: Ha! There is an `-impredicative-set` command-line option in Coq... Keep trying.  
> **username_2**: Why is Type not impredicative? > Check Type.  Type : Type. Well darn :)  
> **username_0**: @AndrejBauer "Why is it off by default?". I guess I'm not grasping if there is any reason *not* to define an impredicative system other than "it feels logically frightening". Sorry if I seem like I'm moving the goal posts a bit :)  
> **username_1**: It's not just logically frightening but also set-theoretically frightening. You'll have to ask the Coq developers why it's off be default.  
> **username_2**: 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. https://coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html and https://coq.inria.fr/library/Coq.Logic.Berardi.html  
> **username_2**: In fact it is not even clear that Coq + impredicative set is consistent without even any additional axioms! Werner's PhD work seems to suggest that it is, but for the full theory with universes this is a very open problem.  

---

## 3 answers

### Answer by username_2 on 2015-03-23. Score: 14 | Accepted answer

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](http://plato.stanford.edu/entries/type-theory/#3). 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](http://en.wikipedia.org/wiki/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](http://plato.stanford.edu/entries/type-theory-church/), [Zermelo's theory of sets](http://en.wikipedia.org/wiki/Zermelo_set_theory)) 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](http://plato.stanford.edu/entries/set-theory-constructive/)). 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](http://en.wikipedia.org/wiki/Hermann_Weyl#Foundations_of_mathematics) (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](http://en.wikipedia.org/wiki/Peano_axioms) and [Second Order Arithmetic](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Reverse_mathematics) 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").

> **Comments:**
> **username_3**: 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.  
> **username_2**: 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$.  

---

### Answer by username_3 on 2015-03-22. Score: 10

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.

> **Comments:**
> **username_2**: To be fair, Russel was one of the first to *try*. He kind of admitted defeat (with the axiom of reducibility), though.  
> **username_3**: @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.  
> **username_2**: 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](http://en.wikipedia.org/wiki/Reverse_mathematics) which precisely quantifies how much "impredicativity" you need.  
> **username_4**: 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?  
> **username_3**: @user21820 I did not say that all mathematics can be built up without impredicative definitions, that's an open question.  
> **username_4**: Hmm it's not an open question, since the incompleteness theorems show that you absolutely cannot computably capture all true facts of arithmetic, and hence no computable formal system can prove the computability of all computable ordinals. If that doesn't count as "all mathematics", then what counts? If you say what has been counted historically as mathematics, then it's also not an open question that some theorems are equivalent to Π[1,1]-CA which nearly everyone considers to be impredicative. So I don't understand your point.  
> **username_3**: @user21820 Computability and impredicativity are (or seem to be) orthogonal. A predicative foundation of mathematics might be non computable.  One may think of ordinal analysis as started by Gentzen as a way to rescue Hilbert's program from Gödel's incompleteness theorems.  Gentzen's proof that Peano arithmetic is consistent uses transfinite induction up to the ordinal ϵ0. Your "nearly everyone considers to be impredicative" points to something important: it's not totally clear what the boundary between predicative and impredicative is.  
> **username_4**: Well okay if you say that one cannot describe the boundary, then you can presumably escape one problem by accepting only what can be justified to be predicative constructions. If you cannot construct the least impredicative ordinal, you might be fine. But then you certainly can't escape the other problem, namely Zermelo set theory can't be counted as part of "mathematics". Do you count it?  
> **username_3**: @user21820 I didn't say one cannot describe the boundary, I expressed it as an open problem. Maybe one day there is a breakthrough like capturing computation with Turing machines, who knows. The boundaries of mathematics itself are not clear, pace Goedel's 2nd: You can add ever stronger axioms and it becomes every more unclear whether the resulting system is consistent, see Alan Turing's PhD dissertation.  (1 of 2)  
> **username_3**: @user21820  Apart from all foundational questions, predicative mathematics is a highly interesting research programme simply because of its connections with computer science and programming language design (my field of research), via the Curry-Howard correspondence, which has been a highly fertile source of problems and ideas. (2 of 2)  
> **username_4**: Well you're still not answering my question: Do you consider Zermelo set theory as predicative? And consistency is a rather useless guide to meaning. Presumably you believe PA is consistent, so PA+¬Con(PA) is consistent too, but you don't consider that to be a valid foundation for mathematics! Why? Nothing to do with consistency. So one can't say that (the boundaries of) mathematics just involves consistency of the foundations. That is why it is crucial to have non-circular justification as far as is possible. Predicativity is one notion towards that goal, and it clearly excludes Z.  
> **username_4**: Also, I'm very well aware of the BHK interpretation of intuitionistic logic, but intuitionism is very distinct from predicativism. That said, I agree that computability is closely related to various constructivist notions such as these.  
> **username_3**: @user21820 ZF(C) set theory is paradigmatically impredicative, for example the construction of the natural numbers as intersection of all inductive sets, see Neel Krishnaswami's answer.  
> **username_3**: @user21820 Consistency is the *sine qua non* of foundations of mathematics (FOMs). Any FOM *must* be consistent in the following sense: *there is                                                  currently no known way of proving inconsistency*. Note that this a *empirical* and *socio-temporal* property, hence may change over time. (Aside: this is quite similar to cryptographic algorithms used to secure the internet (e.g. RSA, DH, AES, SHA256) all of which are not known (2017) to have exploitable flaws, but this may change.) Lack of consistency *immediately* kills a purported FOM.  
> **username_3**: @user21820 Other considerations apply when choosing a FOM to work with: e.g. is it expressive enough to do the mathematics I am interested in? Do I understand it? Is it convenient for humans?  Is it convenient for computer verification? PA+¬Con(PA) fails on several of those: e.g. do you understand models of PA+¬Con(PA)? I don't and by Tennenbaum's theorem, their multiplication or addition can't be computable. That's not helpful for day-to-day mathematical work. But maybe some weird person finds non-computable multiplication useful who know?  
> **username_4**: So you finally admit that ZF[C] is impredicative. Then you know very well that the construction of ordinals in ZF is impredicative, so ordinal analysis (as it currently refers to) is **not predicative**. I am not sure whether you actually understand enough of mathematical logic, since your response about PA+¬Con(PA) doesn't make philosophical sense. Choose any formal system S that **you think** is viable for foundations. Then by your criteria you believe that S is consistent and can perform basic arithmetic. But your criterion **doesn't exclude** the possibility that S proves ¬Con(S). [cont]  
> **username_4**: [cont] So your criteria are not at all strong enough to be philosophically reasonable. The point is that we want arithmetical **soundness**, not simply consistency, as considering PA+¬Con(PA) or S+¬Con(S) would demonstrate. The issue is not about computable models, but about the fact that S+¬Con(S) proves all the theorems of S, and yet we reject it, not because of consistency but because of soundness.  
> **username_4**: Let us [continue this discussion in chat](http://chat.stackexchange.com/rooms/67112/discussion-between-user21820-and-martin-berger).  
> **username_3**: @user21820 Statements like "you finally admit that ZF[C] ..."  when I have never said such a thing make me wonder how I will benefit from a continuation of the discussion.  I'm not sure what you mean by "soundness" and "arithmetical soundness" in this context.  I'm not sure the original reason for ordinal analysis was for "justifying mathematics".  The original reason for analysing and removing impredicativity has been to remove one source of worry: as circularity has historically often been found to lead to inconsistency. Computational interpretations have added urgency to this task. (1/2)  
> **username_3**: As I said, there are many other reasons for choosing a FOM, one of them being aesthetic. But they are of a different nature than consistency: once a FOM is proven inconsistent, it's dead forever, unlike with e.g. philosophical considerations.  PA+¬Con(PA) is not typically chosen as a FOM, because (a) it's not well understood (cf Tenenbaum's theorem), and (b) because one feels queasy about something that -- prima facie -- screams "I'm inconsistent". As of Oct 2017, this feeling is not backed up by anything. (2/2)  
> **username_4**: @MartinBerger: You literally said "ZF(C) set theory is paradigmatically impredicative", so I've no idea why you now say you never admitted it. [Arithmetical soundness](https://en.wikipedia.org/wiki/Soundness#Arithmetic_soundness) is a standard concept in proof theory. The point which you don't seem to be getting is that ZF[C] may very well prove its own inconsistency, **even if** it is consistent. Or it may prove some other unsound arithmetical sentence, such as totality of some program that isn't actually total. And you can't use ZF[C] to do ordinal analysis since ZF[C] is impredicative.  
> **username_4**: If you look at "original reason" for ordinal analysis, it **was indeed** to justify (finitary) mathematics; Gentzen showed that PRA plus well-ordering of ε[0] proves consistency of PA, and hence it provides an alternative way of justifying PA via ordinal analysis. The answer to (b) is the same as in my prior comment; you are still only concerned with consistency when that is far too weak to be philosophically useful, and that's why you can't seem to pinpoint why you are queasy with PA+¬Con(PA). It is arithmetically unsound and hence to be rejected. Every expert logician agrees on this...  
> **username_3**: @user21820 I can only admit to something if I denied it beforehand. But I have never denied that ZF is impredicative, I have always held ZF to be impredicative.  As to "ZF[C] may very well prove its own inconsistency" can you show me such a proof? If not and the formal theory models the things you want to model, then it's currently a reasonable formal system.  
> **username_4**: @MartinBerger: We know that we can't justify non-circularly that ZF[C] does not prove its own inconsistency. Set theorists of course believe so, and even I believe it, but I'm quite doubtful that it is arithmetically sound. I don't agree that ZFC being capable of capturing what I want to model is sufficient to consider it reasonable. See [this](https://math.stackexchange.com/q/1843972/21820). As for "admit", I think it was miscommunication. Notice I never said you claimed contrary, but I was wondering why you appeared to keep avoiding my question about impredicativity of ZF. That's all.  

---

### Answer by username_5 on 2015-03-24. Score: 8

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*](http://www.cl.cam.ac.uk/~amp12/papers/nontpt/nontpt.pdf).

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.

> **Comments:**
> **username_2**: In an excellent paper by Wadler ([The Girard-Reynolds isomorphism](http://homepages.inf.ed.ac.uk/wadler/papers/gr/gr-TACS-FINAL.pdf)), 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.  

---

