4 ms·

Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same tec

Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.

tromp 2y ago
> the 2-color 4-state case? You mean the 2-state 4-color case...
- nickdrozd 2y ago
  Fixed, thanks
LegionMammal978 2y ago
> Has anyone tried applying these same techniques to the 2-color 4-state case? I assume you mean the 4-color case. As I understand it, the deciders currently in use are sufficient to prove all the 2×4 holdouts non-halting. So the current champion gives us Σ(2,4) = 2,050 and S(2,4) = 3,932,964, barring some big errors in the decider design. The result just hasn't been organized in one place. > (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) Yes, 2×5 has the Hydra, and 6×2 has the Antihydra, which compute the same iteration, but with different starting points and halting conditions. The standard conjecture (related to Mahler's 3/2 problem) is that this iteration is uniformly distributed mod 2, and a proof of that conjecture would very likely prove both machines non-halting, by yielding suprema and infima on the cumulative ratio of 0s to 1s. But of course there is no known method of proof.
srcreigh 2y ago
> By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof. The year is 52,000 CE and humans have solved BB(18) in the sense of exhaustively categorizing halting vs non-halting 19-state no-input programs. They have used a proof generator based on a logical theory called Aleph*, and at that time it had been known for 1.5k years that ZFC is incapable of establishing BB(18). Compared to the year 2024 CE, considerable millennia before Aleph* came into use, it is clear that no program written at that point in history was capable of even using brute force proof checking to solve BB(18) in theory (like how we can enumerate and check ZFC proofs today to solve BB(??) in theory). That's what is meant by the "humans intuit solutions to the halting problem" position. AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. And due to BB being incomputable, humans had to develop new theory to be able to construct the programs required. Something has to be accredited for the results, and it can't be computation since the programs did not exist.
- LegionMammal978 2y ago
  > AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. Probably the biggest issue is that they'd have no method to establish that Aleph* is consistent. To continue this BB chain indefinitely, you must invent further and further first-order theories, each of which might not be consistent, let alone Σ₁-sound. And with an Σ₁-unsound theory, any halting proof might not hold up in the standard model of the integers. You'd effectively have to postulate an indefinite amount of oracular knowledge. Also, another physical issue: you can show that within any consistent, recursively axiomatizable theory, the length of the shortest proof of "the longest-running n-state machine is M" must grow at an uncomputable rate in terms of n. Ditto for the shortest proof of "machine M halts", where M is factually the longest-running n-state machine. Otherwise, a machine could use a computable bound on the proof length to solve the halting problem. Therefore, the proof should very quickly become too large to fit within our light cone. In any case, the BB-related evidence for that position rested on BB(5) being determinable by extending the techniques used for BB(4). But in fact, it turns out that similar extensions don't even get you to BB(6). So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time.
ganzuul 2y ago
> extremely stupid This is simply a test for if consciousness has infinite computational resources.

tromp 2y ago

> the 2-color 4-state case? You mean the 2-state 4-color case...

nickdrozd 2y ago
Fixed, thanks

LegionMammal978 2y ago

> Has anyone tried applying these same techniques to the 2-color 4-state case? I assume you mean the 4-color case. As I understand it, the deciders currently in use are sufficient to prove all the 2×4 holdouts non-halting. So the current champion gives us Σ(2,4) = 2,050 and S(2,4) = 3,932,964, barring some big errors in the decider design. The result just hasn't been organized in one place. > (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) Yes, 2×5 has the Hydra, and 6×2 has the Antihydra, which compute the same iteration, but with different starting points and halting conditions. The standard conjecture (related to Mahler's 3/2 problem) is that this iteration is uniformly distributed mod 2, and a proof of that conjecture would very likely prove both machines non-halting, by yielding suprema and infima on the cumulative ratio of 0s to 1s. But of course there is no known method of proof.

srcreigh 2y ago

> By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof. The year is 52,000 CE and humans have solved BB(18) in the sense of exhaustively categorizing halting vs non-halting 19-state no-input programs. They have used a proof generator based on a logical theory called Aleph*, and at that time it had been known for 1.5k years that ZFC is incapable of establishing BB(18). Compared to the year 2024 CE, considerable millennia before Aleph* came into use, it is clear that no program written at that point in history was capable of even using brute force proof checking to solve BB(18) in theory (like how we can enumerate and check ZFC proofs today to solve BB(??) in theory). That's what is meant by the "humans intuit solutions to the halting problem" position. AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. And due to BB being incomputable, humans had to develop new theory to be able to construct the programs required. Something has to be accredited for the results, and it can't be computation since the programs did not exist.

LegionMammal978 2y ago
> AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. Probably the biggest issue is that they'd have no method to establish that Aleph* is consistent. To continue this BB chain indefinitely, you must invent further and further first-order theories, each of which might not be consistent, let alone Σ₁-sound. And with an Σ₁-unsound theory, any halting proof might not hold up in the standard model of the integers. You'd effectively have to postulate an indefinite amount of oracular knowledge. Also, another physical issue: you can show that within any consistent, recursively axiomatizable theory, the length of the shortest proof of "the longest-running n-state machine is M" must grow at an uncomputable rate in terms of n. Ditto for the shortest proof of "machine M halts", where M is factually the longest-running n-state machine. Otherwise, a machine could use a computable bound on the proof length to solve the halting problem. Therefore, the proof should very quickly become too large to fit within our light cone. In any case, the BB-related evidence for that position rested on BB(5) being determinable by extending the techniques used for BB(4). But in fact, it turns out that similar extensions don't even get you to BB(6). So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time.

ganzuul 2y ago

> extremely stupid This is simply a test for if consciousness has infinite computational resources.