[Maxatar]

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.

[Tainnor]

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.

[FartyMcFarter]

> 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.

[Maxatar]

>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.

[FartyMcFarter]

> 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.

[Maxatar]

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.

[FartyMcFarter]

Sure, that is trivially true, but I don't see how that statement is useful in any way.

[Maxatar]

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.