The Coq mailing list

["Roland Zumkeller" <Roland.Zumkeller AT polytechnique.fr>]

On 23/11/06, Haoyang Wang <hywang AT pobox.com> wrote:

On 11/23/06, Klaus Ostermann <ostermann AT informatik.tu-darmstadt.de> wrote:
> 1) What is the technical difference between Prop and Set? The tutorial and
> the book contain a few paragraphs that look like "philosophical" differences
> (e.g., regarding proof irrelevance), but is there also a technical
> difference? I.e., a situation where I can only use Prop but not Set or vice
> versa.

Prop is impredicative, while Set is predicative (stratified). That is,
(forall x:Prop, P x) is itself still a Prop, while (forall x:Set, P x)
belongs to a different Type universe.

Proof Irrelevance does have a technical (rather than philosophical)
meaning. It means any two proofs of the same Prop type are equal. That
is, forall (P:Prop) (x y:P), x = y.

It should be added that inductives (with more than one constructor) of sort Prop cannot be eliminated while constructing objects of type Set. This corresponds to the intuition that Set is for computation, while Prop is for reasoning.

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/