It is never undecidable to determine whether a single particular program halts or not.
For any single program, one of these two functions will correctly output whether it halts or not.
bool always_true(TuringMachine M) {
return true;
}
bool always_false(TuringMachine M) {
return false;
}
It won't work for every Turing Machine, but it will work for a specific one.
This is why it's not very meaningful to talk about the decidability of particular Turing Machines and also why the halting problem is not, and never was about specific Turing Machines.
As to your point about being decidable within ZFC or PA, that is true but it's also not really significant. Neither ZFC or PA are a kind of master authority when it comes to decidability and in fact the vast majority of mathematics is fairly agnostic with respect to the use of ZFC.
The choice of a particular set theory tends to only come up in very explicit circumstances, and even in those circumstances you'll find mathematicians using theories that are more powerful than ZFC such as by making use of large cardinal axioms.
I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist).
Of course, if the program did eventually terminate, then a termination proof would exist (just enumerate all the state transitions, there's only a finite number of them). So what it means is that some programs never halt, but it's impossible to prove this fact.
This ties in with Gödel's theorems, e.g. (if we use ZFC and assume ZFC is consistent) a program that enumerates all possible valid proofs from axioms in ZFC and halts whenever it finds a contradiction, would never halt, but we can't prove this (at least not in ZFC) because that would contradict Gödel's second incompleteness theorem.
> For any single program, one of these two functions will correctly output whether it halts or not.
Saying "one of these functions is correct" is not a decision procedure. You actually need to decide which one of them is correct.
> This is why it's not very meaningful to talk about the decidability of particular Turing Machines
I disagree. There are particular Turing machines whose decidability is extremely meaningful. For example, there are specific Turing machines which encode mathematical problems of interest such as the Goldbach conjecture. Deciding whether they halt is equivalent to solving those mathematical problems, which is definitely meaningful.
>Saying "one of these functions is correct" is not a decision procedure. You actually need to decide which one of them is correct.
That's precisely what a decision procedure is, it's an algorithm that takes as input the description of a Turing machine, and an input, and returns true if and only if the Turing machine halts when given the input. You are using the term "decide" as if there were some kind of agency involved, like you have to actually "choose" what is correct or incorrect, but no such agency is involved, it is a purely mechanical process.
>There are particular Turing machines whose decidability is extremely meaningful.
You are mixing up the notion of decidability with the notion of halting, and there is a subtle difference. The Turing machine that encodes the Goldbach conjecture proves the conjecture if it halts, and disproves the conjecture if it doesn't halt. That is an interesting and meaningful property of such a Turing machine. What is not meaningful or interesting is whether that particular Turing machine is decidable.
As I said, there is a subtle difference between whether a Turing machine halts or not, and whether it's decidable whether it halts or not. The former is interesting, the latter is not particularly insightful.
> You are using the term "decide" as if there were some kind of agency involved, like you have to actually "choose" what is correct or incorrect
Isn't this literally what a decision procedure is? It's an algorithm that always outputs the correct answer, not one which tells you "the correct answer is either true or false". I'm not talking about agency or consciousness.
One of the two algorithms I posted tells you the correct answer for any specific Turing machine, so for any given Turing machine one of them is a decision procedure for it.
Exactly, so then we agree, there is nothing useful about an algorithm that can decide whether one specific Turing machine halts. Utility only emerges from an algorithm that can decide whether entire classes of other Turing machines halt, not from whether a particular machine does.
> there is nothing useful about an algorithm that can decide whether one specific Turing machine halts.
Yes there is. If someone gives me a working algorithm (this means one algorithm, not two algorithms either of which may work or not as you've been doing) which can provably decide whether the machine encoding the Goldbach conjecture halts or not, that is a very useful algorithm.
I must insist that giving two algorithms and saying "one of them works" without telling me which one works is is not a valid answer, since that is strictly different from giving a working algorithm which I can run in finite time in order to find out one correct answer.
You said this yourself earlier:
> The Turing machine that encodes the Goldbach conjecture proves the conjecture if it halts, and disproves the conjecture if it doesn't halt. That is an interesting and meaningful property of such a Turing machine.
I just think you're making a very subtle mistake here by mixing up the question of whether Fermat's Last Theorem (or Goldbach's Conjecture) is true with whether there is an algorithm that tells you that that specific theorem is true.
In my opinion, it's useful to know whether Fermat's Last Theorem is true, and that requires a proof. An algorithm that can only tell you whether a particular theorem is true is entirely useless.
For example, Sir Andrew Wiles proved that Fermat's Last Theorem is true, so would you reject an algorithm that simply returned true for any input as somehow being wrong? Would you only be happy if the algorithm wasted some energy doing some "computation", messing around with some variables and producing copious amounts of heat before telling you that Fermat's Last Theorem were true? Of course not. It doesn't matter what the algorithm does as an implementation detail, what matters is that the output is correct, not the heat it generates in the process.
Knowing a theorem is true is valuable. Having an algorithm that simply returns the correct answer about whether a particular theorem is true is entirely useless.
In general, an algorithm is only useful when it can be used for some arbitrarily large set of inputs. An algorithm that only works for one single instance is hardly an algorithm at all, it's nothing more than a lookup table. To be something more than a lookup table, it needs to work for an entire class of inputs, it needs to take an infinite number of possibilities and compress them down into the finite description of a process.
We know that no such algorithm can decide the halting problem for every single Turing Machine, but we can construct algorithms that can decide the halting problem for subsets of Turing machines, infinitely large subsets in fact.
Having an algorithm that just works for one single Turing machine... pretty meaningless.
For any single program, one of these two functions will correctly output whether it halts or not.
It won't work for every Turing Machine, but it will work for a specific one.This is why it's not very meaningful to talk about the decidability of particular Turing Machines and also why the halting problem is not, and never was about specific Turing Machines.
As to your point about being decidable within ZFC or PA, that is true but it's also not really significant. Neither ZFC or PA are a kind of master authority when it comes to decidability and in fact the vast majority of mathematics is fairly agnostic with respect to the use of ZFC.
The choice of a particular set theory tends to only come up in very explicit circumstances, and even in those circumstances you'll find mathematicians using theories that are more powerful than ZFC such as by making use of large cardinal axioms.