The Busy Beaver Game | Hacker News Reader

The Busy Beaver Game

johncarlosbaez.wordpress.com

112 pointsmathgenius42 comments

Edit: whoa, they really buried the lede: the upper bound for the knowable values may be as low as BB(1919) as of May 15!

I'm confused by the winning TM given for BB(2). It has 3 non-halt states, but N==2 should be a TM with 2, shouldn't it?

Did they merely put the illustration for BB(3) in the wrong place?

Edit: yeah, looks like they just put the illustration for BB(3) in the wrong place: https://en.wikipedia.org/wiki/Turing_machine#/media/File:Sta...

The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns?

Because the byline wasn't easy to find on the device I read it on, and the possibility that someone might be offended by gender neutrality seemed far-fetched at the time.

> The author has the first name "John Carlos". Why not take an educated guess and use (gasp) gendered pronouns?

Because the text of the article could have been generated by a Turing machine with the pseudonym "John Carlos". And on the internet, nobody knows if you're a man, woman, dog, or sufficiently complicated state machine.

tl;dr: Non-gendered pronouns are inclusive and never inappropriate on the internet.

The article says "if the usual axioms of set theory are consistent, we can never use them to determine the value of BB(7910)." But why does this imply that BB(7910) is uncomputable? Perhaps another axiomatic system could compute its value?

> Perhaps another axiomatic system could compute its value?

Of course another axiomatic system could. If you could tell us such an axiomatic system for which you can prove that it can determine the value of BB(7910) and have strong arguments why it is probably consistent (by Gödel one will not be able to prove this property if it is able to express basic arithmetic) mathematicians would love to get to know it, since they really have no idea how such a system might look like.

It's easy to specify such a system that's more powerful than ZFC and has strong arguments for its consistency: ZFC+con(ZFC), which is consistent iff ZFC is consistent.

And it's easy to go one level up, I.e that system plus it's own consistency.

These systems will be stronger than ZFC, and will prove the machine in question halts.

Of course, the lowest unknowable from ZFC BB number is probably around BB(15), so likely none of those systems get that high, but they do probably give us more than just ZFC does.

See also http://www.scottaaronson.com/blog/?p=697 for some limitations on this.

Also, there are large cardinal axioms which imply the consistency of ZFC and are believed to be consistent, but I'm not so familiar with them. I think mathematicians would consider those axioms as "what such a system would look like".

I think they do have some ideas.

