Now, there are finite state systems where the halting problem is arbitrarily hard. But that's not undecidability. That's complexity. That's a problem in the space where P=NP lives.
The article does not make this distinction, and it's important.
If you give me a decider that can tell me for any program with a state space up to size N whether it halts or not, then I will be able to produce another program with a larger state space and which then your decider won't be able to decide. This new program doesn't use infinite space. Just more than your decider can handle. You can't produce a single decider that works for all inputs.
It is often ok to approximate "finite but unbounded" with "infinite", and surely anyhing that can handle infinite inputs will be able to handle finite-but-unbounded inputs too, but in this context the two are not the same.
The term "infinite" is often misused to mean "finite but unbounded" but it is an important distinction.
We have cycle detection algorithms that don't require saving all states and work in the same big-O space complexity (constant factor overhead) as just running the input system normally without cycle detection.
To my understanding that means that, for any input system that runs in finite-but-unbounded space, the detector will determine whether it halts in finite-but-unbounded space - unless I am misunderstanding that term.
We can construct a new turing machine F(TM) = D(TM, TM). That is: We ask D to detect a cycle when a TM receives its own encoding as an input. What is the output of F(F)?
F(F) = D(F, F) = 1 can only happen if your cycle detector detected a cycle in F(F) which we just saw terminates with 1. If F(F) doesn't halt, then your cycle detector claims that F(F) terminated, which it doesn't.
Therefore no such cycle detection can exist. It either has to bound the size of the input system or be non-exhaustive in its detection. The intuition here is: Assume the encoding of D has size N and D can check all encodings up to size N, then D must be able to dectect its own cycles. But the input to D(F, F) is size 2N (cause F is roughly the same size as D).
[1] If your original cycle detection outputs 0 if no cycle is present, then just wrap it in a TM that calls the original cycle detection and either returns on 1 or infinite loops on 0.
* F(F) internally runs its implementation of D's code on (F, F)
* ...which runs F(F) plus some constant-factor-overhead
* ...which runs its implementation of D's code on (F, F)
* ...which runs F(F) plus some constant-factor-overhead
* etc.
Ends up with the F emulating itself recursively, with the overhead adding up.
Note that the claim I make of D is that for any input system that runs in finite-but-unbounded space it will determine whether it halts in finite-but-unbounded space - not for input systems that already by themselves use infinite space.
Yes, if you ask the same question with a fixed (finite) memory restriction on everything, the answer is uninteresting. To me, this is... uninteresting. It tells you nothing about the underlying logical structure of your problem, which is what mathematicians are really trying to get at!
(first and foremost Turing machines are a tool for analysing problems mathematically, not a model of your laptop)
Also note that "states" in your sense are not the same as "states" in a Turing machine (which are just one of the inputs to the transition function). There are Turing machines with less than ten thousand states whose behaviour is undecidable in ZFC (https://arxiv.org/abs/1605.04343).
> (first and foremost Turing machines are a tool for analysing problems mathematically, not a model of your laptop)
I think what makes Animats's distinction worth stressing is that a lot of people miss this and fall into the trap of making false/misleading claims about the impact of the halting problem on actual computers/software.
For instance, claiming that the halting problem proves there are problems humans can solve that computers fundamentally can't, giving "the halting problem makes this impossible" as reason against adding a halt/loop detector to a chip emulator, making all sorts of weird claims about AI[0][1], or arguably even this author's claim that a halt detector would make bcrypt cracking trivial.
[0]: https://mindmatters.ai/2025/02/agi-the-halting-problem-and-t...
(Roger Penrose himself makes a version of that claim in "the Emperor's New Mind", so we're in good company...)
About the bcrypt thing... yeah, so one way you can do it is write a program that generates all possible keys starting with the letter 'a', and tests them. Then you run your halting oracle on that, and if it returns true you know the first letter of the key is 'a'.
Do this for each index/letter combination and you can crack bcrypt keys in linear time (in the number of calls to your halting oracle).
And you really can do that. For actual computers we have cycle detection algorithms that can tell you definitively if your program will halt or not.
Determining whether the program halts can still be complex or slow, which is the case here, but the halting problem does not make it undecidable (because it doesn't apply to real computers) nor place any lower bound on that complexity (nothing preventing a more advanced halt detector from finding better shortcuts).
Right. That leads to the whole 'brains are special and analog and quantum or something and thus can't be emulated digitally' line of thought. That line of argument is looking rather threadbare since LLMs got good. That's a different issue than decidability, though. Penrose does raise a good question as to how biological brains get so much done with so little power and rather low-frequency signals.
Nevertheless, we clearly do have some finite amount of information about this sequence, evident in the axioms of PA or ZFC or any other formal system that proves an infinite number of programs as non-halting (hence why the Busy Beaver project has been able to provably confirm BB(5)). We presume these systems are truly consistent and sound even if that fact is itself unprovable, so then where exactly did the non-halting information in the axioms of these systems “come from”?
Levin stops short of speculating about that, simply leaving it at the fact that what we have so far cannot be extended further by either algorithmic or random means. But if that’s the case, then either AI is capped at these same predictive limits as well (i.e., in the sense of problems AI could solve that humans could not, both given unlimited resources), or there is additional non-halting information embedded in the environment that an AI could “extract” better than a human. (I suppose it’s also possible we haven’t fully exploited the non-halting information we do have, but I think that’s unlikely since we’re not even sure whether BB(6) is ZFC-provable and that’s a rather tiny machine).
> any Martin-Lof random sequence that computes (i.e. allows computing from it) a consistent completion of PA also computes the Halting Problem H; and by deLeeuw et al. [1965], only a recursive sequence (which H is not) can be computed with a positive probability by randomized algorithms.
It's just the sequence of the solutions to the halting problem, i.e., the characteristic function of the halting set. Levin points out this sequence is not recursive/decidable.
But it seems interesting, thanks for the link =)
> a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible.)
A Turing machine can be trivially repurposed as a bcrypt cracker or chess engine (for the same definition of trivial the author is using), so if it's not intuitive that a computer can do this, then your intuition is wrong.
Program optimizers and theorem provers also exist, of course, but in those cases the problems really are undecidable so no Turing machine is guaranteed to work on any given program or theorem.
In other words, you can use undecidability of first-order logic to prove undecidability of the Halting problem if you like, although it's a bit of a chicken-egg thing historically (I believe).
The author is not correct and it's a common misconception. Simple question for you... let's say I give you a magical black box that can solve the halting problem. Now please use it to prove or disprove the continuum hypothesis (within ZFC).
Hopefully you'll come back to me and say the black box shows that the continuum hypothesis can not be proved or disproved (in ZFC). Okay we agree so far, but note that we have established that having a solution to the halting problem can not actually be repurposed as a general purpose theorem prover, since no such proof exists in the first place.
Okay you might counter by saying that a solution to the halting problem can be repurposed as a general purpose theorem prover for propositions that either have a proof or don't have a proof, ignore those pesky propositions that are neither provable or unprovable...
But then the solution to the halting problem doesn't get you anything... if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition.
The claim that a black box that solves the halting problem can be used as a general purpose theorem prover is simply untrue and confuses certain concepts together. At best you can claim it gives you a restricted theorem classifier.
What you are asking for is a machine that for each pair of formulas A, B (correctly) decides that either A -> B or A -> not(B), but this is impossible for model-theoretic reasons (not all theories are complete) and that has nothing to do with decidability.
> if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition.
You don't know what situation you are in ahead of time, this is the point (my proposed algorithm terminates on all inputs, including independent statements). If you had a black box machine that could tell you whether a statement was independent or not then that would be just as useful, yes. But that's also an undecidable problem. Yet a halting oracle can be used to compute it!
The author is correct, you are simply misusing or misunderstanding standard terminology =)
An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independent of ZFC and that's true and something I explicitly pointed out in my reply to you, but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC).
ZFC is not the end-all be-all of first order logic and it's certainly not even a particularly good choice of formal model for dealing with Turing Machines. Your halting oracle will not be able to do the same kind of theorem classification for other formal theories, namely those that do not have a recursively enumerable set of axioms. The most obvious example of such theories are second order theories, but even if you restrict yourself to first order theories, you have examples of such theories like True Arithmetic where your halting oracle won't be able to classify propositions since even though it's a first order theory proofs can't be enumerated in the same way that proofs can be enumerated in ZFC (or other first order theories with recursively enumerable axioms):
https://en.wikipedia.org/wiki/True_arithmetic
In general if the basis of your argument depends on nitpicking terminology, then that's a good sign you might not actually understand the fundamental concepts at play and are instead just regurgitating terms that you've heard from other people which is what I suspect you're doing here.
As for the stuff about CH, yes, there's nothing we disagree about there. And on non-recursive theories and logics without a sound/complete/effective proof theory, sure, a halting oracle isn't enough.
Do I really have to spell out every edge-case?
If you claimed every prime number is odd, and I point out that 2 is an even prime number, you don't get to turn around, pull out your credentials, claim I'm mixing things up and bickering around because I am pointing out an exception to your generalization.
The fact is a halting oracle cannot be used as a general-purpose theorem prover. At best it can be used as a way to classify theorems in specific first order theories with recursively enumerable axioms and I even admitted that much in my original response to you.
That some first order theories do not have recursively enumerable axioms and for these theories even an oracle for the halting problem is insufficient to either prove, refute, or classify as independent particular propositions is actually a fascinating topic in and of itself which could have led to a much more engaging conversation than the one you decided to go with by talking about your failed academic career and claiming I'm misinformed, but alas that ship has sailed and at this point and with that I don't think there is much further to discuss here.
huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.
Of course you have to input the axioms, how would a theorem prover work otherwise?
I think you mean completeness, but essentially yes.
With that out of the way, it's pretty easy to write a general theorem prover for such theories if you can solve the halting problem.
First define a TM G that takes as input 1. the description of another TM A that decides whether a particular sentence is an axiom of some theory T and 2. a sentence P. We enumerate all syntactically valid proofs with P as the conclusion and check whether all axioms are valid according to A and all inferences are sound. If we find a valid proof, we stop. (G can obviously be built.)
Then define H such that it takes the same inputs as G, and then (using the halting oracle) determines whether G would halt given A and P. If yes, return true, otherwise false.
Then H would be a decider for the language consisting of all pairs T |= P, where T is some recursively enumerable theory.
The basic idea is that you can determine whether a sentence X is in the theory or not by searching every natural number for counter-examples, and then using your halting oracle to check whether that search terminates or not.