<p>The definition of an object $X$ is <strong>impredicative</strong>, if the definition uses a collection $C$ in the construction of $X$, such that $X$ is a member of $C$.  So impredicativity is a form of <strong>circularity</strong>.</p>

<p>We are wary of circular definitions because they are often paradoxical. Fortunately it turns out that not all forms of
circularity are (or appear to be) problematic.  The most famous example of an impredicative definition that is circular, but (as far as we know) not contradictory is the definition of natural numbers in set theory:</p>

<p>$$
\mathbb{N}\ \stackrel{\text{def}}{=}\ \bigcap \{X\ |\ X\ \text{is an inductive set}\}
$$</p>

<p>where a set is inductive if it contains $\emptyset$ and
  is closed under the set-theoretic successor operation.  Clearly, $\mathbb{N}$ is itself inductive, hence what you define on the left already occurs in some sense on the right.</p>

<p>By the "impredicative version of Martin-Löf's type theory" I guess you mean the type theory in his 1971 manuscript "<em>An intuitionistic theory of types</em>". This system has an  impredicative axiom  that stipulates a type of all types.  For this reason the system is often simply called "<em>type:type</em>". This axiom is too strong as J.-Y. Girard showed, as it makes the type-theory inconsistent. </p>

<p>In contrast, the impredicativity in the CoC is not (known to be) inconsistent.</p>

<p>In some sense there are two forms of impredicativity: those that are known to be paradoxical, and those that are not.</p>

CC BY-SA 3.0
2016-06-26T06:20:20.743Z
I don't think the definition of N is impredicative in set theory. The infinity axiom simply states that there is an inductive set. N is defined as the smallest inductive subset of that inductive set IIRC, not defined as the intersection of all inductive sets.
Kaveh
CC BY-SA 3.0
2016-06-26T10:58:42.337Z
@Kaveh How do you define "smallest inductive subset" in a predicative way in ZF?
Martin Berger
CC BY-SA 3.0
2016-06-26T11:11:26.787Z
We don't need to define $\omega$ as the smallest inductive set, it is proven to have that property. We can define $\omega$ to be the smallest inductive subset of the inductive set that the infinity axioms states its existence.
Kaveh
CC BY-SA 3.0
2016-06-26T11:12:10.680Z
I don't see how this definition of $\omega$ can be carried out in ZF in a predicative way.
Martin Berger
CC BY-SA 3.0
2016-06-26T11:24:33.260Z
ps: I just checked Jech, Enderton, and Kunen's books, they do define $\omega$ as you said. But as I said this is not really needed, when defining using intersection you can get rid of impredicativity and make it predicative if you start with an inductive set which the axiom of infinity tells it exists.
Kaveh
CC BY-SA 3.0
2016-06-26T11:28:51.790Z
I would be interested in seeing the ZF formula that defines $\omega$ in a predicative way. I don't believe it can be done.
Martin Berger
CC BY-SA 3.0
2016-06-26T11:44:13.787Z
Here is an argument for the existence of a smallest inductive subset that I mentioned: let $X$ be the inductive set that axiom of infinity states its existence. Now let $N := \cap\{Y \in P(X) | Inductive(Y)\}$. We can show that it is subset of any inductive set $Z$ because the intersection of $Z$ and $X$ is inductive and in $P(X)$. The formula depends on the name of the inductive set that the axiom of infinity states its existence but if you give it a name then the formula is rather simple.
Kaveh
CC BY-SA 3.0
2016-06-26T11:53:00.317Z
Is the issue that $P(X)$ contains N?
Kaveh
CC BY-SA 3.0
2016-06-26T12:04:44.100Z
Yes. Your definition is impredicative as the set you are defining ($N$) already occurs on the something you use on the right hand side of the definition.
Martin Berger
CC BY-SA 3.0
2016-06-26T12:13:33.843Z
Let me give you a different example. If $S$ is a set of vectors in a vector space $V$ then $span(S)$ = $\bigcap \{W\ |\ S \subseteq W, W \ \text{subspace of}\ V\}$. This is the usual impredicative definition of the vector space generated by $S$. We can make it predicative by setting $span(S)$ = $\{\alpha_1v_1 + ... + \alpha_nv_n\ |\ 0 \leq n, \alpha_i \in \mathbb{R}, v_i \in S\}$.  I'm not sure how to carry out a similar 'predicativation' for $\mathbb{N}$ in ZF.
Martin Berger
CC BY-SA 3.0
2016-06-25T19:37:55.483Z
2017-03-06T15:55:08.780Z
2017-03-06T15:55:08.780Z
Martin Berger
<p>In a system where Type:Type, the typing rule for the product would be trivial:</p>

