The Coq mailing list

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

On 09/06/2013 07:27 PM, Satrajit Roy wrote:
> Why can't I prove:
> forall p:Type->Prop, ~(forall q:Type, (p q))->(exists q:Type, ~(p q))
> When I can easily prove:
> forall p:Type->Prop, exists q, ~p q->~forall q, p q

To expand on the answer from t x, or come at it from a different angle:

You can't prove the first one because it isn't true. :P  [<-- 
tongue-in-cheek answer]

Newcomers often assume that there is one uncontroversial notion of 
logical truth, which all theorem-proving tools must implement.  In fact, 
there are some points of contention, like whether a logic is 
_constructive_ or _classical_.  Coq's is constructive, though you can 
make it classical by assuming the right axioms.  The first formula above 
is unprovable in constructive logic, which has a fundamentally 
computational flavor, such that it wouldn't make sense for a procedure 
to exist of the type you gave.  (A famous idea called the Curry-Howard 
Isomorphism explains how to interpret formulas as the types of 
functional programs.)

For more information on this distinction, there are many sources, and I 
try to explain it in CPDT <http://adam.chlipala.net/cpdt/>.