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)?
Thinking about this a little, I think I might have gotten confused with how you can use a solution to the halting problem to estblish the truth or falsity even of some unprovable propositions in some given system – if the halting checker says some proof-program doesn’t halt, and the theorem to be proven is of the form of the Goldbach conjecture, I’d still know it to be true, since otherwise, a counterexample – and hence, a proof of its falsity – could be found; however, if it is of the form of the Twin Prime conjecture, the non-halting result does not tell me anything.
Right; the Goldbach conjecture is what’s known as a Pi-1 conjecture, which means that it can be expressed in the form “This program never halts” (e.g., a program that goes looking for a counterexample), and thus a machine which settles the halting problem settles it. However, the Twin Prime conjecture is a Pi-2 conjecture, which means it can be put in the form “This program outputs a stream of programs, each of which in turn never halts”; you can’t settle this with a mere solver for the plain old halting problem. To settle this, you need to solve the new halting problem for machines equipped with a solver for the plain old halting problem; it’s one step up.
In other words, it is conceivably the case that, whatever formal proof system you have in mind, the Twin Prime conjecture is true and unprovable, and it is just as conceivably the case that the Twin Prime conjecture is false and unprovable, so that merely learning about its unprovability from whatever system does not settle the issue.
You could set up two programs that systematically generate theorems and always derive every theorem eventually. Have one halt when a proof of the twin prime conjecture is found and the other halt when a disproof (proof of negation of the conjecture) is found.
What if you put them through the halting checker and it proves that neither ever halts?
Your exhaustive proof-searcher would just tell you whether the statement is provable, not whether it’s true. If it’s provable, then it’s true, assuming you’re starting with a sane set of rules, and likewise if it’s disprovable then it’s not true, but there are a great many statements which cannot be proven nor disproven, and for those, you just don’t know.
On the Twin Prime Conjecture, by the way, your halting-oracle by itself might not be enough, but if you build your halting-oracle into a computer system (so effectively, your programming language has a function that takes in a program as input and returns “true” or “false”), and then you build a new oracle device to solve the halting-problem for that new computer, I’m pretty sure that’s enough. First, you write a program that takes an input N, and halts if it finds a pair of twin primes above N, or continues forever otherwise. Then, you feed that into your first-order oracle. Then, you write a program in your meta-language that incorporates the first-order oracle, and increments N: It halts if it ever reaches an N for which the oracle says the first-order program doesn’t halt. And then you wave your second-order-oracle magic wand over that second-order program.
Indistinguishable’s post snuck in there before me. I’m pleased to learn, though not at all surprised, that there’s a term for that property of propositions like the twin-prime conjecture. I’d stumbled across that myself. I imagine, though, that it’s not actually known whether the twin-prime conjecture can be converted somehow to a form that’s pi-1.
Right. In general, an Nth-level halting problem solver lets you compute predicates of quantifier complexity N (those which can be expressed in the form “y is such that for all x1, there exists an x2, such that for all x3, …, the computably decidable relation R holds of (y, x1, …, xn)”, where there are n many alternations of quantifier type). If one is interested only in propositions and not in predicates, one simply ignores the y; the Goldbach conjecture is then of quantifier complexity 1 (“For all n, n is either odd, 2, or the sum of two primes below it”), while the Twin Prime conjecture is of quantifier complexity 2 (“For all x, there exists a y such that y > x and y and y + 2 are both prime”).
No one knows of any reduction of the twin prime conjecture to a Pi-1 form, though of course a proof one way or another would reduce it even further, to quantifier complexity 0 (things which are straight-up computably decidable).
Incidentally, the study of what is computable with higher- and higher levels of halting problem oracles (and other things besides) is the study of the Turing degrees, should you be interested in learning more about them.
Well, let me be a bit more precise: If a statement is of quantifier complexity N, using a string of quantifiers starting with “for all”, it’s considered Pi-N. If it’s of quantifier complexity N, using a string of quantifiers starting with “there exists”, it’s considered Sigma-N. If it’s equivalent both to a Pi-N statement and to a Sigma-N statement, it’s considered Delta-N.
An oracle for the Nth-level halting problem allows you to decide precisely the Delta-(N+1) predicates, no more and no less. These include all the Pi-N predicates (and all the Sigma-N predicates, these just being the negations of the Pi-N predicates), but some more on top of that as well. (It’s not too hard to prove this yourself, but it’s known as Post’s theorem.)
To be absolutely clear here, Delta(N) would be a subset of Delta(N+1), right? Because it’s trivial to turn a higher-level oracle into a lower-level oracle.
Yes; Delta-N is the intersection of Pi-N and Sigma-N, and is a proper subset of each (except, the way I’ve defined it, when N = 0, as Delta-0 = Pi-0 = Sigma-0 = the computable). Pi-N and Sigma-N are in turn distinct proper subsets of Delta-(N+1) (except, again, when N = 0; in fact, it’s easy to see that Delta-1 = the computable as well), and it continues in this manner all the way up [and into the transfinite, for that matter, through the computable ordinals].
Just noticed this typo: this was supposed to read “This program outputs a stream of programs, none of which in turn never halts”; i.e., this program never outputs a program that never halts (of course, as the later discussion of quantifier complexity should’ve made clear, there are other ways to characterize Pi-2 as well; e .g., “This program halts on all inputs”, or “This program equipped with an oracle for the ordinary halting problem never halts”, or even just “This program beeps infinitely many times”).
Thanks for clearing up my confusion, folks. One day, I should get my hand on a good textbook on these matters, rather than just browsing through scattered online resources…
Note that any Π[sub]2[/sub]-complete problem is still unsolvable given a Halting Problem oracle. It is no doubt unlikely (and I wouldn’t be surprised if it’s been proven) that the twin prime problem is not Π[sub]2[/sub]-complete. But a host of other problems are. In computing, the question of “Does this program halt on all inputs?” is Π[sub]2[/sub]-complete. (It’s a tremendously hard problem, even for trivial programs.)
No doubt some universal question involving infinite number of solutions for Diophantine equations, for example, is Π[sub]2[/sub]-complete.
(“Π” in the above is “Pi” in case your browser can’t render it.)
Right; the problems computably decidable relative to an oracle for the ordinary halting problem are precisely those which are both Σ[sub]2[/sub] and Π[sub]2[/sub] (i.e., Δ[sub]2[/sub]).
On the other hand, the problems computably decidable relative to C[sub]2[/sub] (equivalently, with an oracle for a CC[sub]2[/sub]-complete problem) are those which are both Π[sub]3[/sub] and C[sub]3[/sub] (i.e., Δ[sub]3[/sub]). Indeed, the prototypical Π[sub]2[/sub]-complete problem is (the complement of) the 2nd-level halting problem itself.
In general, to be decidable relative to X is to be both semidecidable and co-semidecidable relative to X, and to be semidecidable relative to X is to be part of Σ(X) (accordingly, co-semidecidable relative to X is Π(X)); the halting problem relative to X is always in Σ(X) but not Π(X), and is always complete for Σ(X) [in the sense of many-one reduction].
Er, those 'C’s shouldn’t be there. Corrected version of the above post:
Right; the problems computably decidable relative to an oracle for the ordinary halting problem are precisely those which are both Σ[sub]2[/sub] and Π[sub]2[/sub] (i.e., Δ[sub]2[/sub]).
On the other hand, the problems computably decidable relative to Π[sub]2[/sub] (equivalently, with an oracle for a Π[sub]2[/sub]-complete problem) are those which are both Π[sub]3[/sub] and Σ[sub]3[/sub] (i.e., Δ[sub]3[/sub]). Indeed, the prototypical Π[sub]2[/sub]-complete problem is (the complement of) the 2nd-level halting problem itself.
In general, to be decidable relative to X is to be both semidecidable and co-semidecidable relative to X, and to be semidecidable relative to X is to be part of Σ(X) (accordingly, co-semidecidable relative to X is Π(X)); the halting problem relative to X is always in Σ(X) but not Π(X), and is always complete for Σ(X) [in the sense of many-one reduction].
Stop that, Indistinguishable; you’re making me want to go back to grad school. I remember that I had good reasons for quitting, but I get excited reading posts like yours and can’t remember what they were.