The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hello,

  I think impredicativity of Prop adds some practical logical expressiveness. 
There are practical things you can do with Prop but not predicative types, for
example, Prop has a complete lattice structure so you can express fix point 
theorems
using it (see for example the Paco library for “logical” coinduction 
principles
using this). Proof-theoretically, this translates to extra power. If I’m not 
mistaken,
CIC is stronger than Agda in this respect (ignoring large inductive-recursive 
universes in Agda).

Best,
— Matthieu

On 12 févr. 2014, at 11:25, Ali Assaf 
<ali.assaf AT inria.fr>
 wrote:

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