4 ms·
> it is always possible to compute BB(k) for a specific and arbitrary k How do you do that once k is large enough that it admits Turing machines whose halting
by dllthomas 4y ago
> it is always possible to compute BB(k) for a specific and arbitrary k
How do you do that once k is large enough that it admits Turing machines whose halting behavior is independent of our axioms?
- vainguard 4y agoBB(k) for a specific k is just a number. Ao just write it to the output. Proofing correctness is different from „computing“ and not required here.
- puffoflogic 4y ago> BB(k) for a specific k is just a number. That's not as obvious as you might think. The value of BB(800) is independent of ZFC. So it isn't "just a number" if you're working in ZFC.
- dllthomas 4y agoHmm... As ZFC specifically cannot identify that number as special (at least as relates to the Busy Beaver function), maybe it is quite specifically "just a number"!
- dllthomas 4y agoAh, so pointing out that the number itself, being an integer, is computable even though the function isn't. Makes sense.
- kevinventullo 4y agoPerhaps you need larger and larger sets of axioms as k increases. This is fascinating to me, because Turing machines can in principle be manifested as physical objects. It feels like you shouldn’t need axioms if you have the thing sitting in front of you, but on the other hand how else are you supposed to prove something doesn’t halt? Still, if you have two axiomatic systems that disagree, what does that mean? Surely you can just run the machine in question for a certain number of steps to determine which system is right.
- kevinventullo 4y agoAh, the issue is that one system may be able to prove the correct answer but it remains independent for the other system.