Dan Doel wrote:
On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:
Sure, that's another option. But the failure of exhaustive search isn't
a constructive/intuitionistic technique, so not everyone would accept
the proof. Djinn is essentially an implementation of reasoning by
parametricity, IIRC, so it comes down to the same first principles.
How, exactly, is it non-constructive to encode the propositional calculus and
its proofs as, say, types in intuitionistic type theory, write the algorithm
djinn uses in the same (it was specially crafted to be provably terminating,
after all), and prove the algorithm complete (again, hopefully in the type
theory)? I realize this has not all been done, strictly speaking, but I see
nowhere that it is necessarily non-constructive.
All I'm saying is that a proof of (\forall x. ~ P x) does not constitute
a proof of (~ \exist x. P x) for some intuitionists. The issue is one
of the range of quantification and whether \forall truly exhausts every
possibility. The BHK interpretation says the two propositions are the
same, but others say the latter is a stronger claim.
If you believe that Djinn truly does exhaust the search space, then it's
fine to convert Djinn's proof of (\forall x. ~ P x) into a proof of (~
\exist x. P x). However, that just pushes the question back to why you
feel justified in believing that Djinn truly exhausts the search space.
I'm not saying you shouldn't believe in Djinn, I'm saying that belief in
Djinn is not justification for a theorem unless you have justification
for believing in Djinn.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
