Half Man Half Wit

07-06-2010, 11:22 AM

So, let's say I have obtained some kind of device that can infallibly tell me whether or not any given algorithm halts. It's often said that using this thing, one can easily tell the truth or falsity of any mathematical conjecture that is in a sense finitely refutable -- i.e. if, assuming that the conjecture is false, one can find a counterexample in finitely many steps. The Goldbach conjecture is a good example: if there is an even number such that it can't be written as a sum of two primes, a simple exhaustive search will eventually find it; thus, applying the halting checker to an algorithm implementing this search immediately decides the conjecture: if the algorithm halts, there exists a counterexample, and the conjecture is wrong, if it doesn't halt, the conjecture is true.

However, there are mathematical statements that aren't similarly finitely refutable (for example, the twin prime conjecture, which states that there are infinitely many twin primes, basically), and I seem to recall -- though I can't remember from where -- that this implies they can't be similarly checked through only the knowledge of the solution to the halting problem. I can't quite see why, though. Obviously, the method above won't work; however, I see no reason why one couldn't simply set up an exhaustive search through all the theorems of some axiomatic system, and check whether or not it ever turns up -- i.e. have a Turing machine just derive blindly from the axioms according to the rules of inference in such a way as to guarantee that every theorem is hit eventually, compare each result with the desired theorem, and halt if it is found; the halting checker applied to this procedure then decides whether or not the theorem can be derived immediately.

The only snag I could see this hitting is that it is perhaps not so easy to find out if the theorem has actually been derived -- i.e. if somehow the theorem might turn up, but not in a form the comparison routine recognizes as actually being the sought for theorem. But then, it seems to me a human attempting to find a proof for some theorem would be faced with the same difficulty. Besides, it seems to me that one should always be able to re-cast any formula in some reasonably easy to recognize form, something like the prenex normal form perhaps.

So what's the deal? Am I just remembering things wrong, and knowledge of the halting problem's solution does in fact enable one to prove everything mathematically provable, or have I missed something (probably dreadfully obvious)?

However, there are mathematical statements that aren't similarly finitely refutable (for example, the twin prime conjecture, which states that there are infinitely many twin primes, basically), and I seem to recall -- though I can't remember from where -- that this implies they can't be similarly checked through only the knowledge of the solution to the halting problem. I can't quite see why, though. Obviously, the method above won't work; however, I see no reason why one couldn't simply set up an exhaustive search through all the theorems of some axiomatic system, and check whether or not it ever turns up -- i.e. have a Turing machine just derive blindly from the axioms according to the rules of inference in such a way as to guarantee that every theorem is hit eventually, compare each result with the desired theorem, and halt if it is found; the halting checker applied to this procedure then decides whether or not the theorem can be derived immediately.

The only snag I could see this hitting is that it is perhaps not so easy to find out if the theorem has actually been derived -- i.e. if somehow the theorem might turn up, but not in a form the comparison routine recognizes as actually being the sought for theorem. But then, it seems to me a human attempting to find a proof for some theorem would be faced with the same difficulty. Besides, it seems to me that one should always be able to re-cast any formula in some reasonably easy to recognize form, something like the prenex normal form perhaps.

So what's the deal? Am I just remembering things wrong, and knowledge of the halting problem's solution does in fact enable one to prove everything mathematically provable, or have I missed something (probably dreadfully obvious)?