> In what sense is the BB sequence even well-defined if we can prove that it can't be determined?
Every BB number can be determined. However, each one must require zillions of special cases which require their own reasoning---this is the only way to prevent the BB numbers from being computable.
So, if you consider, for example, the proof of the four-color theorem (which amounts to checking many special cases), as mathematics, then mathematics surely can determine BB(n). It's just extremely hard---as hard as doing all of mathematics (in the sense that if you could easily get BB(n) you could then take a logical proposition you are interested in proving in some axiomatic system and construct a TM to derive the statement using those axioms. Then, count how many states that TM has, and start running it. If it runs for more than BB(# states), there is no proof from your system of your proposition).
I think it is possible, in principle, to find a number which you can be pretty sure is BB(n). The problem I think is being sure that this number really is BB(n).
Like you run all n-state Turing Machines for a super long time, and take the max of the output of all the ones that have halted. Now this might give you BB(n), but you can't be sure because you don't know whether the ones that haven't halted are ever going to halt.
In mathematics, we can just say "Well consider the set of all the ones that do halt, and take their max." In real life, it's not so easy to "consider the set".
That's clear. My point is that mathematics can't list the Busy Beaver machines.
> In what sense is the BB sequence even well-defined if we can prove that it can't be determined?
Every BB number can be determined. However, each one must require zillions of special cases which require their own reasoning---this is the only way to prevent the BB numbers from being computable.
So, if you consider, for example, the proof of the four-color theorem (which amounts to checking many special cases), as mathematics, then mathematics surely can determine BB(n). It's just extremely hard---as hard as doing all of mathematics (in the sense that if you could easily get BB(n) you could then take a logical proposition you are interested in proving in some axiomatic system and construct a TM to derive the statement using those axioms. Then, count how many states that TM has, and start running it. If it runs for more than BB(# states), there is no proof from your system of your proposition).
I think it is possible, in principle, to find a number which you can be pretty sure is BB(n). The problem I think is being sure that this number really is BB(n).
Like you run all n-state Turing Machines for a super long time, and take the max of the output of all the ones that have halted. Now this might give you BB(n), but you can't be sure because you don't know whether the ones that haven't halted are ever going to halt.
In mathematics, we can just say "Well consider the set of all the ones that do halt, and take their max." In real life, it's not so easy to "consider the set".
2 replies →