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 merely convincing. -- Live well, ~wren