<p>$$\frac{\Gamma \vdash A:Type\hspace{1cm}     \Gamma, x:A \vdash B:Type}
      {\Gamma \vdash \forall x\!:\!A.B : Type}$$</p>

<p>Unfortunately, Type:Type is known to be inconsistent, and Type must
inhabit some different sort, say Type:BigType. Then, the following case of the
product becomes problematic:</p>

<p>$$\Gamma \vdash A:BigType\hspace{1cm}     \Gamma, x:A \vdash B:Type$$</p>

<p>You may either conclude that</p>

<p>$$       (*)\;\;\Gamma \vdash \forall x:A.B : BigType$$</p>

<p>or</p>

<p>$$ (**)\;\; \Gamma \vdash \forall x:A.B : Type $$</p>

<p>The first approach, where you take the maximum among the type of A and
B is the so called predicative approach, giving rise to a strictly
stratified type theory. This is indeed consistent with our intuition of
types as data structures.</p>

<p>The second approach is "impredicative": since Type:BigType, if B:Type, we get</p>

<p>$$                      \forall X\!:\!Type.B: Type$$</p>

<p>but this expression is quantifying over a collection of items (Type)
comprising the product type we are defining as one of its elements.</p>

<p>Note however that is not so unreasonable in case you are interpreting Types as
propositions: if $B:Prop$, then $\forall X\!:\!Prop.B$ looks like a legitimate, higher order
proposition, hence it looks quite "natural" (for everybody who is not a
constructivist) to conclude that 
                      $\forall X\!:\!Prop.B : Prop$</p>

<p>In fact, (**) is not inconsistent (system F adopts this rule).
The only price you have to pay is that you must renounce to have strong
elimination rules. In Coq terms, you
cannot extract from a proposition anything but a proof of some other
proposition. As a corollary, you have no way in Coq to prove that two proofs of a same proposition are different from each other.</p>

CC BY-SA 3.0
2017-03-06T12:45:52.597Z
2017-03-06T17:59:46.037Z
2017-03-06T17:59:46.037Z
Andrea Asperti
<p>I am confused. I think I've read two usages of the word "impredicative" in type theory:</p>

<ol>
<li>When people talk about the "impredicative" version of Martin-Löf's type theory, which they say it is inconsistent. Apparently they call it impredicative because of Type : Type.</li>
<li>When people talk about the "impredicative" Prop in CoC. Apparently they call it impredicative because you can quantify over Prop and get Prop stuff.</li>
</ol>

<p>Is it the case? One notion of impredicativity implies the other? Is there no problem (i.e. inconsistency) by assuming "Prop impredicative"?</p>

CC BY-SA 3.0
2016-06-25T13:49:45.530Z
http://adam.chlipala.net/cpdt/html/Universes.html should be useful.
Alexey Romanov
CC BY-SA 3.0
2016-06-25T14:34:20.040Z
https://en.wikipedia.org/wiki/Impredicativity
Kaveh
CC BY-SA 3.0
2016-06-26T11:58:43.317Z
https://math.stanford.edu/~feferman/papers/predicativity.pdf
Kaveh
<type-theory><calculus-of-constructions>
"Impredicative" in type theory
user40579
# "Impredicative" in type theory

(Asked by: username_0 on 2016-06-25)

I am confused. I think I've read two usages of the word "impredicative" in type theory:

1. When people talk about the "impredicative" version of Martin-Löf's type theory, which they say it is inconsistent. Apparently they call it impredicative because of Type : Type.
2. When people talk about the "impredicative" Prop in CoC. Apparently they call it impredicative because you can quantify over Prop and get Prop stuff.

Is it the case? One notion of impredicativity implies the other? Is there no problem (i.e. inconsistency) by assuming "Prop impredicative"?

**Tags:** type-theory, calculus-of-constructions
> **Comments:**
> **username_1**: http://adam.chlipala.net/cpdt/html/Universes.html should be useful.  
> **username_2**: https://en.wikipedia.org/wiki/Impredicativity  
> **username_2**: https://math.stanford.edu/~feferman/papers/predicativity.pdf  

---

## 2 answers

### Answer by username_3 on 2016-06-25. Score: 8

The definition of an object $X$ is **impredicative**, if the definition uses a collection $C$ in the construction of $X$, such that $X$ is a member of $C$. So impredicativity is a form of **circularity**.

We are wary of circular definitions because they are often paradoxical. Fortunately it turns out that not all forms of
circularity are (or appear to be) problematic. The most famous example of an impredicative definition that is circular, but (as far as we know) not contradictory is the definition of natural numbers in set theory:

$$
\mathbb{N}\ \stackrel{\text{def}}{=}\ \bigcap \{X\ |\ X\ \text{is an inductive set}\}
$$