You might look at Believing The Axioms (http://cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf, but it's two parts) which studies set theorists who are investigating new axioms for set theory, especially large cardinal axioms, iirc. Honestly, that work is a ways beyond what I can understand, but it's clear that it's an active area of research.

You might also read about Hugh Woodin has a very developed program arguing for axioms which would imply the negation of the Continuum Hypothesis.

(This doesn't necessarily apply to this specific question, but in general, research into axiomatic foundations of math is ongoing).

That's what he means. We need a formal system more powerful than ZFC, i.e. new mathematics. If a formal system can compute BB(7910), then it is more powerful than ZFC. I'm not sure anyone knows how to build that yet.

See https://news.ycombinator.com/item?id=11753046

You can get more powerful, it's just unlikely anything we can build will get that high.

I'm surprised it's that simple. Then again, simplicity is usually surprising.

Be careful with the word "incomputable" (the article never said it was "undecidable" or "incomputable"); in computability theory BB(7910) is computable because it's just a single finite number. You could in theory specify a TM that writes down the answer without doing any calculation - incomputable problems necessarily involve unbounded outputs or inputs which prevents such trivial solutions.

I realise you're talking about formal systems specifically (which corresponds to a some theorem-checking TM implementing that system) but when you allow any system of axioms (e.g. one with the value of BB(7910) of axioms) you basically ask whether any TM can compute that number (including one that already 'knows' it).

They created a Turing machine that may run forever. However we can't prove that. It could stop the next second, or tomorrow, or the day after.

They also proved however that you'll never see it halt. Because that would be a proof of consistency.

Wait. What?

No; halting would be a proof of inconsistency.

We expect it never to halt because we believe ZFC to be consistent.

Belief has nothing to do with it. I can believe ZFC is inconsistent and the world will not change a bit. You can't prove me wrong. (It's almost a religious argument)

If I believe the inconsistency of ZFC then I believe the machine must halt. I can't ever observe it since I can't know the number of steps needed. There's almost a paradox but not quite.

No, if ZFC is inconsistent, then you can know the number of steps needed. Every statement, true or false, is derivable from ZFC if it is inconsistent. If there's contradiction in ZFC, it can be found in finite time by enumerating all the theorems.

If you're refering to Yedidia and Aaronson's machine, the machine searches for counterexamples in ZFC. We believe, but cannot prove, that ZFC is consistent. Also, we can prove that assuming ZFC is consistent, ZFC cannot prove that ZFC is consistent. Hence, since we believe ZFC is consistent, we believe that the machine will not halt, but we can't prove it. This implies that BB(7910) cannot be computed.

BB 7910 can be computed: it's just a finite number. What you mean is that the value can't be proven correct in ZFC.

If you write down a value for BB 7910 but can't prove that it is correct, I wouldn't say that you "computed it".

But ZFC isn't the only system in town. It's possible (although highly unlikely) that we could prove its value in another system that we can see to be just as valid as ZFC. (Like adding consistency axioms and so on.)

Yeah, sure, if we agree to do math in the system ZFC+Con(ZFC) we can prove that Yedidia's machine does not halt. But then we can just construct another machine (call it M', a n'-state turing machine) that searches for contradictions in ZFC+Con(ZFC), and now we believe that M' does not halt, but we can't prove it; and now, BB(n') can't be computed.

Sure, but that n' will be larger.

Sure, but no matter what model of math we choose to work in, I can come up with some n such that I can say "...hence, BB(n) cannot be computed", and you cannot reply "BB(n) can be computed; it's just a finite number. What you mean is the value can't be proven correct..."

It can always be computed. If you're choosing a specific model of math, you need to specify that in your statement.

It will still be computable within that model, just not provably so within that model.

Computable has a very specific meaning in computability theory, and any finite number is computable.

The function BB(n) is not computable, but this was known for decades, it has nothing to do with the recent result.

> If you're choosing a specific model of math, you need to specify that in your statement.

I mean, in my most recent statement I quantified over all consistent models...

> It will still be computable within that model, just not provably so within that model.

OK, now I'm confused; what is the specific definition of "computable number" you're using?

Also, informally speaking, say we're both working in ZFC. You claim that BB(7910) is computable. What does that mean? Does it mean you can write down its value as a normal decimal number?

>I mean, in my most recent statement I quantified over all consistent models...

Not quite, as I pointed out in https://news.ycombinator.com/item?id=11753020. You can easily have a consistent system that proves the value of all BB numbers, it just won't be computable.

If you restrict us to computable consistent systems, then for any given model there will be some value of BB it doesn't prove, but also for any given value of BB there will be some consistent model that proves it. There's nothing in particular added about knowability by Aaronson's et al result, only about provability.

>OK, now I'm confused; what is the specific definition of "computable number" you're using?

https://en.wikipedia.org/wiki/Computable_number

Any finite number is computable, we just can't prove that a specific machine is the one that computes BB(N). We can prove that some machine in a finite set (all TMs of size N we haven't seen to halt or proven nonhalting) computes it, but we can't pin down which one, within that model.

>Also, informally speaking, say we're both working in ZFC. You claim that BB(7910) is computable. What does that mean? Does it mean you can write down its value as a normal decimal number?

Lol nope. We can't even write down anything above BB(6). BB(7) has more digits than atoms in the observable universe.

My claim that BB(7910) is computable means there's a Turing machine that computes it. That's easy to prove, as any finite integer can be computed by a Turing machine.

There's no Turing machine that computes every BB number sequentially, though.

