The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

Edsko de Vries wrote:
>> I have chosen unfortunate notation. I thought, it is obvious. E was
>> meant as a "environment" (set of hypotheses) from which we want to prove
>> succedent. E is not a proposition.
> 
> What is the difference? :)
> 
> Edsko
> 

Aha, there is probably nothing wrong with E.

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).