The Coq mailing list

[Tillmann Rendel <rendel AT cs.au.dk>]

Matej Kosik wrote:
> However, I haven't expressed myself clearly enough in what direction I
> wanted to progress.
>
>         Lemma foo : (E -> p) -> (E /\ ~p -> False).
>
> helps in the direction I was not interested in.
>
> However, the following:
>
>         Lemma bar : forall P : Prop, (~ P -> False) -> P
>
> would help me to prove NNPP. Thus,  `bar' must be unprovable too without
> loading additional axioms from the classical logic (if NNPP is unprovable).

Recall the type of NNPP.

    NNPP : forall p : Prop, ~ ~ p -> p

Since (~x = x -> False) by definition of ~, this is the same as the type 
of bar. That means that a proof of bar *is* a proof of NNPP.

  Tillmann