The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Wednesday 16 September 2009 11:13:01 am Adam Chlipala wrote: 
> The important difference of [Prop] vs. [Type] is that [Prop] is
> impredicative: you may define a [Prop] by quantifying over all [Prop]s.
> This is a natural thing to do, even in basic theorems about
> "propositional" logic, like this:
>     forall P : Prop, P -> ~~P
> This statement is itself a [Prop].  If you used [Type] instead of [Prop]
> everywhere (both in this statement and in the standard library), then
> the statement would exist at a higher universe level than the universe
> it quantifies over, so it wouldn't apply to itself.
> 
> To me, this justification is separate from the extraction restrictions
> that you asked about.  I think [Prop] (as opposed to impredicative
> [Set]) exists solely to enable extraction of efficient programs, so
> there's not so much detective work required about its justification as
> your question suggests.  Impredicativity in a type without [Prop]'s
> restrictions _is_ inconsistent with some popular classical axioms, so
> there's another reason.
>
> I think I've heard that Agda is purely predicative, but I might be wrong.

It is. However, one can pass a flag (--type-in-type) to make Set : Set, which 
would get you impredicativity as a corollary, I think, although Set : Set is 
stronger. With the latter you're able to construct analogues to Russel's 
paradox which let you prove false via non-termination:

  http://sneezy.cs.nott.ac.uk/darcs/Agda/test/succeed/Hurkens.agda

Obviously Prop isn't subject to this, as it'd be pretty useless if you could 
prove false propositions. However, it may be (though I'm not sure) that the 
non-computational aspect of Prop is what prevents one from being able to 
construct such pathological cases, despite being able to quantify over 
arbitrary higher universe levels. Someone with more knowledge than I have 
will 
have to say whether that's true or not, though.

-- Dan