Hacker News Reader

Comment by vecter | Hacker News Reader

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.

View on HN

> 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 am a small brain here. How is this so clear?

Because it says 'clearly'. (but yeah, agree with you)

Checking whether a string of bits encodes a proof of False in ZF is decidable. Now enumerate the bitstrings and check each.

> and check each.

"Now, draw the rest of the owl." Not saying you're wrong, just, this jump is super non-obvious even to most mathematicians.

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?

> There are infinite many such strings

And they can be enumerated by a finite program. For example, in lazily evaluated pseudocode:

    bits = ["0", "1"]
    bitstrings = bits + [(bit + suffix for bit in bits) for suffix in bitstrings]

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).

Ooh, are they basically the number of possible turing programs encodable in a state of N?

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.

I think the part that eludes me here is that it's not clear that such a Turing machine could be built from a finite number of states.

Reply on news.ycombinator.com