The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

In order to define the tarski fixed point, you need the impredicativity of 
Prop.

The following works.
===========================================
Definition powerset (A: Type) := A -> Prop.

Definition lfp A (f: powerset A -> powerset A) : powerset A :=
  fun a => forall P, (forall a, f P a -> P a) -> P a.
===========================================

But, if you change Prop to Type, then you get university inconsistency.
===========================================
Definition powerset (A: Type) := A -> Type.

Definition lfp A (f: powerset A -> powerset A) : powerset A :=
  fun a => forall P, (forall a, f P a -> P a) -> P a.
Error: Universe inconsistency.
===========================================

Cheers,
Gil

On Wed, Jul 25, 2012 at 4:23 PM, Benjamin C. Pierce
<bcpierce AT cis.upenn.edu>
 wrote:
> What is the most elementary example showing why we want Prop to be 
> impredicative?
>
> Thanks!
>
>     - Benjamin
>