The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

I think impredicativity is a classical artefact a consequence of thinking
that Prop = Bool, hence quantifying over all propositions is small.

The better way is to view Prop as the types which have no information
(HProp) that is at most one inhabitant. But then there are HProps at
different usniverses but I am not sure why this is a problem. I mean we
have x and + at every universe too.

Thorsten


On 12/02/2014 10:57, "Matthieu Sozeau" 
<matthieu.sozeau AT gmail.com>
 wrote:

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

This message and any attachment are intended solely for the addressee and may 
contain confidential information. If you have received this message in error, 
please send it back to me, and immediately delete it.   Please do not use, 
copy or disclose the information contained in this message or in any 
attachment.  Any views or opinions expressed by the author of this email do 
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, 
you are advised to perform your own checks. Email communications with the 
University of Nottingham may be monitored as permitted by UK legislation.