User talk:Hakerh400/What we could do if we could solve the halting problem

I just wanted to leave a few mathematical notes.

• The halting problem doesn't ask whether a given Turing machine halts. It asks whether there exists an algorithm that decides whether any Turing machine halts.
• Accordingly, the real-world example with specified properties of rocket firmware is not a problem; there is no obstacle to proving that a specific Turing machine halts. However, each such proof must be hand-made, because there is no algorithm which does it automatically.
• Theoretically, there is no algorithm which decides whether any Turing machine halts. If there were such an algorithm, then there is a Turing machine which contradicts itself merely by existing, since it simultaneously halts and does not halt. To build this machine, simply take the algorithm which decides halting, and generate a Turing machine which runs that algorithm, and then halts or runs forever based on whether its input runs forever or halts. Feed this machine to itself as an input, and we get a situation where the machine halts if and only if it does not halt.
• In terms of particle physics, it is known that spectral gaps are uncomputable; specifically, spectral mass gaps are not computable from first principles. Nonetheless, physicists can experimentally measure spectral gaps.

Corbin (talk) 11:38, 27 November 2021 (UTC)

Your second statement is incorrect. There is no difference between a "hand-made" and an automatically generated proof. If we fix the logic framework, every statement that is provable by a human is also provable by a computer and vice versa. Determining whether any specific Turing machine halts is not possible in a fixed logic framework. For example, given a Turing machine that searches for contradictions in ZFC (and halts if it finds one). Does it halt? In order to answer it, we must use a stronger axiom, such as "ZFC is consistent" or "ZFC is not consistent". But then there is a Turing machine that also includes that axiom and to prove that it doesn't halt we need more axioms (and none of them we can prove that is consistent). --Hakerh400 (talk) 07:35, 3 December 2021 (UTC)

Sure, my words were poorly chosen. By automatic proof, I mean the universal quantifier. It's not true that, for all Turing machines T, there is a procedure which decides whether T halts. But it could be the case that there is a "hand-made" proof that T halts or diverges, written using specific properties of T which aren't true of all Turing machines.

What I was attempting to justify was that the original page's claim, "mathematics does not deny the possibility of solving the halting problem," is flatly incorrect. In fact, we have a century's worth of fixed-point paradoxes and theorems, of which the halting problem is just one instance. [1] What might be confusing is what I explained above: while we cannot decide for all Turing machines T whether T halts or diverges, we might be able to decide specific Turing machines as special cases. This leads to Rice's theorem; the special cases which are acceptable are just the syntactic properties! Corbin (talk) 08:41, 3 December 2021 (UTC)

The confusion arises from your assumption that there exists a unique convention regarding the definition of the Halting problem. Added clarification in the article to reflect that fact. --Hakerh400 (talk) 07:15, 4 December 2021 (UTC)