I'm brand new to Coq and working through Mike Nahas's tutorial here: nahas_tutorial.v. Specifically, I'm having trouble understanding the statement given below:
Theorem forall_exists : (forall P : Set -> Prop, (forall x, ~(P x)) -> ~(exists x, P x)).
Here's my interpretation so far, corrections welcome.
The statement Set -> Prop is a proposition which can be expanded to forall s: Set, Prop which I understand as "for every proof (read instance) of a Set, we also have a proof (instance) of a Prop".
Thus forall P : Set -> Prop can be roughly read as "for every proof that a set gives rise to a proposition".
Then for (forall x, ~(P x)), my guess is that x is inferred to be of type Set by Coq, and that it's read as "every set gives rise to an unprovable/false proposition".
And for ~(exists x, P x), I read that as there exist no sets which imply the existence of a true proposition under P.
These seem logically equivalent. I'm just struggling with the language. Can P be interpreted as a function which maps from the space of sets to the space of propositions? I've used the phrases "give rise to" and "imply existence of"; is this correct? Is there a more correct way to state this?
Thanks for any and all assistance!
EDIT: For anyone who has a similar question, my confusion mostly amounted to an ignorance of the Curry-Howard isomorphism.
My interpretation (perhaps still a bit shaky) is now that the theorem reads "For every predicate (boolean-valued function) P ranging over elements of type Set, if the image of every set under P is false, then there's no set for which P yields True."
Set -> Prop belongs to Type, not Prop. When you're in Type, X -> Y should be read as a function from X to Y, and when you're in Prop, it should be read as X implies Y (though by Curry-Howard these are the same).
When a function returns a Prop it's usually considered a predicate or a property. So forall P : Set -> Prop can be read as "for every Set-valued property..."