where a set is inductive if it contains $\emptyset$ and
is closed under the set-theoretic successor operation. Clearly, $\mathbb{N}$ is itself inductive, hence what you define on the left already occurs in some sense on the right.

By the "impredicative version of Martin-Löf's type theory" I guess you mean the type theory in his 1971 manuscript "*An intuitionistic theory of types*". This system has an impredicative axiom that stipulates a type of all types. For this reason the system is often simply called "*type:type*". This axiom is too strong as J.-Y. Girard showed, as it makes the type-theory inconsistent.

In contrast, the impredicativity in the CoC is not (known to be) inconsistent.

In some sense there are two forms of impredicativity: those that are known to be paradoxical, and those that are not.

> **Comments:**
> **username_2**: I don't think the definition of N is impredicative in set theory. The infinity axiom simply states that there is an inductive set. N is defined as the smallest inductive subset of that inductive set IIRC, not defined as the intersection of all inductive sets.  
> **username_3**: @Kaveh How do you define "smallest inductive subset" in a predicative way in ZF?  
> **username_2**: We don't need to define $\omega$ as the smallest inductive set, it is proven to have that property. We can define $\omega$ to be the smallest inductive subset of the inductive set that the infinity axioms states its existence.  
> **username_3**: I don't see how this definition of $\omega$ can be carried out in ZF in a predicative way.  
> **username_2**: ps: I just checked Jech, Enderton, and Kunen's books, they do define $\omega$ as you said. But as I said this is not really needed, when defining using intersection you can get rid of impredicativity and make it predicative if you start with an inductive set which the axiom of infinity tells it exists.  
> **username_3**: I would be interested in seeing the ZF formula that defines $\omega$ in a predicative way. I don't believe it can be done.  
> **username_2**: Here is an argument for the existence of a smallest inductive subset that I mentioned: let $X$ be the inductive set that axiom of infinity states its existence. Now let $N := \cap\{Y \in P(X) | Inductive(Y)\}$. We can show that it is subset of any inductive set $Z$ because the intersection of $Z$ and $X$ is inductive and in $P(X)$. The formula depends on the name of the inductive set that the axiom of infinity states its existence but if you give it a name then the formula is rather simple.  
> **username_2**: Is the issue that $P(X)$ contains N?  
> **username_3**: Yes. Your definition is impredicative as the set you are defining ($N$) already occurs on the something you use on the right hand side of the definition.  
> **username_3**: Let me give you a different example. If $S$ is a set of vectors in a vector space $V$ then $span(S)$ = $\bigcap \{W\ |\ S \subseteq W, W \ \text{subspace of}\ V\}$. This is the usual impredicative definition of the vector space generated by $S$. We can make it predicative by setting $span(S)$ = $\{\alpha_1v_1 + ... + \alpha_nv_n\ |\ 0 \leq n, \alpha_i \in \mathbb{R}, v_i \in S\}$.  I'm not sure how to carry out a similar 'predicativation' for $\mathbb{N}$ in ZF.  

---

### Answer by username_4 on 2017-03-06. Score: 7

In a system where Type:Type, the typing rule for the product would be trivial:

$$\frac{\Gamma \vdash A:Type\hspace{1cm} \Gamma, x:A \vdash B:Type}
{\Gamma \vdash \forall x\!:\!A.B : Type}$$

Unfortunately, Type:Type is known to be inconsistent, and Type must
inhabit some different sort, say Type:BigType. Then, the following case of the
product becomes problematic:

$$\Gamma \vdash A:BigType\hspace{1cm} \Gamma, x:A \vdash B:Type$$

You may either conclude that

$$ (\*)\;\;\Gamma \vdash \forall x:A.B : BigType$$

or

$$ (\*\*)\;\; \Gamma \vdash \forall x:A.B : Type $$

The first approach, where you take the maximum among the type of A and
B is the so called predicative approach, giving rise to a strictly
stratified type theory. This is indeed consistent with our intuition of
types as data structures.

The second approach is "impredicative": since Type:BigType, if B:Type, we get

$$ \forall X\!:\!Type.B: Type$$

but this expression is quantifying over a collection of items (Type)
comprising the product type we are defining as one of its elements.

Note however that is not so unreasonable in case you are interpreting Types as
propositions: if $B:Prop$, then $\forall X\!:\!Prop.B$ looks like a legitimate, higher order
proposition, hence it looks quite "natural" (for everybody who is not a
constructivist) to conclude that
$\forall X\!:\!Prop.B : Prop$

In fact, (\*\*) is not inconsistent (system F adopts this rule).
The only price you have to pay is that you must renounce to have strong
elimination rules. In Coq terms, you
cannot extract from a proposition anything but a proof of some other
proposition. As a corollary, you have no way in Coq to prove that two proofs of a same proposition are different from each other.


---

