coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ali Assaf <ali.assaf AT inria.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] impredicativity of Prop
- Date: Wed, 12 Feb 2014 11:25:53 +0100 (CET)
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
>
- [Coq-Club] impredicativity of Prop, Kirill Taran, 02/07/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/08/2014
- Re: [Coq-Club] impredicativity of Prop, Jonas Oberhauser, 02/09/2014
- Re: [Coq-Club] impredicativity of Prop, Ali Assaf, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Altenkirch Thorsten, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Kirill Taran, 02/13/2014
- Re: [Coq-Club] impredicativity of Prop, Altenkirch Thorsten, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Matthieu Sozeau, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Ali Assaf, 02/12/2014
- Re: [Coq-Club] impredicativity of Prop, Kristopher Micinski, 02/08/2014
Archive powered by MHonArc 2.6.18.