8
$\begingroup$

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"?

|cite|improve this question
$\endgroup$
5
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kaveh Jun 26 '16 at 6:20
  • 1
    $\begingroup$ @Kaveh How do you define "smallest inductive subset" in a predicative way in ZF? $\endgroup$ – Martin Berger Jun 26 '16 at 10:58
  • $\begingroup$ 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. $\endgroup$ – Kaveh Jun 26 '16 at 11:11
  • 3
    $\begingroup$ 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. $\endgroup$ – Martin Berger Jun 26 '16 at 12:04
  • 7
    $\begingroup$ 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. $\endgroup$ – Martin Berger Jun 26 '16 at 12:13
5
$\begingroup$

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.

|cite|improve this answer
$\endgroup$

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.