Does the unsolvability of the halting problem imply the existence of Turing machines which cannot be proven either to halt or not halt?

Question

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.

Answer 1

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 similarly reverse-engineer a "Gödel algorithm" for that theory. And of course, if ZFC were not to be consistent, then all of these stronger theories which prove its consistency would be inconsistent as well, which would topple the entire house of cards.

That doesn't mean your question has no answer. It does mean that you have to figure out what kind of "proof" would satisfy you. For instance, we could trivially prove that some Turing machine halts by simply stating it as an axiom: Turing machine T halts, formalized somehow or another. This would be a formal system of logic which does prove that T halts, but it would be silly. An even worse example is just to look at the algorithm TRUE, which just returns "true" and accepts any input. This will, through sheer random chance, correctly assess the halting status of any program which really does halt, if sent in as input - also silly.

Some deep thought is required to determine what you would view as a valid proof system: something where we haven't baked the answer to the haltingness of individual Turing machines into the axioms, but which are somehow derivable from some basic first principles. If you can actually figure out how to phrase that question in a rigorous way - and I'm not sure how - then you can ask if, for any candidate Turing machine $T$, some consistent proof system does exist which has whatever properties you are looking for, and which correctly proves if $T$ will halt.

Answer 2

Great question! To try to give a slightly shorter answer:

Fist, we know that for any formal system, no matter how powerful, there are TMs A and B such that A cannot be proven to halt on B. Given your argument, how can this be?

To be concrete, we can define "provable" formally as "provable in ZFC" (any other powerful axiomatic system would work, too). When that is done, your argument is actually correct (!), but doesn't show what you think it shows.

What you have showed is that:

• IF there is a TM A and an input B, such that it is impossible to prove in ZFC whether A halts on B
• THEN A does not halt on B.

However, the flaw in your argument is "A is proven to not halt". We only showed that A does not halt, not that it is provable that that is so.

It is useful to denote "provable" with a box symbol: $\square$. You first assumed, towards a contradiction, that $$ \lnot \square P \land \lnot \square \lnot P $$ You then correctly observed that, where $P$ = A halts on B, $$ P \to \square P $$ from which it follows (correctly!), using the contrapositive and $\lnot \square P$, that $$ \lnot P $$

But it does not follow that $\square \lnot P$. Godel's theorems show that there are for any formal system, statements that are true, but not provable in that system. So unfortunately, we cannot make this final leap in your argument.