5 ms·

> 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

> 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.
- srcreigh 2y ago
  Thanks for sharing interesting info! How do we know that there would be consistency issues or Σ₁-soundness issues? Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this? The argument doesn't make sense to me. Rather it seems like more of a consequence of BB being incomputable in the first place. The proof sizes for each BB(n) aren't expected to be computable at all. There is necessarily a different theory for each n (or intervals of n where each theory applies with limits on each). > So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time. Something something burden of proof something. It would be extremely fascinating to have a conclusive argument that large BB numbers cannot be solved.
  - LegionMammal978 2y ago
    > How do we know that there would be consistency issues or Σ₁-soundness issues? From Gödel's second incompleteness theorem, no consistent first-order recursively-axiomatizable theory (i.e., a theory that can have its proofs validated by a Turing machine) can prove its own consistency. Thus, to prove that your current theory (e.g., ZFC) is consistent, you must move to a stronger one (e.g., Aleph*). But then you can't prove the consistency of that without an even stronger theory, and so on. Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories. > Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this? Not really, other than some of my own ramblings on the bbchallenge Discord server. But it's not that long: Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols, and checks whether it shows that a particular n-state machine halts. The TM then simulates all of the proven halters to see how long they run. By assumption, the longest-running machine M is included in this list. So this TM can compute BB(n), which is an impossibility. Therefore, the function f(n) cannot exist. As a corollary, since it's "uncomputably difficult" to prove that the longest-running machine halts at all, it's no less difficult to fully establish the value of BB(n).
nickdrozd 2y ago
> They have used a proof generator based on a logical theory... I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.
- srcreigh 2y ago
  You got it - the creative developments of a stronger theory. This allows the creation of tools which can categorize TMs, tools which wouldn’t exist otherwise. It’s fascinating that the entire space of finite amounts of random gibberish contains every such stronger theory. As a thought experiment it does well. Interestingly the Church-Turing thesis seems to exclude ingenuity. That is, it doesn’t try to say there aren’t functions on natural numbers which are uncomputable but can be calculated with ingenuity. Seems that a ton of people conflate those things.
lupire 2y ago
Why would Aleph* be necessary or relevant? ZFC and larger theories are only relevant for infinite objects, not finite objects like BB.
- srcreigh 2y ago
  I don’t have the understanding, but apparently there are finitary statements which are independent of ZFC. This has been used to prove that BB(745) is independent of ZFC. https://mathoverflow.net/a/26605 https://mathoverflow.net/a/26605 Furthermore, Scott aaronson jokingly conjectured that even BB(20) is independent of ZFC. That’s my reference here where we end up needing Aleph* for BB(18).

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.

srcreigh 2y ago
Thanks for sharing interesting info! How do we know that there would be consistency issues or Σ₁-soundness issues? Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this? The argument doesn't make sense to me. Rather it seems like more of a consequence of BB being incomputable in the first place. The proof sizes for each BB(n) aren't expected to be computable at all. There is necessarily a different theory for each n (or intervals of n where each theory applies with limits on each). > So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time. Something something burden of proof something. It would be extremely fascinating to have a conclusive argument that large BB numbers cannot be solved.
- LegionMammal978 2y ago
  > How do we know that there would be consistency issues or Σ₁-soundness issues? From Gödel's second incompleteness theorem, no consistent first-order recursively-axiomatizable theory (i.e., a theory that can have its proofs validated by a Turing machine) can prove its own consistency. Thus, to prove that your current theory (e.g., ZFC) is consistent, you must move to a stronger one (e.g., Aleph*). But then you can't prove the consistency of that without an even stronger theory, and so on. Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories. > Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this? Not really, other than some of my own ramblings on the bbchallenge Discord server. But it's not that long: Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols, and checks whether it shows that a particular n-state machine halts. The TM then simulates all of the proven halters to see how long they run. By assumption, the longest-running machine M is included in this list. So this TM can compute BB(n), which is an impossibility. Therefore, the function f(n) cannot exist. As a corollary, since it's "uncomputably difficult" to prove that the longest-running machine halts at all, it's no less difficult to fully establish the value of BB(n).

nickdrozd 2y ago

> They have used a proof generator based on a logical theory... I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.

srcreigh 2y ago
You got it - the creative developments of a stronger theory. This allows the creation of tools which can categorize TMs, tools which wouldn’t exist otherwise. It’s fascinating that the entire space of finite amounts of random gibberish contains every such stronger theory. As a thought experiment it does well. Interestingly the Church-Turing thesis seems to exclude ingenuity. That is, it doesn’t try to say there aren’t functions on natural numbers which are uncomputable but can be calculated with ingenuity. Seems that a ton of people conflate those things.

lupire 2y ago

Why would Aleph* be necessary or relevant? ZFC and larger theories are only relevant for infinite objects, not finite objects like BB.

srcreigh 2y ago
I don’t have the understanding, but apparently there are finitary statements which are independent of ZFC. This has been used to prove that BB(745) is independent of ZFC. https://mathoverflow.net/a/26605 https://mathoverflow.net/a/26605 Furthermore, Scott aaronson jokingly conjectured that even BB(20) is independent of ZFC. That’s my reference here where we end up needing Aleph* for BB(18).