7 ms·

The Busy Beaver function is fascinating. Seemingly so easy to define: Of all possible turing machines with N states that eventually halt, what's the number of s

The Busy Beaver function is fascinating. Seemingly so easy to define: Of all possible turing machines with N states that eventually halt, what's the number of steps that the longest-running one takes? It's not "just" that this is uncomputable, given the halting problem. Lots of things in mathematics are uncomputable. What's special about this function is that it will eventually blast through the limits of what any given formalization of mathematics can prove at all, no matter how powerful -- like ZFC + CH + whatever other axioms you come up with.[1] To be honest, I can't fully wrap my head around what this means. Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would. That wouldn't make much sense to me at least, because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets. But I don't know. [1] Also from Scott Aaronson's blog, BB(8000) and above are independent from ZFC: https://scottaaronson.blog/?p=2725 https://scottaaronson.blog/?p=2725

Sharlin 4y ago
So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it can enumerate all theorems of ZF(C). But because of Gödel, at some point it must necessarily either get stuck in a loop or return "can’t prove or disprove this" for some candidate theorem. As I understand it, the result relayed by Scott proves that N=7198 – as in a state space of merely 13 bits – is sufficient to construct a Gödel-territory TM (but this is just an upper bound)! Having an unbounded tape as a scratch space helps, of course.
karatinversion 4y ago
> because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. And no finite enumeration of steps can prove that it doesn’t halt eventually. Since the statement is infinitary, it’s liable to avoid being probable if our axioms don’t capture it - and so computable set of axioms captures all true statements. And if we can’t prove that a particular Turing machine of N states doesn’t halt, we can’t prove any value for BB(N), as otherwise we could just staple the first BB(N) states of the Turing machine to show it doesn’t halt, which we can’t prove.
- nickdrozd 4y ago
  > Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. Machines that halt can always be proved to halt, as you say just by exhibiting them running to halting. (In principle at least; in practice this can be quite difficult.) Machines that don't halt fall into two groups: those that can be proved not to halt and those that cannot be proved not to halt. Provably non-halting machines are not rare or strange. For example, a machine can wind up getting stuck in one state that just moves off to the edge of the tape forever. If this happens, it's obvious that the machine will never halt, and that's provable. Sometimes non-haltingness has an infinitary character, but not always.
  - Retric 4y ago
    The incompleteness proof depends on the input to the program under consideration, BB is limited to programs that don’t have any input which makes the incompleteness proof irrelevant. For similar reasons you can have a solution to the halting problem given a program of infinite size that is only considering programs of finite size with finite inputs.
    - xyzzyz 4y ago
      This is not a material distinction: for every pair (M, input) you can create a machine M’ which has no actual input and instead first writes down the input to M onto the empty tape, and then runs M. This technique practically allows you to perform most of the same proofs on inputless machines. > For similar reasons you can have a solution to the halting problem given a program of infinite size. Sorry, what is a “program of infinite size” in context of Turing machines?
      - Retric 4y ago
        > This technique practically allows you to perform most of the same proofs on inputless machines. Emulating a machine allows you to know stuff that the machine being emulated can’t such as the width the the data written to the tape. It seems reasonable that you can still prove incompleteness, but I suspect it’s non trivial. > Sorry, what is a “program of infinite size” in the context of Turing machines. “The choice of which replacement symbol to write and which direction to move is based on a finite table that specifies what to do for each combination of the current state and the symbol that is read.” https://en.wikipedia.org/wiki/Wikipedia https://en.wikipedia.org/wiki/Wikipedia Replace “finite table” with “infinite table”.
jerf 4y ago
"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would." It can not. The TMs can only be affected by things that affect them at a finite level. To put it another way that may be easier to see, for them to have a different idea about a given BB number, there must be two otherwise identical machines facing their decision about what state to transfer into, but the one armed with the CH must choose one state and one without it must choose another. (There must always be some such first state, even if it is the very first transition.) There's nowhere to encode that inside a TM state transition table. That is the "outside" mechanics of a TM, which are fully defined by the problem itself. The "inner" mechanics of a TM, where we talk about what the machine is "really doing", may have such effects, but that's a bit more mundane. And not even necessarily relevant; while you may have two machines, one with ZFC+CH and one with ZFC without CH, they're both going to be hammered by a machine doing "something" that definitely isn't just running a clearly-defined axiomatic system over propositions, but something "mixed up" beyond all human understanding. What can affect the BB number is oracles. This is also in some sense "why" oracles are defined as essentially function calls that TMs can make with a sort of equivalent of a system call operation that user space code can use to invoke a kernel's functionality... you can easily encode that into a single finite state transfer. BB relative to an external oracle can be (and is) different than conventional BB. However, while the numbers are larger... much, much, much (etc.) larger... I think in some sense it's also less mathematically interesting and returns to just being "yet another large number generator"; BB is interesting precisely as the boundary between computability and non-computability, and BB+oracle is just straight-up uncomputable. But that's not that interesting, really; there's an infinite number of already-uncomputable functions anyhow.
- hakuseki 4y ago
  It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.

