The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/25/2012 10:23 AM, Benjamin C. Pierce wrote:
> What is the most elementary example showing why we want Prop to be 
> impredicative?
>    

I'd say the simplest (but dubious) example has to do with propositional 
logic meaning what it seems to be taken to mean in informal math.  
However, IMO this is dubious for the same reason that it's dubious to 
worry about duplicating ZF proofs exactly in Coq.

Definition ModusPonens_Prop := forall P Q : Prop, (P -> Q) -> P -> Q.

Theorem ModusPonens_Prop_proof : ModusPonens_Prop.
  hnf; auto.
Qed.

Check ModusPonens_Prop_proof ModusPonens_Prop ModusPonens_Prop.

Definition ModusPonens_Type := forall P Q : Type, (P -> Q) -> P -> Q.

Theorem ModusPonens_Type_proof : ModusPonens_Type.
  hnf; auto.
Qed.

Check ModusPonens_Type_proof ModusPonens_Type ModusPonens_Type.
(* Error: Universe inconsistency. *)