The Coq mailing list

[Andrew Hirsch <akhirsch AT cs.cornell.edu>]

I think an important thing to understand here is why coq makes this impossible to prove. Imagine that I told you that I had something that you didn't believe I had. If you wanted proof that I had this thing, you'd probably want to see the thing itself! After all, other evidence you could give me could be faked. Furthermore, you'd probably want some evidence that it is what I say it is, like a certificate of authenticity or a receipt.

This is exactly what Coq is trying to do here. In order to prove something exists to Coq, you should give it that thing, and provide a proof that it is what you want. To be more precise, a proof that exists x : A, P x is a pair (a, P a), consisting of a : A and a proof P a that a has the property P. The proof rule you give would get around that. Allowing this can create all sorts of weird things. In classical set theory, it allows the Banach-Tarski Paradox, which says that there is a function which will take a sphere, divide it into sections, and then reorganize those sections into two spheres of the same size as the original. (This also requires the axiom of choice, which is equivalent to P \/ ~P in set theory.) What this function is, no one can tell you. To a constructivist, that's not good enough.

- Andrew

On Sat, Sep 7, 2013 at 9:08 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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