I'm trying to get an intuition about why this whole game can even be played, and it's proving (ha) rather tricky. I'm ok with the idea that things sometimes cross into the realm of the impossible when transitioning from discrete/finite to continuous/infinite, or maybe from countably to uncountably infinite, but the notion that there's some constant threshold seems so counterintuitive. The link at the end of the article is pretty good [1] as is wikipedia [2], but I'm clearly missing some intuition here. Help!

[1] https://johncarlosbaez.wordpress.com/2011/10/28/the-complexi... [2] https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin....

You can't solve the halting problem. Therefore, if you take a program that takes a Turing machine as input, searches for a proof in ZFC (or your favorite alternative) that the program halts or that it doesn't, and if it doesn't find a proof either way then it runs forever, your program is not a halting solver.

Therefore, there are some Turing machines which can't be proven to halt or run forever in any given consistent system that can be computed.

(Because if every TM had a proof, then the program above would solve the unsolvable halting problem).

Therefore, there is a smallest such program that's independent of ZFC.

Does that help?

> Therefore, there is a smallest such program that's independent of ZFC.

http://www.scottaaronson.com/blog/?p=2725

    we give a 7,918-state Turing machine, called Z
    (and actually explicitly listed in our paper!),
    such that:

      Z runs forever, assuming the consistency of a large-cardinal
      theory called SRP (Stationary Ramsey Property), but

      Z can’t be proved to run forever in ZFC [...],
      assuming that ZFC is consistent.

edit: Just saw that this was linked at the bottom of the article. As pohl mentioned, the article really buried the lede.

Yeah a bit. This part

> searches for a proof in ZFC (or your favorite alternative)

is tripping me up though. It's not obvious to me that you can do this in an automated fashion. I assume this is a standard tool for theorists though? How does such a program work?

Proofs can be expressed using a string and verified to check every step is valid.

So brute force over every string, checking if it's a valid proof for the claim you want.

It's not letting me reply any deeper, but that makes sense, thanks!

I think it's that you can't reply to posts that are too new.

You can, you just have to click on the timestamp to visit the comment's item page first, something like https://news.ycombinator.com/item?id=11750351

The idea is that proof systems can be formulated as a grammar for a recursively enumerable language (Type 0 grammars in the Chomsky hierarchy): https://en.wikipedia.org/wiki/Chomsky_hierarchy#Summary, such that if there is a proof of a particular statement a corresponding word can be derived by the corresponding grammar. But this can easily be done by a Turing machine (either check through all possible derivations in the grammar or, more abstract, let the Turing machine let non-deterministically choose a possible derivation and use the fact that the expressiveness of non-deterministic Turing machines is the same as for deterministic Turing machines).

  Therefore, there are some Turing machines which can't be
  proven to halt or run forever in any given consistent
  system that can be computed.

I feel like it's worth clarifying the quantifiers here. For all consistent systems, there exist Turing machines whose halting behavior can't be proven in that system. Unless I have some disastrous misunderstanding...

Well a consistent system that can't be computed can prove things about all Turing machines.

E.g. ZFC plus an infinite set of axioms of the sort "machine X halts" for all machines that halt. We can't compute all the axioms, but the system is perfectly consistent. We could compute the axioms if we had a halting Oracle.

It wouldn't be able to prove the halting behavior of some Turing machines that have halting oracles attached, though.

May I ask if you are able to visualize things using your mind's eye at at what levels (size, detail, color/brightness)? Just curious about correlation with the subject matter.

I made a small implementation of the Busy Beaver game in React a while ago: http://rajk.me/static/busybeaver.html. (Click the rules to toggle them).

Start with 1-state, and 2-state is a decent challenge. Not sure if 3-state is possible by hand.

I wrote an interesting article a while ago with graphs of how the beaver walks across the tape, and other interesting info.

http://www.catonmat.net/blog/busy-beaver/

Numberphile did a great video on Busy Beaver which I found easy to follow - https://youtu.be/CE8UhcyJS0I

FWIW, I implemented some BB code in Python and made some pretty neat plots:

https://github.com/cslarsen/busy-beaver

Of course I cheat by knowing S(n).

Reply on news.ycombinator.com