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. If you point is that the result you get is: ¬ ⊢ (...) instead of ⊢ ¬ (...) then this is true, but the former is what was originally claimed (there are no total functions of that type ==> that proposition is not a theorem). In fact, if one can prove the second, then we're in trouble, because the proposition is a classical theorem, and djinn provides a result for ⊢ ¬ ¬ (...) which contradicts the second statement above. -- Dan