Lennart Augustsson wrote:
Yes, of course you have to trust Djinn to believe its proof.
That's no different from having to trust me if I had done the proof by hand.
Our you would have to trust yourself if you did the proof.
True, though I think I didn't make my point clearly.
The question is, when can we consider a proof of (\forall x. ~ P x) as a
valid *constructive* proof of (~ \exists x. P x)?
If you tell me you've checked every x and found none supporting P, and I
believe you have the capability to have done so, and I believe things
you say are true, then I may take your statement that (\forall x. ~ P x)
and prove to myself that (~ \exists x. P x). However, my proof ---no
matter how much I believe it--- is not the sort of thing I can pick up
and hand to someone else. If they do not trust your diligence, then they
have no reason to trust my proof. I haven't constructed a witness to the
proposition, I've only convinced myself of it.
If, however, you construct a proof of (\forall x. ~ P x) which shows
that all options have been exhausted, but does so in a finite way that's
open to inspection and analysis, well then that's a different story. In
this case, because we've actually constructed some mathematical object
that we can poke and prod to understand what it is and how it works, we
do have something that we can hand to a skeptic to convince them. We
needn't argue from authority or put our faith in an elder or prophet,
the proof stands on its own.
When someone says "prove it", it's not always clear whether they mean
they want to be convinced it's true, or whether they mean they want
concrete evidence that witnesses its truth. Exhaustive search may be
convincing, but it's not constructive. When the OP was asking how we'd
go about proving that no total function exists with a particular type, I
was assuming they were seeking a witness rather than a convincing. For a
witness, I'd think you'd have to reason from parametricity, understand
the process that Djinn is automating, or similar; just running Djinn is
Haskell-Cafe mailing list