{"id":2725,"date":"2016-05-03T18:04:26","date_gmt":"2016-05-03T22:04:26","guid":{"rendered":"https:\/\/scottaaronson.blog\/?p=2725"},"modified":"2019-01-30T02:38:55","modified_gmt":"2019-01-30T08:38:55","slug":"the-8000th-busy-beaver-number-eludes-zf-set-theory-new-paper-by-adam-yedidia-and-me","status":"publish","type":"post","link":"https:\/\/scottaaronson.blog\/?p=2725","title":{"rendered":"The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me"},"content":{"rendered":"

I’ve supervised a lot of great student projects in my nine years at MIT, but my inner nerdy teenager has never been as personally<\/em> delighted by a project as it is right now.  Today, I’m proud to announce that Adam Yedidia, a PhD student at MIT (but an MEng student when he did most of this work), has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses.  Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.  In all three cases, this is the first time we’ve had a reasonable explicit upper bound on how many states you need in a Turing machine before you can see the behavior in question.<\/p>\n

Here’s our research paper<\/a>, on which Adam generously included me as a coauthor, even though he did the heavy lifting.  Also, here’s a github repository<\/a> where you can download all the code Adam used to generate these Turing machines, and even use it to build your own small Turing machines that encode interesting mathematical statements.  Finally, here’s a YouTube video<\/a> where Adam walks you through how to use his tools.<\/p>\n

A more precise statement of our main result is this: we give a 7,918-state Turing machine, called Z (and actually explicitly listed in our paper!), such that:<\/p>\n

    \n
  1. Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but<\/li>\n
  2. Z can’t be proved<\/em> to run forever in ZFC (Zermelo-Fraenkel set theory with the Axiom of Choice, the usual foundation for mathematics), assuming that ZFC is consistent.<\/li>\n<\/ol>\n

    A bit of background: it follows, as an immediate consequence of G\u00f6del’s Incompleteness Theorem, that there’s some<\/em> computer program, of some<\/em> length, that eludes the power of ordinary mathematics to prove what it does, when it’s run with an unlimited amount of memory.  So for example, such a program could simply enumerate all the possible consequences of the ZFC axioms, one after another, and halt if it ever found a contradiction (e.g., a proof of 1+1=3).  Assuming ZFC is consistent, this program must run forever.  But again assuming ZFC is consistent, ZFC can’t prove<\/em> that the program runs forever, since if it did, then it would prove its own consistency, thereby violating the Second Incompleteness Theorem!<\/p>\n

    Alas, this argument still leaves us in the dark about where<\/em>, in space of computer programs, the “G\u00f6delian gremlin” rears its undecidable head.  A program that searches for an inconsistency in ZFC is a fairly complicated animal: it needs to encode not only the ZFC axiom schema, but also the language and inference rules of first-order logic.  Such a program might be thousands of lines long if written in a standard programming language like C, or millions of instructions if compiled down to a bare-bones machine code.  You’d certainly never run across such a program by chance—not even if you had a computer the size of the observable universe, trying one random program after another for billions of years in a “primordial soup”!<\/p>\n

    So the question stands—a question that strikes me as obviously<\/em> important, even though as far as I know, only one or two people ever asked the question before us; see here<\/a> for example.  Namely: do the axioms of set theory suffice to analyze the behavior of every computer program that’s at most, let’s say, 50 machine instructions long?  Or are there super-short programs that already<\/em> exhibit “G\u00f6delian behavior”?<\/p>\n

    Theoretical computer scientists might object that this is “merely a question of constants.”  Well yes, OK, but the origin of life in our universe—a not entirely unrelated puzzle—is also “merely a question of constants”!  In more detail, we know that it’s possible<\/em> with our laws of physics to build a self-replicating machine: say, DNA or RNA and their associated paraphernalia.  We also know that tiny molecules like H2<\/sub>O and CO2<\/sub> are not self-replicating.  But we don’t know how small<\/em> the smallest self-replicating molecule can be—and that’s an issue that influences whether we should expect to find ourselves alone in the universe or find it teeming with life.<\/p>\n

    Some people might also object that what we’re asking about has already been studied, in the half-century quest to design the smallest universal Turing machine<\/a> (the subject of Stephen Wolfram’s $25,000 prize<\/a> in 2007, to which I responded with my own $25.00 prize<\/a>).  But I see that as fundamentally different, for the following reason.  A universal Turing machine—that is, a machine that simulates any other machine that’s described to it on its input tape—has the privilege of offloading almost all of its complexity onto the description format for the input machine.  So indeed, that’s exactly what all known tiny universal machines do!  But a program that checks (say) Goldbach’s Conjecture, or the Riemann Hypothesis, or the consistency of set theory, on an initially blank tape, has no such liberty.  For such machines, the number of states really does<\/em> seem like an intrinsic measure of complexity, because the complexity can’t be shoehorned anywhere else.<\/p>\n

    One can also phrase what we’re asking in terms of the infamous Busy Beaver function<\/a>.  Recall that BB(n), or the nth<\/sup> Busy Beaver number, is defined to be the maximum number of steps that any n-state Turing machine takes when run on an initially blank tape, assuming that the machine eventually halts. The Busy Beaver function was the centerpiece of my 1998 essay Who Can Name the Bigger Number?<\/a>, which might<\/i> still attract more readers than anything else I’ve written since. As I stressed there, if you’re in a biggest-number-naming contest, and you write “BB(10000),” you’ll destroy<\/em> any opponent—however otherwise mathematically literate they are—who’s innocent of computability theory.  For BB(n) grows faster than any computable sequence of integers: indeed, if it didn’t, then one could use that fact to solve the halting problem, contradicting Turing’s theorem.<\/p>\n

    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<\/em>, 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\u00f6del’s Theorem.<\/p>\n

    OK, but we can now ask a quantitative question: how many<\/em> values of the BB function is it possible for us to know?  Where exactly is the precipice at which this function “departs the realm of mortals and enters the realm of God”: is it closer to n=10 or to n=10,000,000?  In practice, four<\/em> values of BB have been determined so far:<\/p>\n