Sharlin 4y ago

So there exists a Turing machine (with some finite number of states N, naturally) that is just complex enough to encode ZF(C) and first-order logic such that it can enumerate all theorems of ZF(C). But because of Gödel, at some point it must necessarily either get stuck in a loop or return "can’t prove or disprove this" for some candidate theorem. As I understand it, the result relayed by Scott proves that N=7198 – as in a state space of merely 13 bits – is sufficient to construct a Gödel-territory TM (but this is just an upper bound)! Having an unbounded tape as a scratch space helps, of course.

karatinversion 4y ago

> because a Turing machine halting or not halting feels like a concrete fact that shouldn't depend on assumptions about weird infinite sets Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. And no finite enumeration of steps can prove that it doesn’t halt eventually. Since the statement is infinitary, it’s liable to avoid being probable if our axioms don’t capture it - and so computable set of axioms captures all true statements. And if we can’t prove that a particular Turing machine of N states doesn’t halt, we can’t prove any value for BB(N), as otherwise we could just staple the first BB(N) states of the Turing machine to show it doesn’t halt, which we can’t prove.

nickdrozd 4y ago
> Think about it this way. If a particular Turing machine halts, that’s a finitary fact: you can prove it by exhibiting a finite sequence of valid states for the Turing machine which ends in a halt. But if it doesn’t halt, that’s an infinitary statement: it doesn’t halt after N steps, for any N. Machines that halt can always be proved to halt, as you say just by exhibiting them running to halting. (In principle at least; in practice this can be quite difficult.) Machines that don't halt fall into two groups: those that can be proved not to halt and those that cannot be proved not to halt. Provably non-halting machines are not rare or strange. For example, a machine can wind up getting stuck in one state that just moves off to the edge of the tape forever. If this happens, it's obvious that the machine will never halt, and that's provable. Sometimes non-haltingness has an infinitary character, but not always.
- Retric 4y ago
  The incompleteness proof depends on the input to the program under consideration, BB is limited to programs that don’t have any input which makes the incompleteness proof irrelevant. For similar reasons you can have a solution to the halting problem given a program of infinite size that is only considering programs of finite size with finite inputs.
  - xyzzyz 4y ago
    This is not a material distinction: for every pair (M, input) you can create a machine M’ which has no actual input and instead first writes down the input to M onto the empty tape, and then runs M. This technique practically allows you to perform most of the same proofs on inputless machines. > For similar reasons you can have a solution to the halting problem given a program of infinite size. Sorry, what is a “program of infinite size” in context of Turing machines?
    - Retric 4y ago
      > This technique practically allows you to perform most of the same proofs on inputless machines. Emulating a machine allows you to know stuff that the machine being emulated can’t such as the width the the data written to the tape. It seems reasonable that you can still prove incompleteness, but I suspect it’s non trivial. > Sorry, what is a “program of infinite size” in the context of Turing machines. “The choice of which replacement symbol to write and which direction to move is based on a finite table that specifies what to do for each combination of the current state and the symbol that is read.” https://en.wikipedia.org/wiki/Wikipedia https://en.wikipedia.org/wiki/Wikipedia Replace “finite table” with “infinite table”.

jerf 4y ago

"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would." It can not. The TMs can only be affected by things that affect them at a finite level. To put it another way that may be easier to see, for them to have a different idea about a given BB number, there must be two otherwise identical machines facing their decision about what state to transfer into, but the one armed with the CH must choose one state and one without it must choose another. (There must always be some such first state, even if it is the very first transition.) There's nowhere to encode that inside a TM state transition table. That is the "outside" mechanics of a TM, which are fully defined by the problem itself. The "inner" mechanics of a TM, where we talk about what the machine is "really doing", may have such effects, but that's a bit more mundane. And not even necessarily relevant; while you may have two machines, one with ZFC+CH and one with ZFC without CH, they're both going to be hammered by a machine doing "something" that definitely isn't just running a clearly-defined axiomatic system over propositions, but something "mixed up" beyond all human understanding. What can affect the BB number is oracles. This is also in some sense "why" oracles are defined as essentially function calls that TMs can make with a sort of equivalent of a system call operation that user space code can use to invoke a kernel's functionality... you can easily encode that into a single finite state transfer. BB relative to an external oracle can be (and is) different than conventional BB. However, while the numbers are larger... much, much, much (etc.) larger... I think in some sense it's also less mathematically interesting and returns to just being "yet another large number generator"; BB is interesting precisely as the boundary between computability and non-computability, and BB+oracle is just straight-up uncomputable. But that's not that interesting, really; there's an infinite number of already-uncomputable functions anyhow.

hakuseki 4y ago
It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.