FTA this is an interesting tidbit about Busy Beavers:
But the BB function has a second amazing property: namely, it’s a perfectly well-defined integer function, and yet once you fix the axioms of mathematics, only finitely many values of the function can ever be proved, even in principle. To see why, consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory. Clearly such a machine could be built, with some finite number of states k. But then ZF set theory can’t possibly determine the value of BB(k) (or BB(k+1), BB(k+2), etc.), unless ZF is inconsistent! For to do so, ZF would need to prove that M ran forever, and therefore prove its own consistency, and therefore be inconsistent by Gödel’s Theorem.
> consider again a Turing machine M that halts if and only if there’s a contradiction in ZF set theory. Clearly such a machine could be built, with some finite number of states k.
I wouldn’t defend the idea that it’s “clear”, but the idea is to build a machine that combines the axioms of ZF set theory in all possible ways to generate all possible conclusions, checking each one for contradiction as it goes. If it never generates a contradictory conclusion from those axioms, it’ll run forever.
This sounds like it relies on the halting problem, or maybe the other way around? Really interesting stuff, been a while since I read about a higher level math topic and been able to sorta kinda understand the "quanta-level" summaries out there
The Nth Busy Beaver number lets you solve the halting problem for Turing Machines up to size N.
Only a handful of them are known, for very small N, and they increase incredibly rapidly. For the most common version of the problem (S for 2-symbol machines), they go: 1, 6, 21, 107, some number greater than or equal to 47176870, and some number greater than 10⇈15 (that's up arrow notation on the last one).
It's the maximum amount of time a Turing machine of size N can run. So if you want to know whether a Turning machine of size N or less will halt, just run it for BB(N) steps. If it hasn't halted by then, it never will.
If you can check any given bitstring for whether it encodes a valid ZFC proof of the (in)consistency of ZFC in finite time, then you can write a program to enumerate over all possible bit strings in shortlex order and halt the first time you see a valid proof.
There are infinite many such strings, so that alone can't be used to prove the Turing machine of k states can check all strings. So that leaves open the original question, how do we know that a Turing machine of k states is able to have one of the stated outcomes for any possible bit string?
