What’s the relationship between Gödel incompleteness and the halting problem? Is either a stricter version of the other? And if not, is it possible that both are a stricter version of a more general principle that applies to a wider class of systems than either formal models of arithmetic and TM’s?
I ask because, from my limited understanding, it seems they must be related in some way, but I’ve read posts in this much earlier thread that suggest otherwise. Consider, for example, Goldbach’s conjecture, which some suggest might be a true but unprovable statement, the possibility of which is guaranteed by Gödel’s. However, it’s easy to create a Turing machine that halts iff Goldbach’s conjecture is false: just go through all integers one by one and halt if you find a counterexample. If Goldbach’s is true and unprovable though, then it must be that this is a TM that halts but cannot be proven to halt, the possibility of which is guaranteed by the halting problem. So it seems like the two ideas must be linked…
Also, to throw another spanner in the works, what about Turing oracles? If a first-order Turing oracle existed (solving the halting problem on TMs, but not its own halting problem), then it could clearly prove or disprove Goldbach’s. So does “unprovable” in Gödel’s really mean unprovable in finite time?
I am not a mathematician but I am a computer scientist, so I can speak with marginal authority on this. As far as I know, the Incompleteness Theorem and the Halting Theorem are not directly related, in that they were proved by different people using different approaches. Neither can really be considered a subset of the other.
On the other hand, they are similar, in that they refer to formal systems that can represent themselves recursively, and there is probably a general statement that could incorporate both of them.
By the way, it is trivial to create a Turing machine that halts. First instruction–halt. Done! The problem is to determine if a random Turing machine would halt with any input.
An excellent book on this subject, as well as many others, is *Godel Escher Bach: An Eternal Golden Braid *by Douglas Hofstadter. It is not easy going but it is very rewarding.
Cool, that’s exactly what I’m getting at…is there any research into what kind of statement that might be?
Yep, of course, but such a trivial machine can be proved to halt with a finite length proof. If Goldbach’s is true but unprovable, then presumably no finite length proof will show whether the TM described in the OP will halt or not. However, a Turing oracle would. Is this true in general? Can all true but unprovable statements be proved with a Turing oracle?
Actually, scratch that last part. Obviously, not all true by unprovable statments will be provable with a Turing oracle that solves the (first-order) halting problem. But regardless, I’d be interested if such a Turing oracle corresponds to any concept related to Gödel’s incompleteness…
Indistinguishable will be along soon enough, I’m sure, but from what I remember from previous threads, both Turing’s and Gödel’s theorems, as well as Cantor’s proof of the uncountability of the reals, are special cases of a more general theorem that can apply to a very wide variety of different contexts.
And there’s a hierarchy of unresolved problems based on what sort of oracle would solve them. Many interesting problems would be solved by a first-order oracle that can solve the Halting Problem for Turing machines. Then you could have a second-order oracle, that can solve the Halting Problem on a system of Turing machine plus first-order oracle, and higher-order oracles according to the same pattern. IIRC, the Twin Prime Conjecture would (so far as anyone can tell) require a second-order oracle to resolve it, though I don’t know of any problems offhand that would require a third-order oracle (they doubtless exist, though).
Ahh, ok, thanks Bytegeist. Unfortunately that thread is similar to the one that I linked to in my OP, in descending into a heated debate…
Anyway, I gather from reading that thread that statements which are neither provable nor disprovable within a system are (usually/always?) due to them implicitly encoding some form of self-reference within them, and that Gödel’s in particular shows that, in the case of any system obeying the axioms of Peano arithmetic, and that they may be very well hidden as apparently simple statements of pure arithmetic.
Ok, this is really interesting. I’m just going out on a limb here (and please excuse my sloppy language), but would it make sense to say that every level of Turing oracle-ness peels away another “layer” of problems from the space of all problems, making them computable, like peeling all layers of some (very transfinite) onion. As you add more and more layers of oracle-ness, you will be able to compute the answers to more and more problems, however, but the set of problems which you cannot solve will approach some steady set?
If that’s the case, then what would this final set of problems that you cannot solve look like? Would they all be very trivial forms of self reference? Basically, would an infinite-order Turing oracle be able to solve anything that wasn’t a “clear” (for some definition of clear) paradox (similar to the problem of asking God to create a rock so heavy that even He could not lift it, to throw in a metaphor)
Just a baseless hunch, but if you assumed a countably infinite Turing machine, someone would probably come up with a problem requiring an uncountably infinite Turing machine (whatever that is).
(Actually, my hunch is that both of those have already occurred.)
Actually, the Halting Problem and the Incompleteness Theorem are pretty closely related. The basic outlines of their proofs are very similar essentially using the same diagonalisation trick, and the Halting Problem can be viewed as a theorem that, though it appeared in the literature later, is actually a conceptual predecessor of the Incompleteness Theorem. Indeed, if you have the notion of Turing Machine handy, as well as a proof of the Halting Problem, a strengthening of the Incompleteness Theorem in the form of Rosser’s Theorem falls out as a corollary.
Capt. Ridley is absolutely correct. For one thing if the halting problem for a machine is undecidable, then so is the conjecture that it halts. And that can be coded in Goedel arithmetic. I’m pretty sure you can go the other way too, code an arithmetic statement into a halting problem. And they certainly have the same “feel”.
This is borne out in Michael Sipser’s book on computation theory, where he derives the incompleteness theorem pretty easily from the basic notions of uncomputability. But just out of curiosity, is there any insight to be gained by looking at the two statements in light of Curry-Howard?
That’s great, and confirms my initial intuition that the two are related. But according to Indistinguishable, Gödel’s goes further than simple uncomputability and implies that statements exist that can’t be proved or disproved by any level of Turing oracle-ness. Anyone have any idea what kind of statement that would be?
Also, I’ve seen mentioned the idea of Gödel sentences, but I don’t really understand quite what they are. Would a Gödel sentence for a particular system be encodable as a particular TM, or does that not make sense?
There’s a fixed-point theorem originally due to Lawvere that incorporates basically all the classical paradoxes of self-reference – it’s discussed and explained in this pedagogical paper.
I think it’s also useful to refer to the work of Chaitin, who showed that the halting probability of a Turing machine, and uncomputable number, can by any given formal system only be approximated to a finite degree – i.e. after some certain bit in the binary expansion of the halting probability, the value of any following bit isn’t derivable. This is a statement of the incompleteness theorem, and it follows directly from the fact that if you could derive all the values of all the bits of the halting probability, you could also solve the halting problem. (See here for an overview.)
Not that I’m aware, or at least I don’t see any deep rephrasing of the two subjects in those terms. Curry-Howard discusses the analogy between typed lambda-calculi and intuitionistic logics (and player-opponent games, and categories, and …). The typed lambda-calculi in question almost always are strongly normalizing (in fact, I’d argue for there to be any interest in the correspondence they must be at least weak head normalizing), and therefore there’s no corresponding halting problem.
The book recommended above, GEB does a good job of showing you how to construct a Godel sentence.
Essentially, the process he goes through (as far as I remember) is:
Using several simpler languages as building blocks, he constructs a language in which you can make statements about number theory (ie, “three is a prime number”, “there are no a,b,c,n >2 for which a^n + b^n = c^n”, “2 > 7”), which can be either true or false, using a fairly restrictive set of symbols.
He establishes a set of typographical rules and axioms for generating theorems in this language, ie, sentences that are true, without ascribing meaning to the manipulation. That is, you can take one or more true statements and generate new ones without
He encodes the symbols used in the language in step one into numerical form.
He demonstrates that the typographical rules derived in step 2 are actually mathematical rules; the combination of some string(s) symbols to create another string of symbols, when encoded as numbers, is basically shifting (multiplying by a factor of 10^n) and addition, which are mathematical operations that the language itself can describe.
He constructs a sentence (in number form), that, when translated back to the symbols, is a statement about the number form of that sentence, and which includes a contradiction. Since this sentence can be neither true nor false within the context of the given system, the system is incomplete.
Note that the Godel sentence is the sentence that proves Godel’s theorem. It’s not necessarily the only way to make a statement within a given system that can neither be proven nor disproven.