The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hello,

I think Kirill's question is *why* impredicativity, and not *what* is 
impredicativity. In other words, can't we work with just Type instead of 
Prop? Does an impredicative universe add more expressiveness?

In practice, the answer is no, Prop does not add more expressiveness. You 
could do almost everything you already do in Type instead of Prop. However, 
that would be much less practical. For example, you will need multiple 
versions of the logical connectives False, /\, \/, ... at every Type level. 
Declaring only one version of False at a high Type level would not solve the 
problem, because you need to be able to deduce any "proposition" from False, 
in particular False itself. Universe polymorphism might alleviate that issue, 
but it is a relatively new feature.

Moreover, as mentioned by Kristopher, there are restrictions on Prop types 
since impredicativity can easily lead to inconsistencies. As a result, since 
Prop types are irrelevant, they can always safely be erased during program 
extraction, while doing the same for types in Type would require a more 
careful and complicated analysis.

There might be some complex statements that cannot even be expressed without 
an impredicative Prop, but I cannot think of one. Maybe experts in logic can 
answer that one.

Regards,

Ali

----- Mail original -----
> De: "Jonas Oberhauser" 
> <s9joober AT gmail.com>
> À: 
> coq-club AT inria.fr
> Envoyé: Dimanche 9 Février 2014 15:24:16
> Objet: Re: [Coq-Club] impredicativity of Prop
> 
> Am 07.02.2014 15:27, schrieb Kirill Taran:
> > Hello,
> >
> > Why we need impredicativity of Prop?
> > Also, is there difference in expressivity between Coq and Agda due
> > difference in predicativity of Prop (in Agda everything is
> > predicative)?
> 
> Hi Kirill,
> 
> Impredicativity means, informally, that if you create a proposition
> that
> talks about all propositions, it also talks about itself.
> 
> In Coq this is implemented by the (informal...) typing rule
> 
>    A : U         x : A => B : Prop
> -----------------------------------
>        forall x : A , B : Prop
> 
> 
> In particular, if  A = Prop (and U = Type_0), you get:
> 
> (forall x : Prop ,  B) : Prop
> 
> Thus, you could instantiate x with (forall x : Prop ,  B).
> 
> For types this doesn't work, as the term would automatically have
> type U
> (or higher). For the formal typing rules, refer to:
> http://coq.inria.fr/doc/Reference-Manual006.html#sec167
> 
> Kind regards, jonas
>