debugMinor
Does the unsolvability of the halting problem imply the existence of Turing machines which cannot be proven either to halt or not halt?
Viewed 0 times
cannotproblemimplytheexistencewhichunsolvabilityhaltingeitherdoes
Problem
My understanding is that this statement regarding the halting problem is proven:
There does not exist any TM C that can, given a Turing machine A and input B as inputs, determine in a finite number of steps whether A halts on input B, and that works correctly for all A and B.
What I want to know is whether this related statement is also proven:
There exists some TM A and input B for which no analysis exists which can prove whether A will halt on B.
To my mind this seems to create a contradiction as follows:
Assume TM A and input B exist.
If A halts on B, it must do so in a finite number of steps - this is a property of Turing Machines in general. Therefore, if A halts on B, such can be proven by simulating A for a finite number of steps.
Because it is impossible to prove whether A(B) halts, A does not halt (because if it did, such would be provable).
A is proven to not halt, but was given the property of being unprovable as to whether it halts - this is (P ∧ ¬P), an apparent disproof by contradiction.
Have I misapplied a rule here, or is there an important aspect of this problem I'm missing?
I'm trying to understand whether the insolvability of the halting problem expresses a limit on the power of Turing Machines to solve or a more general unprovability of some true statements.
Edit:
What I'm getting from some helpful comments seems to be that the problem pretty quickly becomes degenerate in that "prove" can't be defined in a way that is both true to the intuitive sense of the word and formalizable.
There does not exist any TM C that can, given a Turing machine A and input B as inputs, determine in a finite number of steps whether A halts on input B, and that works correctly for all A and B.
What I want to know is whether this related statement is also proven:
There exists some TM A and input B for which no analysis exists which can prove whether A will halt on B.
To my mind this seems to create a contradiction as follows:
Assume TM A and input B exist.
If A halts on B, it must do so in a finite number of steps - this is a property of Turing Machines in general. Therefore, if A halts on B, such can be proven by simulating A for a finite number of steps.
Because it is impossible to prove whether A(B) halts, A does not halt (because if it did, such would be provable).
A is proven to not halt, but was given the property of being unprovable as to whether it halts - this is (P ∧ ¬P), an apparent disproof by contradiction.
Have I misapplied a rule here, or is there an important aspect of this problem I'm missing?
I'm trying to understand whether the insolvability of the halting problem expresses a limit on the power of Turing Machines to solve or a more general unprovability of some true statements.
Edit:
What I'm getting from some helpful comments seems to be that the problem pretty quickly becomes degenerate in that "prove" can't be defined in a way that is both true to the intuitive sense of the word and formalizable.
Solution
Elaborating from my comments above, here is at least one partial answer to your question:
As has been clearly known for about 100 years, there is no program that can correctly solve the halting problem 100% of the time, given any other program we want it to analyze. Or, at least, as Turing put it, such a program "cannot be a [Turing] machine." So, on the one hand, this would seem like a profound limitation for how powerful computers can ever get.
On the other hand, clearly people "solve the halting problem" for specific situations all the time. Every time you debug a program and realize that you need a mutex because your threads will deadlock, you have "solved the halting problem" for your program. Even something as mundane as proving a mathematical theorem is equivalent in strength to solving the halting problem, but grad students do it every day (first-order validity is RE-complete). And then there's the entire discipline of computational complexity theory: in order to determine the asymptotic complexity of any algorithm, the first step is to show that the worst-case running time is finite - meaning we have to show that it halts on all inputs - which is much harder than the halting problem! Yet we haven't given up on computational complexity as a useless endeavor. How does this work?
The first way to start making sense of this situation is to relax our constraints for the halting problem. We can look at programs which can correctly solve the halting problem for some subset of inputs. In this situation, we will say that we don't really care what the program does for programs outside of this subset: it can return the wrong answer, or not halt at all, or return a special error value; whatever you want. This is something like what humans do when we solve the above "real-world" problems: we have some subset of things we know how to analyze, and outside of that we basically give up. Of course, humans are even less rigorous than this; even when we look at some program which we do know how to analyze, there's always some chance we'll get it wrong anyway, or get stuck until we give up. But good enough.
The same, presumably, would be true for artificial intelligence algorithms: I really don't want to get into a huge debate about the future of AI here, but I will simply say that clearly, they are getting very good at writing and debugging code - including debugging bugs which could cause programs to deadlock, hang, or otherwise "not halt" - and they will also certainly get much better. However, they, like humans, can also screw up, or return an "I don't know" answer. Training (e.g. from GPT-3 to GPT-4) can increase the subset of situations these AI systems can correctly analyze. So again, the idea of looking at "partial oracles" which can solve the halting problem "sometimes," or "enough of the time for problems I care about," or etc, would seem to be relevant here as well.
Here is the subtlety with all of this: you have to determine what it actually means to "analyze" or "prove" that a program will halt at all. So, for instance, let's say you follow the majority of mathematicians and formalize your proof in ZFC set theory, such that a Turing machine is defined as a "set" of symbols, states, and so on, where the first+order ZFC axioms tell us what a "set" means. Then, you can go about looking for some mathematical proof of whatever it is you want to prove.
The main problem, here, is that if you start with ZFC - or any first-order proof system - we can reverse-engineer an algorithm that will never halt, but which ZFC will not be able to prove doesn't halt - unless ZFC is inconsistent and can prove anything, at which point we don't want to use it at all. I will call this algorithm the Gödel algorithm for ZFC, as it's really just a restatement of Gödel's famous incompleteness theorem in computer science-ish terms.
It's very simple: any mathematical proof formalized in something like ZFC is just a finite-length string of symbols on some alphabet. So we just enumerate through all strings, one by one - and at each step, we check if the current string happens to encode a valid proof that 1 = 0. If we have, then we have proven that ZFC is inconsistent. If ZFC is consistent, then no such proof string will exist, and this program will never halt.
We may ask if this particular program is an example of your Turing machine A. After all, the standard foundation of mathematics is insufficient to prove that it doesn't halt - unless the standard foundation of mathematics itself is logically contradictory. But this isn't the entire answer either. Just because ZFC set theory can't prove this, doesn't mean that nothing can prove it. We just can't prove it using ZFC itself - we need to go to a stronger theory which is able to prove this. In fact, a natural example of such a theory really does exist, which is ZFC plus the existence of a strongly inaccessible cardinal, or equivalently a "Grothendieck universe." But then, we can si
As has been clearly known for about 100 years, there is no program that can correctly solve the halting problem 100% of the time, given any other program we want it to analyze. Or, at least, as Turing put it, such a program "cannot be a [Turing] machine." So, on the one hand, this would seem like a profound limitation for how powerful computers can ever get.
On the other hand, clearly people "solve the halting problem" for specific situations all the time. Every time you debug a program and realize that you need a mutex because your threads will deadlock, you have "solved the halting problem" for your program. Even something as mundane as proving a mathematical theorem is equivalent in strength to solving the halting problem, but grad students do it every day (first-order validity is RE-complete). And then there's the entire discipline of computational complexity theory: in order to determine the asymptotic complexity of any algorithm, the first step is to show that the worst-case running time is finite - meaning we have to show that it halts on all inputs - which is much harder than the halting problem! Yet we haven't given up on computational complexity as a useless endeavor. How does this work?
The first way to start making sense of this situation is to relax our constraints for the halting problem. We can look at programs which can correctly solve the halting problem for some subset of inputs. In this situation, we will say that we don't really care what the program does for programs outside of this subset: it can return the wrong answer, or not halt at all, or return a special error value; whatever you want. This is something like what humans do when we solve the above "real-world" problems: we have some subset of things we know how to analyze, and outside of that we basically give up. Of course, humans are even less rigorous than this; even when we look at some program which we do know how to analyze, there's always some chance we'll get it wrong anyway, or get stuck until we give up. But good enough.
The same, presumably, would be true for artificial intelligence algorithms: I really don't want to get into a huge debate about the future of AI here, but I will simply say that clearly, they are getting very good at writing and debugging code - including debugging bugs which could cause programs to deadlock, hang, or otherwise "not halt" - and they will also certainly get much better. However, they, like humans, can also screw up, or return an "I don't know" answer. Training (e.g. from GPT-3 to GPT-4) can increase the subset of situations these AI systems can correctly analyze. So again, the idea of looking at "partial oracles" which can solve the halting problem "sometimes," or "enough of the time for problems I care about," or etc, would seem to be relevant here as well.
Here is the subtlety with all of this: you have to determine what it actually means to "analyze" or "prove" that a program will halt at all. So, for instance, let's say you follow the majority of mathematicians and formalize your proof in ZFC set theory, such that a Turing machine is defined as a "set" of symbols, states, and so on, where the first+order ZFC axioms tell us what a "set" means. Then, you can go about looking for some mathematical proof of whatever it is you want to prove.
The main problem, here, is that if you start with ZFC - or any first-order proof system - we can reverse-engineer an algorithm that will never halt, but which ZFC will not be able to prove doesn't halt - unless ZFC is inconsistent and can prove anything, at which point we don't want to use it at all. I will call this algorithm the Gödel algorithm for ZFC, as it's really just a restatement of Gödel's famous incompleteness theorem in computer science-ish terms.
It's very simple: any mathematical proof formalized in something like ZFC is just a finite-length string of symbols on some alphabet. So we just enumerate through all strings, one by one - and at each step, we check if the current string happens to encode a valid proof that 1 = 0. If we have, then we have proven that ZFC is inconsistent. If ZFC is consistent, then no such proof string will exist, and this program will never halt.
We may ask if this particular program is an example of your Turing machine A. After all, the standard foundation of mathematics is insufficient to prove that it doesn't halt - unless the standard foundation of mathematics itself is logically contradictory. But this isn't the entire answer either. Just because ZFC set theory can't prove this, doesn't mean that nothing can prove it. We just can't prove it using ZFC itself - we need to go to a stronger theory which is able to prove this. In fact, a natural example of such a theory really does exist, which is ZFC plus the existence of a strongly inaccessible cardinal, or equivalently a "Grothendieck universe." But then, we can si
Context
StackExchange Computer Science Q#159640, answer score: 4
Revisions (0)
No revisions yet.