[HN Gopher] BusyBeaver(6) Is Quite Large
       ___________________________________________________________________
        
       BusyBeaver(6) Is Quite Large
        
       Author : bdr
       Score  : 260 points
       Date   : 2025-06-28 16:53 UTC (1 days ago)
        
 (HTM) web link (scottaaronson.blog)
 (TXT) w3m dump (scottaaronson.blog)
        
       | seeknotfind wrote:
       | > So I said, imagine you had 10,000,000sub10 grains of sand. Then
       | you could ... well, uh ... you could fill about 10,000,000sub10
       | copies of the observable universe with that sand.
       | 
       | I don't get this part. Is it really rounding away the volume of
       | the observable universe divided by the average volume of a grain
       | of sand? That is many more orders of magnitude than the amount of
       | mass in the universe, which is a more usual comparison.
        
         | Scarblac wrote:
         | Yes, that's only some normal number amount of orders of
         | magnitude. Even 10,000,000^10,000,000 is already so large that
         | it doesnt matter, let alone after exponentiating _the exponent_
         | nine times more.
        
           | wizzwizz4 wrote:
           | It's the other way around: we're talking about
           | 10^(10^(10^(10^...))) (which is _vastly_ bigger).
        
         | mckeed wrote:
         | With tetration you're not dealing with orders of magnitude
         | anymore, but orders of magnitude of orders of magnitude.
        
         | Chirono wrote:
         | Exactly. This number is so so much bigger than 10^100000 or
         | however many grains of sand would fit, that dividing by that
         | amount doesn't really change it, certainly not enough to bring
         | it down closer to 9,999,999sub10
        
         | Straw wrote:
         | Yes, that's right, dividing by that ratio essentially barely
         | affects the number in a sense that 'adjacent' numbers in that
         | notation give a much bigger change.
         | 
         | 10||10,000,000 / (sand grains per universe) is vastly larger
         | than, say, 10||9,999,999
         | 
         | So on system we're using to write these numbers, there's really
         | no better way to write (very big)/ (only universally big) than
         | by writing exactly that, and then in the notation for very big,
         | it pretty much rounds to just (very big).
        
         | lupire wrote:
         | Here's a more common example of this sort of comparison:
         | 
         | In significant figures, 1.0 billion minus 1.0 million equals
         | 1.0 billion.
        
           | Nevermark wrote:
           | True but this is a ratio.
           | 
           | However many universes in question, there is a qualitative
           | difference between that many empty universes (with 1 grain),
           | and that many completely packed with grain.
           | 
           | Ask anybody who lives in one!
        
             | fwip wrote:
             | At very large numbers, even ratios don't really matter.
             | 
             | For instance, if you personally owed $100 trillion, you
             | wouldn't be much relieved by a court order that reduced
             | your liability by 99%. Or, if you're looking at numbers in
             | scientific notation, you don't much care about the
             | difference between 2e40 and 5e40.
             | 
             | In this case, the ratio is around 10^200. An
             | incomprehensibly vast number, to be sure.
             | 
             | But because tetration is the next operator up from
             | exponentiation (the way exponents are from multiplication),
             | any fixed divisor ceases to "matter" very quickly. The
             | difference between 10^^10,000,000 and 10^^10,000,001 is
             | (10^^10,000,000 to the tenth power), if my understanding is
             | right.
             | 
             | There's basically no way to get it into comprehensible
             | territory even with repeated divisions. 10^^1 = 10, 10^^2 =
             | 10^10 (ten billion), and 10^^3 is 10^(10^10) =
             | 10^10,000,000. Already, dividing by 10^200 isn't going to
             | meaningfully affect your number (10^99,999,800).
             | 
             | 10^^10,000,000 is that kind of incomprehensible growth that
             | we just saw from 1 to 2 to 3, repeated 10 million times.
        
       | fjfaase wrote:
       | I wonder if the visible universe is large enough to write down
       | the exact value of BB(6).
        
         | Scarblac wrote:
         | It's not.
        
           | Alive-in-2025 wrote:
           | I want some easier to comprehend number for BB(6), in decimal
           | notation. But it's such a massive number I would need to
           | invent a new notation to express that. I love this new (to
           | me) concept of tetration number representation. 10-million
           | sub 10, what is the number?
           | 
           | Look at 3 sub 10 = which is (10^(10^10)). So that is 10 to
           | the power of 10 billion. In regular decimal notation, that is
           | a "1" with 10 billion "0"s following it. It takes 10
           | gigabytes of ram to represent the number in decimal notation,
           | naively.
           | 
           | The number of atoms in the universe is only 10^80, or
           | 1,000...000 (80 zeroes). 10-million sub 10 is so huge, how
           | much ram to represent it.
           | 
           | This example is from
           | https://www.statisticshowto.com/tetration-function-simple-
           | de...
        
         | kaashif wrote:
         | It definitely isn't. The amount of information you can store in
         | the universe is something like 10^120 bits. Even if I'm off by
         | a trillion orders of magnitude it doesn't matter.
        
         | aeve890 wrote:
         | If you treat the observable universe as a closed system, you
         | could try to apply the Bekenstein bound using - R [?] 46.5
         | billion light-years (radius of the observable universe) - E [?]
         | total mass-energy content of the observable universe
         | 
         | The mass-energy includes ordinary matter, dark matter, and dark
         | energy. Current estimates suggest the observable universe
         | contains roughly 10^53 kg of mass-energy equivalent.
         | 
         | Plugging these into S <= 2pER/c gives someting on the order of
         | 10^120 bits of maximum information content.
         | 
         | S <= 2pER/c
         | 
         | S <= (2 x 3.141593 x 3.036e+71 x 4.399e+26)/(1.055e-34 x
         | 299792458)
         | 
         | S <= 2.654135e+124
         | 
         | S <= 10^120
         | 
         | So, no.
        
         | Dylan16807 wrote:
         | Just the starting number in the article is 1510. That means
         | it's 10^(1410). That means it has 1410 digits. So no, you
         | can't.
        
         | layer8 wrote:
         | You're probably referring to a state where all parts of the
         | complete representation exist at the same time. Because if they
         | don't have to exist at the same time, then it might be possible
         | to "write it down" if the universe has unbounded duration
         | ("might" because I don't know how the heat death plays into
         | that). However, "at the same" time isn't well-defined in
         | relativistic spacetime. The sibling comments are definitely
         | right with respect to the reference frame implied by the CMB.
         | But I'm wondering if it wouldn't be possible to slice spacetime
         | in a way that actually makes a representation possible "at the
         | same time" in _some_ reference frame?
        
       | Scarblac wrote:
       | It boggles my mind that a number (an uncomputable number,
       | granted) like BB(748) can be "independent of ZFC". It feels like
       | a category error or something.
        
         | ChadNauseam wrote:
         | The number itself is not independent of ZFC. (Every integer can
         | be expressed in ZFC.) What's independent of ZFC is the process
         | of computing BB(748).
        
           | Straw wrote:
           | Sure, if someone just gives you the number, ZFC can represent
           | it. But ZFC cannot prove that the value is correct, so how do
           | you know you have the right number? Use a stronger proof
           | system? Go a bit bigger and same issue.
        
             | ajkjk wrote:
             | Not an expert, but I've read about this a bit because it
             | bothered me also and I think this is the answer:
             | 
             | Most of these 'uncomputable' problems are uncomputable in
             | the sense of the halting problem: you can write down an
             | algorithm that should compute them, but it might never
             | halt. That's the sense in which BB(x) is uncomputable: you
             | won't know if you're done ever, because you can't
             | distinguish a machine that never halts from one that just
             | hasn't halted yet (since it has an infinite number of
             | states, you can't just wait for a loop).
             | 
             | So presumably the independence of a number from ZFC is like
             | that also: you can't prove it's the value of BB(745)
             | because you won't know if you've proved it; the only way to
             | prove it is essentially to run those Turing machines until
             | they stop and you'll never know if you're done.
             | 
             | I'm guessing that for the very small Turing machines there
             | is not enough structure possible to encode whatever
             | infinitely complex states end up being impossible to deduce
             | halting from, so they end up being Collatz-like and then
             | you can go prove things about them using math. As you add
             | states the possible iteration steps go wild and eventually
             | do stuff that is beyond ZFC to analyze.
             | 
             | So the finite value 745 isn't really where the
             | infinity/uncomputability comes from-it comes from the
             | infinite tape that can produce arbitrarily complex
             | functions. (I wonder if over a certain number of states it
             | becomes possible to encoding a larger Turing machine in the
             | tape somehow, causing a sort of divergence to infinite
             | complexity?)
        
               | lupire wrote:
               | It has to come from a finite value (specifically, the
               | amount of complexity that can be enocoded in 745 pieces
               | of information
               | https://turingmachinesimulator.com/shared/vgimygpuwi),
               | because the finite size 745 with infinite tape leads to
               | uncomputability, but the size 5 does not.
               | 
               | In a very real sense, a deep kind of infinite complexity
               | can be generated from 745 objects of certain kind, but
               | not from 5 objects of that kind..
               | 
               | Turing machines have infinite tape, not infinite state.
               | The entire set of all halting machines of a given size
               | collectively only use finite tape. Totally finite. Only
               | (some of) the non-halting machines use infinite tape.
               | 
               | The problem is that we don't know in advance how large
               | the (definitely finite) upper bound on the amount of tape
               | all the size-N halting machines use, until after enough
               | of them (one per known equivalence class) halt. And we
               | don't know (in general) how to run all the halting ones
               | until they halt, without also running a non-halting
               | program for an unbounded amount of time.
               | 
               | TL:DR: unbounded is not infinite, but big enough to be a
               | problem.
        
               | ajkjk wrote:
               | I am aware it's an infinite tape and finite state (maybe
               | I misspoke somewhere), as well as the halting machines
               | using finite tape (because of course they do).
               | 
               | But the overall 'complexity' (at a timestep, say) is
               | going to be due to the states and the tape together. The
               | BB(5) example that was analyzed, iirc, was a Collatz-like
               | problem (Aaronson describes it here:
               | https://scottaaronson.blog/?p=8088 ). My interpretation
               | of this is that:
               | 
               | 1. collatz-like functions have a lot of complexity just
               | due to math alone 2. 5 states turned out to be enough to
               | "reach" that one that 3. more states means you're going
               | to reach more possible Collatz-like functions (they don't
               | have to be Collatz-like; it's just easier to think about
               | them like that) 4. eventually you reach ones that ZFC
               | cannot show to halt, because there is effectively no way
               | to prove it other than running them, and then you would
               | have to solve the halting problem.
               | 
               | The part that was helpful for me to be less unsettle by
               | BB(745) being independent of the ZFC was the notion that
               | it eventually boils down to a halting problem, and asking
               | ZFC to "solve" it... which is more agreeable than the
               | idea that "ZFC cannot compute a function that seems to be
               | solvable by brute force".
        
               | dtech wrote:
               | I am also not an expert, but this does not sound right to
               | me. Godel's incompleteness theorem shows that there are
               | certain things that cannot be proven. Being independent
               | of ZFC means that something is such a case. So BB(643)
               | being independent of ZFC means that we cannot prove or
               | disprove that a certain number is BB(643). Aka we don't
               | have the math to know for certain.
        
               | ajkjk wrote:
               | Yeah, but the vexing part is "how can that be true for
               | e.g. N=643 but not N=642"? What _happens_ at whatever
               | number it starts true at?
               | 
               | Incidentally, Godel's theorem eventually comes down to a
               | halting-like argument as well (well, a diagonal
               | argument). There is a presentation of it that is in like
               | less than one page in terms of the halting problem---all
               | of the Godel-numbering stuff is essentially an antiquated
               | proof. I remember seeing this in a great paper which I
               | can't find now, but it's also mentioned as an aside in
               | this blog post: https://scottaaronson.blog/?p=710
               | 
               | wait jk I found it: https://arxiv.org/abs/1909.04569
        
               | LegionMammal978 wrote:
               | > What _happens_ at whatever number it starts true at?
               | 
               | Usually, "what _happens_ " is that the machines become
               | large enough to represent a form of induction too strong
               | for the axioms to 'reason' about. It's a function of the
               | axioms of your theory, and you can add more axioms to
               | stave it off, but of course you can't prove that your new
               | axioms are consistent without even more axioms.
               | 
               | > There is a presentation of it that is in like less than
               | one page in terms of the halting problem---all of the
               | Godel-numbering stuff is essentially an antiquated proof.
               | 
               | Only insofar as you can put faith into the Church-Turing
               | thesis to sort out all the technicalities of enumerating
               | and verifying proofs. There still must be an encoding,
               | just not the usual Godel numbering.
        
               | thaumasiotes wrote:
               | > Incidentally, Godel's theorem eventually comes down to
               | a halting-like argument as well (well, a diagonal
               | argument).
               | 
               | > There is a presentation of it that is in like less than
               | one page in terms of the halting problem
               | 
               | Those are two very different ideas. Your second sentence
               | says that Godel's theorem is easy to prove if you have
               | results about the halting problem. Your first one says
               | that in order to prove Godel's theorem, you need to
               | establish results about the halting problem.
        
               | ajkjk wrote:
               | I'm saying that if you want to understand why Godel's
               | theorem is true, look at the one-paragraph proof based on
               | the halting problem, not the like 20-page one with Godel
               | numbers.
        
               | wasabi991011 wrote:
               | Wow that might be the best, most entertaining, and most
               | elucidating academic article I've ever read. Thanks for
               | sharing.
        
               | SAI_Peregrinus wrote:
               | Independence from ZFC means we can't prove that any given
               | number is BB(643) _using ZFC_. It doesn 't mean we can't
               | prove it at all, e.g. one could use a stronger set theory
               | like NBG which can prove the consistency of ZFC to verify
               | the value of BB(643). But there would be some n for which
               | BB(n) is independent of _that_ set theory, requiring a
               | yet-stronger theory, and so on ad infinitum.
               | 
               | ZF & ZFC are as important as they are because they're the
               | _weakest_ set theories capable of working as the
               | foundations of mathematics that we 've found. We can
               | always add axioms, but taking axioms away & still having
               | a usable theory on which to base mathematics is much more
               | difficult.
        
               | ajkjk wrote:
               | sure, but it is still very hard to wrap one's head around
               | how the value of a function can be independent of ZFC,
               | and how it could not be for (e.g.) 642 but then be true
               | for 643. That was the point of my post. It _seems_ like
               | you could just... run the function on every 643-state
               | input and see what the value is, which would in some
               | sense constitute a  "proof" in ZFC? but maybe not,
               | because you wouldn't even know if you had the answer?
               | That's the part that is so intriguing about it.
        
               | Scarblac wrote:
               | And also, if BB were computable, then it could be used to
               | solve the halting problem: run the Turing machine of size
               | n for BB(n) steps, and if it hasn't halted yet, it never
               | will. So the BB function is clearly not computable.
               | 
               | But to me as a layman that seems true regardless of
               | formal axioms chosen, but I guess I need to read that
               | linked thesis.
        
               | ajkjk wrote:
               | That is the standard argument for why BB is uncomputable
               | for general n, but it's not the same as why BB(n) would
               | be independent of ZFC for fixed n.
        
               | thaumasiotes wrote:
               | > Most of these 'uncomputable' problems are uncomputable
               | in the sense of the halting problem: you can write down
               | an algorithm that should compute them, but it might never
               | halt. That's the sense in which BB(x) is uncomputable:
               | you won't know if you're done ever, because you can't
               | distinguish a machine that never halts from one that just
               | hasn't halted yet (since it has an infinite number of
               | states, you can't just wait for a loop).
               | 
               | > So presumably the independence of a number from ZFC is
               | like that also: you can't prove it's the value of BB(745)
               | because you won't know if you've proved it; the only way
               | to prove it is essentially to run those Turing machines
               | until they stop and you'll never know if you're done.
               | 
               | These aren't similar ideas. You can't know if a machine
               | that hasn't halted yet will ever halt. But you can easily
               | know if a machine that has already halted was going to
               | halt.
               | 
               | Independence is the second case. For the value of BB(x)
               | to be independent of ZFC, one of two things must hold:
               | 
               | (1) ZFC is inconsistent, and therefore all statements are
               | independent of it.
               | 
               | (2) ZFC is consistent with two different statements,
               | "BB(x) = a" and "BB(x) = b" for two different a, b. This
               | means that a disproof of either statement cannot exist.
               | 
               | This, in turn, means that there is no observation you
               | could ever make that would distinguish between the values
               | a and b (for the identity of BB(x)). No matter what you
               | believe the value of BB(x) might secretly be, there are
               | _no consequences_ ; nothing anywhere could ever change if
               | the value turned out to be different. Because, if there
               | were an observable consequence of the value being
               | different, the hypothetical observation of that
               | consequence would be a disproof of the value that didn't
               | cause it, and no such disproof can exist.
               | 
               | Neither value, a or b, can be more true than the other as
               | the answer to the question "what is BB(x)?". It doesn't
               | make sense to consider that question to have an answer at
               | all.
        
               | Scarblac wrote:
               | What happens if you take the larger of a and b and run
               | all the Turing machines for that many steps?
        
               | thaumasiotes wrote:
               | What are a and b?
        
               | Kranar wrote:
               | Among all possible values of BB(n) for some fixed n, it's
               | the smallest such value that is the true value.
               | 
               | The issue is that there is no way within ZFC to determine
               | which value is the smallest.
        
               | josephcsible wrote:
               | > (2) ZFC is consistent with two different statements,
               | "BB(x) = a" and "BB(x) = b" for two different a, b. This
               | means that a disproof of either statement cannot exist.
               | 
               | > This, in turn, means that there is no observation you
               | could ever make that would distinguish between the values
               | a and b (for the identity of BB(x)). No matter what you
               | believe the value of BB(x) might secretly be, there are
               | no consequences; nothing anywhere could ever change if
               | the value turned out to be different. Because, if there
               | were an observable consequence of the value being
               | different, the hypothetical observation of that
               | consequence would be a disproof of the value that didn't
               | cause it, and no such disproof can exist.
               | 
               | There's one part of this I don't understand. "BB(x) = n"
               | means "there is at least one x-state Turing machine that
               | halts after exactly n steps, and there are no x-state
               | Turing machines that halt after more than n steps",
               | right? Then why wouldn't this approach work (other than
               | the numbers being way too big to actually do in this
               | universe)? WLOG, assume a < b. Run all possible x-state
               | Turing machines for b steps. If any halted on step b,
               | then you've disproved "BB(x) = a". If not, then you've
               | disproved "BB(x) = b".
        
             | thechao wrote:
             | We need to distinguish between a computer that's equivalent
             | to BB(n), and a computer big enough to compute the value of
             | the number that is BB(n). By (terrible) analogy: a 4004 can
             | be made to write a finite loop that describes how many
             | FLOPs the number 1 supercomputer can compute without,
             | itself, being able to usefully perform the computations of
             | that supercomputer. (The 4004 will run out of
             | memory/addressable disk space.) Similarly, we can no longer
             | build _decidable_ programs in ZFC that can compute the
             | number BB(748). Scott is saying that they now think this
             | "disassociation" might occur at BB(7)!
        
             | vhcr wrote:
             | Nobody can give you that number, because it's way bigger
             | than what can be represented in the universe.
        
           | nyrikki wrote:
           | To try and help people digging into this, the following
           | helped me.
           | 
           | Two lenses for trying to understand this are potentially
           | Chastain's limits on output of a lisp program being more
           | complex than the program itself [1] or Markov's proof that
           | you can't classify manifolds in d>= 4.
           | 
           | If you try the latter and need/want to figure out how the
           | Russian school is so different this is helpful [2]
           | 
           | IMHO the former gives an intuition why, and the latter
           | explains why IMHO.
           | 
           | In ZFC, C actually ends up implying PEM, which is why using
           | constructionism as a form of reverse math helped it click for
           | me .
           | 
           | This is because in the presence of excluded middle, every
           | sequentially complete metric space is a complete space, and
           | we tend to care about useful things, but for me just how huge
           | the search space grows was hidden due to the typical (and
           | useful) a priori assumption of PEM.
           | 
           | If you have a (in my view) dislike for the constrictive
           | approach or don't want/have to invest in learning an obscure
           | school of it, This recent paper[3] on the limits for finding
           | a quantum theory of everything is another lens.
           | 
           | Yet another path is through Type 2 TMs and the Borel
           | hierarchy, where while you can have a uncomputable number on
           | the input tape you algorithms themselves cannot use them,
           | while you can produce uncomputable numbers by randomly
           | selecting and/or changing an infinite sequence.
           | 
           | Really it is the difference between expressability and
           | algorithms working within what you can express.
           | 
           | Hopefully someone else can provide more accessible resources.
           | I think a partial understanding of the limits of algorithms
           | and computation will become more important in this new era.
           | 
           | [1] https://arxiv.org/abs/chao-dyn/9407003 [2]
           | https://arxiv.org/abs/1804.05495 [3]
           | https://arxiv.org/abs/2505.11773
        
             | drdeca wrote:
             | Looking at [3], they seem to argue that the system isn't
             | complete for the usual Godel reasons, which, sure, it
             | isn't, but then they call the claim that the system fails
             | to decide, which is a statement about probability, a
             | "scientific fact". This seems to me like a mistake?
             | 
             | Like, a TOE is not expected to decide all statements
             | expressible in the theory, only to predict particular
             | future states from past states, with as much specificity as
             | such past states actually determine the future states. It
             | should not be expected to answer "given a physical setup
             | where a Turing machine has been built, is there a time at
             | which it halts?" but rather to answer "after N seconds,
             | what state is the machine (as part of the physical system)
             | in?" (for any particular choice of N).
             | 
             | Whether a particular statement expressed in the language of
             | the theory is provable in the theory, is not a claim about
             | the finite-time behavior of a physical system, unless your
             | model of physics involves like, oracle machines or
             | something like that.
             | 
             | Edit: it later says: " Chaitin's theorem states that there
             | exists a constant K_{F_{QG}} , determined by the axioms of
             | F_{QG} , such that no statement S with Kolmogorov
             | complexity K(S) > K_{F_{QG}} can be proven within F_{QG} ."
             | 
             | But this, unless I'm badly misinterpreting it, seems very
             | wrong? Most formal systems of interest have infinitely many
             | distinct theorems. Given an infinite set of strings, there
             | is no finite universal upper bound on the Kolmogorov
             | complexity of the strings in that set.
             | 
             | Maybe this was just a typo or something?
             | 
             | They do then mention something about the Bekenstein bound,
             | which I haven't considered carefully yet but seems somewhat
             | more promising than the parts of the article that preceded
             | it.
        
               | tromp wrote:
               | It looks like the authors of [3] misunderstood Chaitin.
               | What Chaitin said about the limits of provability is that
               | no statements of the form "K(x) > c_F" can be proven in
               | formal system F where c_F is some constant depending on
               | F.
        
               | nyrikki wrote:
               | I will admit that I added that cite mostly because of the
               | very real barriers to even learning RUSS.
               | 
               | By the typos etc.. you. can probably also tell I was
               | doing this on mobile, unfortunately as a passenger in a
               | car.
               | 
               | To quote Chaitin's explanation here:
               | 
               | > In contrast I would like to measure the power of a set
               | of axioms and rules of inference. I would like to be able
               | to say that if one has ten pounds of axioms and a twenty-
               | pound theorem, then that theorem cannot be derived from
               | those axioms.
               | 
               | This paper's notation does seem to be confusing, but I
               | still think it is essentially complete with the above.
               | 
               | "K_{F_{QG}}" would probably most commonly be _L_ in most
               | descriptions, a natural number that is the upper bound of
               | complexity for provable statements in a formal system _S_
               | 
               |  _L_ is not a limit on complexity, it means that there is
               | no formal proof for _S_ that its Kolmogorov complexity
               | exceeds _L_ , for any string.
               | 
               | You can still prove that there are strings far more
               | complex than _L_ with _S_ , and in fact there will often
               | be far more of those strings than the ones equal to or
               | less than _L_.
               | 
               | It is a limit on what you can prove about those strings
               | with a greaterKolmogorov complexity in _S_.
               | 
               | Or to rewrite the above:
               | 
               | "There exists a natural number L such that we can't prove
               | the Kolmogorov complexity of any specific string of bits
               | is more than L."
               | 
               | Does that help or did I miss the mark on your objection?
        
           | bo1024 wrote:
           | I think the more correct statement is that there are
           | different models of ZFC in which BB(748) are different
           | numbers. People find that weird because they don't think
           | about non-standard models, as arguably they shouldn't.
        
             | Strilanc wrote:
             | Isn't that incompatible with the models being consistent?
             | 
             | Suppose model A proves BB(748) = X and model B proves
             | BB(748) = Y > X. But presumably the models can interpret
             | running all size 748 Turing machines for Y steps. Either
             | one of the machines halts at step Y (forming a proof within
             | A that BB(748) >= Y contradicting the assumed proof within
             | A that BB(748) = X < Y) or none of the machines halts at
             | step Y (forming a proof within B that BB(748) != Y
             | contradicting the assumed proof within B that BB(748) = Y).
             | 
             | I'm guessing the only way this could ever work would be
             | some kind of nastiness like X and Y aren't nailed down
             | integers, so you can't tell if you've reached them or not,
             | and somehow also there's a proof they aren't equal.
        
               | Kranar wrote:
               | The issue is that X and Y are not actual natural numbers.
               | They are mathematical objects that satisfy all the ZFC
               | axioms and Peano arithmetic but are infinitely large. The
               | issue is that ZFC underspecifies natural numbers.
        
             | wat10000 wrote:
             | How is that possible? That implies there's at least one
             | specific program whose execution changes based on the ZFC
             | model. The rules of program execution are so simple, it
             | doesn't make sense that they'd change based on anything
             | like that.
        
               | bo1024 wrote:
               | Because what it means to "halt in finite time" has
               | different meanings in different models, because time is
               | measured with different numbers.
        
               | wat10000 wrote:
               | I don't get it. Let's say that BB(748) is 10,000. (I
               | realize the true number is somewhat larger, this is just
               | an example that doesn't change the argument.) That means
               | there's one or more Turing machines of that size which
               | run for that many steps. All of the others either run for
               | fewer, or never stop.
               | 
               | Running for fewer steps is extremely well defined and I
               | don't imagine that enters into this.
               | 
               | That means there's issue is "never stop"? That also seems
               | pretty well defined to me. For BB(748) to vary based on
               | your model, if the machines that run for fewer steps
               | don't change, then that means one of the machines that
               | never stops in one model will stop in another. Or the BB
               | winner for our model will never stop in another model.
               | 
               | How can changing your model make it so a specific Turing
               | machine goes from stopping after 10,000 steps to never
               | stopping, or from never stopping to stopping after 11,000
               | steps?
        
               | Kranar wrote:
               | Yes the issue has to do with "never stops". One of the
               | machines that never stops in one model will stop in
               | another model.
               | 
               | So in one model a Turing Machine called R never stops. In
               | another model R stops after Q steps. But here's the
               | issue... Q isn't an _actual_ natural number, what it is
               | is some mathematical object that satisfies all of the
               | properties of a natural number in ZFC, but is not an
               | actual natural number. What it actually is is some
               | infinitely large object that satisfies all of the Peano
               | axioms of what a natural number is as well as satisfies
               | the following set of rules:                  Q > 0
               | Q > 1        Q > 2        Q > 3        ...
               | 
               | Q is basically some infinitely large construct that from
               | within the model appears to be finite, but from outside
               | of the model is not finite.
               | 
               | So within this model, the Turing machine R halts after Q
               | steps, and since from within the model Q is finite then
               | from within this model BB(748) is at least equal to Q.
               | 
               | If BB(748) is actually 10,000, then we can add this as an
               | axiom to ZFC to get a new formal theory ZFC + "BB(748) =
               | 10000".
               | 
               | In this new theory the previous structure that contained
               | Q as an element will not satisfy the definition of a
               | natural number, so we don't have to worry about Q
               | anymore... however, there will exist some number T > 748
               | where BB(T) is independent of our new theory. For BB(T),
               | there will exist some other model that has its own Q*
               | which satisfies all of our axioms including the axiom
               | that BB(748) = 10000, but also that                   Q*
               | > 0         Q* > 1         Q* > 2         Q* > 3
               | ...
               | 
               | And rinse and repeat...
        
               | wat10000 wrote:
               | What do you mean, Q isn't a natural number? If you had
               | unlimited time and paper, you could sit down and run the
               | machine by hand, counting each step, until it reaches the
               | halting state. You will have counted Q steps. Or the
               | machine never stops. There's no such thing as a machine
               | that stops after a number of steps defined by an
               | infinitely large construct. There are machines that stop
               | after some whole number of steps, and there are machines
               | that don't stop. There are no others.
               | 
               | If there's another model where this machine doesn't stop,
               | then that means that at some point during this process,
               | you reach a particular machine state and tape contents
               | and transition to a different state than you did in the
               | first model. That has to happen, because otherwise the
               | execution follows the same process as before, and halts
               | at Q steps. But the mechanics of the machine don't depend
               | on your theory. They're just state transitions and tape
               | operations.
        
               | Kranar wrote:
               | >What do you mean, Q isn't a natural number?
               | 
               | Q isn't a natural number because natural numbers must be
               | finite, but Q is infinitely large.
               | 
               | >If you had unlimited time and paper, you could sit down
               | and run the machine by hand, counting each step, until it
               | reaches the halting state. You will have counted Q steps.
               | 
               | What if the machine never stops? How many steps will you
               | run before you decide that the machine never halts?
               | 
               | >There's no such thing as a machine that stops after a
               | number of steps defined by an infinitely large construct.
               | 
               | There's no such thing as an _actual_ machine that stops
               | after an infinite number of steps, but that 's not the
               | issue. The issue is that ZFC has different models with
               | conflicting definitions of what infinite is. In one model
               | there is an object called Q that satisfies all of the
               | properties in ZFC of being a natural number, but is
               | infinitely large. In this model the Turing Machine halts
               | after Q steps. But there is another model, called the
               | standard model, and in this model there is no Q, all
               | elements of this model are actually finite, and in this
               | model the Turing machine never halts.
               | 
               | ZFC doesn't know which of these two models is the "real"
               | model of natural numbers. From within ZFC both of these
               | models satisfy all properties of natural numbers. It's
               | only from outside of ZFC that one of these models is
               | wrong, namely the model that contains Q as an element.
               | 
               | You can add more axioms to ZFC to get rid of the model
               | that has Q as an element, but if the resulting theory
               | containing your new axiom is consistent, then it
               | necessarily follows that there is some other model that
               | will contain some element Q* which is also infinitely
               | large but from within the theory satisfies all of the
               | new/stronger properties of being a natural number.
        
               | wat10000 wrote:
               | > In one model there is an object called Q that satisfies
               | all of the properties in ZFC of being a natural number,
               | but is infinitely large. In this model the Turing Machine
               | halts after Q steps.
               | 
               | That doesn't make any sense. A Turing machine can't halt
               | after a infinite number of steps. It either halts after a
               | finite number of steps, or it never halts.
               | 
               | I'm sure there are models of hypercomputation and
               | corresponding "what's the largest number of steps they
               | can run?" functions that would admit infinities, but
               | those would not be Turing machines and the function would
               | not be the Busy Beaver.
        
               | Kranar wrote:
               | There is a lot of nuance you are skipping over that needs
               | to be fully appreciated if you wish to understand this
               | topic.
        
               | wat10000 wrote:
               | I can accept that there is a lot of nuance on the math
               | side that I'm completely missing, but the Turing machine
               | side is really straightforward. A Turing machine either
               | never stops, or it stops after a finite number of steps.
               | If it stops, the number of steps that it runs is a finite
               | whole number, no different from "three" in its
               | relationship to infinity or its theoretical ability to be
               | written down. This doesn't depend on your mathematics,
               | only on your Turing machine.
        
               | bo1024 wrote:
               | The point is that when it "never stops", there are models
               | of ZFC in which the "infinity" number of steps it runs
               | for isn't considered infinity by the model, it's a made-
               | up "nonstandard" number that is smaller than infinity but
               | larger than any integer. And that model considers that to
               | be "halting", so that model says the TM halts.
        
               | wat10000 wrote:
               | That's just a change of definition. That isn't really
               | saying that BB(748) is different under a different model,
               | just that there's a BB' equivalent for that model and
               | BB'(748) is equal to something else.
        
               | raincole wrote:
               | It's not about hypercomputation.
               | 
               | What the commenter above you said doesn't make sense in
               | our daily life, but it makes perfect sense when in comes
               | to non-standard models.
               | 
               | You got confused because you're thinking natural numbers
               | as something we can count in real physical world, which
               | is a perfectly sane mental model, and that is why there
               | was a comment above said:
               | 
               | > People find that weird because they don't think about
               | non-standard models, as arguably they shouldn't.
               | 
               | Q is not a number you can actually count, so it doesn't
               | fit into our intuition of natural number. The point is
               | not that Q exists in some physical sense in real life,
               | like "3" in "3 apples" (it doesn't). The point is that ZF
               | itself isn't strong enough to prevent you from defining
               | random shit like Q as a natural number.
        
               | red75prime wrote:
               | > The point is not that Q exists in some physical sense
               | in real life
               | 
               | Ultrafinitism? If you'd run the Turing machine that
               | performs BB(748) steps in a physical universe that admits
               | it, you'd get a physical representation of BB(748). If
               | you have a competing theory about which Turing machine
               | computes BB(748), you can run them both alongside in this
               | universe and see with your own eyes which one finishes
               | first.
               | 
               | I guess from ultrafinitist's point of view such universe
               | has different mathematics, but isn't it a fringe
               | viewpoint in mathematical circles?
        
               | raincole wrote:
               | > ultrafinitism
               | 
               | I'm not sure what flavor of ultrafinitism you're
               | referring here. If it's the "very big numbers, like
               | TREE(3), are not natural numbers as they are far bigger
               | than the number of atoms in this universe..." kind, then
               | it has nothing to do with what this is about.
               | 
               | > physical representation
               | 
               | > your own eyes
               | 
               | Non standard models of ZFC have nothing to do with our
               | physical world. That's why no physicist or engineer cares
               | about them (or cares about axiom systems at all). So we
               | need to be very careful when connecting the idea of
               | physical, running "stuff" to the discussion of ZFC.
               | 
               | Anyway, back to
               | 
               | > you can run them both alongside in this universe and
               | see which one finishes first
               | 
               | There are two Turing Machines, Foo and Bar. We build and
               | run them in our physical universe. Foo halts at the
               | standard BB(748) steps. Bar just keeps running and
               | running. That's what we will see with our own eyes.
               | 
               | The issue is that when we try to reason out whether Bar
               | will ultimately halts, ZFC doesn't _prevent_ us from
               | defining a non-standard model where Bar halts after a
               | non-standard number of steps. Note that the physical Bar
               | will not halt in our universe. The  "non-standard number
               | of steps" is as nonsense as it sounds. It's just that ZFC
               | doesn't _prevent_ us from defining such a nonsense. The
               | point of ZFC is it 's compatible with almost all the
               | useful, sane math. It's not necessarily incompatible with
               | bullshit and insane math.
               | 
               | That is it. The fact that Bar is still keeping running in
               | our universe is completely irrelevant.
        
               | wat10000 wrote:
               | > ZFC doesn't prevent us from defining a non-standard
               | model where Bar halts after a non-standard number of
               | steps.
               | 
               | But it does prevent you from defining a non-standard
               | model where Bar halts after a _finite_ number of steps.
               | Since BB is finite by definition, the non-standard number
               | of steps after which Bar halts cannot be BB(748).
               | 
               | I'm pretty sure you and the other commenter have this
               | mixed up. The fact that BB(748) is independent of ZFC
               | doesn't mean there are different models that have
               | different values of BB(748). It means that ZFC is
               | insufficient to determine the value of BB(748). That
               | value is still some finite integer, you just can't prove
               | which one it is. Equivalently, there is some 748-state
               | Turing machine which never halts but ZFC cannot prove
               | never halts.
               | 
               | And no, you can't change your model such that this Turing
               | machine halts in some non-standard number of steps. Or
               | rather, you can, but that doesn't actually change
               | anything. The machine still doesn't halt for the purposes
               | of defining BB(748).
        
               | raincole wrote:
               | > I'm pretty sure you and the other commenter have this
               | mixed up.
               | 
               | We really don't.
               | 
               | > that BB(748) is independent of ZFC
               | 
               | > there are different models that have different values
               | of BB(748)
               | 
               | > ZFC is insufficient to determine the value of BB(748)
               | 
               | These three statements are equivalent.
               | 
               | f(n)=X is independent of ZFC means there are different
               | models of ZFC that have different values of f(n). It's a
               | very trivial theorem[0]. If you don't like it, I can't
               | convince you otherwise.
               | 
               | > that doesn't actually change anything
               | 
               | Changing the model will not change how any machine works
               | in our physical, mechanical universe. However, it does
               | change the value of BB(748).
               | 
               | I understand your line of thinking: There is only one
               | mechanical universe, which is the one where we exist. We
               | can build Turing machines in this universe. BB(n) depends
               | on Turning machines. Since there is only one single
               | universe, there is only one single value of BB(n).
               | 
               | It's a perfectly fine mental model for most cases. This
               | was exactly how I thought when the first time I heard
               | about BB(n). But it's not the kind of math than Scott
               | Aaronson et al. are doing.
               | 
               | Bar keeps running in our mechanical universe. But it can
               | also halt in some non-standard number of steps. This
               | weird, absurd-sounding proposition works because non-
               | standard numbers simply don't map to anything in
               | mechanical universe. They're purely abstract objects
               | living in ZFC+~Con(ZFC).
               | 
               | [0]: Given f(n)=X is independent of ZFC. Which means
               | f(n)=X and ~(f(n)=X) are both consistent relative to ZFC.
               | Therefore, if there is any model of ZFC, there is a model
               | M1 that entails ZFC+(f(n)=X), and a model M2 that entails
               | ZFC+~(f(n)=X). The value of f(n) cannot be the same in M1
               | and M2.
        
               | wat10000 wrote:
               | My argument has nothing to do with the universe. My
               | argument is that there is a single definition of the BB
               | function and its definition does not allow for different
               | values in different circumstances.
               | 
               | What is "a model" here? Can I say that there's a model
               | ZFC' which is the same as ZFC except that 107 is
               | considered to be equivalent to 200, and therefore BB(4)
               | in ZFC' is actually 200? Or can I say that ZFC'' says
               | integers only go up to 100 and therefore BB(4) is 100 in
               | that model? Or is it something more restricted than that?
        
               | raincole wrote:
               | > Or can I say that ZFC'' says integers only go up to 100
               | and therefore BB(4) is 100 in that model?
               | 
               | You'd be defining a new axiomatic system here, not just a
               | model of ZFC. I don't know how we're going to formalize
               | Turning machine in this system, but if we managed to do
               | it, the value of BB(4) is likely to be indeed 100, at
               | least for some models of this new system.
               | 
               | Roughly speaking, a model of ZFC is a set and a binary
               | relationship over the set, whose members all satisfy
               | every axiom of ZFC. Obviously this super simplified
               | definition does a crazy amount of handwaving.
               | 
               | But we don't need to accept or understand the idea of
               | model. What we need to accept is this simple idea:
               | 
               | An axiomatic system can be consistent, but _wrong_.
               | 
               | For example, if ZFC is consistent, then T = ZFC+~Con(ZFC)
               | would be consistent as well. But this T is _wrong_ , as
               | it believes ZFC is inconsistent.
               | 
               | Similarly, if ZFC is indeed consistent, then T is _wrong_
               | about which Turing machines halt. Therefore it would have
               | a _wrong_ value of BB(748) (and many other BB(n)).
               | 
               | However, since ZFC can't prove its own consistency, it
               | can't prove that value is _wrong_. That 's why there are
               | different values of BB(748). Those values are not
               | necessarily equally _correct_ , it's just that ZFC isn't
               | strong enough to prove which one is _wrong_.
               | 
               | Models, nonstandard natural numbers, etc... are more or
               | less technical details (so mathematicians can avoid scary
               | terms like 'wrong'.)
        
               | red75prime wrote:
               | > The "non-standard number of steps" is as nonsense as it
               | sounds.
               | 
               | That is we can add a nonsensical axiom and get a
               | consistent nonsensical theory that has nothing to do with
               | actually running Turing machines (no matter in which
               | physical or abstract universe they run). Er, OK, fine I
               | guess.
               | 
               | A universally inapplicable theory.
               | 
               | No. I can't wrap my head around it. Successors for the
               | tape state are defined for the initial segment of a non-
               | standard natural numbers. How the proof of termination
               | would even look like? Something non-constructive that
               | doesn't allow to choose the machine among a finite number
               | of the machines?
        
               | wat10000 wrote:
               | But Q is a number you can actually count, for a
               | definition of "actually" that includes unimaginably large
               | space and time. That finiteness comes from the basic
               | mechanics of the Turing machine, which don't depend on
               | your mathematical axioms.
               | 
               | Sure, you can come up with a set of axioms where the
               | natural numbers include infinities. You may be able to
               | use it to prove interesting things. But all that does
               | here it make it so that the set of numbers describing how
               | many steps a Turing machine runs before it stops is no
               | longer the "natural numbers."
        
         | Straw wrote:
         | The category error is in thinking that BB(748) is in fact, a
         | number. It's merely a mathematical concept.
        
           | Almondsetat wrote:
           | As if numbers weren't merely mathematical concepts
        
           | jerf wrote:
           | No, that's one of the freakiest things about things like the
           | Busy Beaver function. There is an exact integer that BB(748)
           | defines. You can add one to it and then it would no longer be
           | that number anymore.
           | 
           | If you are refering to the idea that nothing that can't exist
           | in the real universe "really exists", then the "Busy Beaver"
           | portion of that idea is extraneous, as 100% of integers can't
           | exist in the real universe, and therefore, 100% of integers
           | are equally just "mathematical concepts". That one of them is
           | identified by BB(748) isn't a particularly important aspect.
           | But certainly, a very specific number is identified by that
           | designation, though nothing in this universe is going to know
           | what it is in any meaningful sense.
        
             | perthmad wrote:
             | This integer only exists if you assume classical logic.
             | Otherwise, there is no such integer a priori, and actually
             | there is none in general.
        
               | nyssos wrote:
               | Classical logic is the presumed default for mathematics,
               | if someone is working in a different system they will say
               | so explicitly.
        
               | gylterud wrote:
               | Pondering mathematical objects such as BB(n) is exactly
               | the kind of stuff which rooks one's faith in classical
               | logic.
        
               | jerf wrote:
               | I'm fairly certain that's wrong, and I see a couple of
               | other people may be making that mistake elsewhere in this
               | conversation too. A Turing Machine is a Turing Machine.
               | The execution trace of a Turing Machine is fully
               | determined by its ruleset and its initial input. It
               | doesn't matter which axioms you "take", nor does it
               | matter what the intent of the initial construction of the
               | 748-state machine was, or indeed even if that proof is
               | somehow flawed. The definition of a Turing Machine is
               | effectively the axiom set for this particular case. There
               | is a finite set of 748-state Turing machines, and it is
               | absolutely the case that there is a set of them that loop
               | infinitely, the complementary set that do not, and that
               | there is a maximum length amoung the set that do not.
               | There is no situation where "the next step" of the Turing
               | Machine "depends on your axioms" and could thereby be
               | affected by such a decision.
               | 
               | For that to be the case, there would _have_ to be some
               | symbol under the tape and some state the machine is in
               | for which the action the machine takes and the next state
               | it goes to would depend on the axioms taken somehow.
               | There is no place where the Turing Machine has somehow
               | been running for so long and just gotten so large that
               | its behavior becomes non-deterministic somehow.
               | 
               | What this means is that even if we lived in a universe
               | where we had the unfathomable resources to actually have
               | this number somehow meaningfully "in hand", we would be
               | unable to prove that it was the correct one with just
               | ZFC. Maybe one of the really quite numerous other
               | machines still spinning away would in fact terminate in
               | the future and be the real BB winner, because even this
               | staggeringly monstrously large universe is still piddling
               | nothing next to infinity and the other machines still
               | require infinite resources to run them to discover they
               | never terminate. But that doesn't do anything to affect
               | whether or not there in fact is a single concrete integer
               | that corresponds to BB(748).
               | 
               | Although one imagines that any universe with the
               | resources to "have" BB(748) in it might also have some
               | much more powerful axiom systems to play with in the
               | process. The amount of computational power this universe
               | apparently possesses is beyond all comprehension and who
               | knows what they could know. But even if they used a more
               | powerful system, it wouldn't change what BB(748) is... it
               | just might affect whether or not they were _correct_
               | about it.
        
               | LegionMammal978 wrote:
               | > There is no situation where "the next step" of the
               | Turing Machine "depends on your axioms" and could thereby
               | be affected by such a decision.
               | 
               | That's easy, you just have to be an ultrafinitist, and
               | say, "The definition of a TM presupposes an infinite set
               | of natural numbers for time steps and tape
               | configurations. But there aren't actually infinitely many
               | natural numbers, infinitely long executions, arbitrarily
               | long proofs, etc., outside of the formalism. If a formal
               | statement and its negation do not differ regarding any
               | natural numbers small enough to actually exist (in
               | whatever sense), then neither is more true than the
               | other." In particular, consistency statements may have no
               | definite truth value, if the hypothetical proof of an
               | inconsistency would be too large.
               | 
               | Of course, metamathematics tells us "you can't do that,
               | in principle you could tell the lie if you wrote out the
               | whole proof!" But that principle also presupposes the
               | existence of arbitrarily-long proofs.
               | 
               | (Personally, hearing some of the arguments people make
               | about BB numbers, I've become attracted to agnosticism
               | toward ultrafinitist ideas.)
        
               | jerf wrote:
               | To be honest I'm not even particularly impressed by that
               | line of reasoning because even if you accept
               | ultrafinitism, there's still a definite _integer_ that it
               | corresponds to. You can deny the  "existence" of
               | integers, and thus that the number "exists", but that's
               | contingent on your definition of "existence". It doesn't
               | change what it would be if it did exist.
               | 
               | Plus, ultafinitism is essentially relative to the
               | universe you find yourself in. I hypothesized a universe
               | in which BB(748) could actually exist, but you can
               | equally hypothesize ones in which not only can it exist,
               | it exists _comfortably_ and is considered a small number
               | by its denizens. We can 't conceive of such a thing but
               | there's no particular a priori reason to suppose it
               | couldn't exist. If such a universe does actually "exist"
               | does that mean our ultrafinitism is wrong? I'm actually a
               | sort of a proponent of _knowing_ whether your operating
               | in a math space that corresponds to the universe (see
               | also constructive mathematics), but concretely declaring
               | that nothing could possibly exist that doesn 't fit into
               | _our_ universe is a philosophical statement, not a
               | mathematical one.
        
               | LegionMammal978 wrote:
               | > there's still a definite _integer_ that it corresponds
               | to.
               | 
               | The formalism _says_ that there 's still a definite
               | integer that it corresponds to. The ultrafinitist would
               | deny that the formalism keeps capturing truth past where
               | we've verified it to be true, or some unknown distance
               | farther.
               | 
               | > I hypothesized a universe in which BB(748) could
               | actually exist, but you can equally hypothesize ones in
               | which not only can it exist, it exists _comfortably_ and
               | is considered a small number by its denizens.
               | 
               | Sure, but the ultrafinitist would argue, "All this is
               | still just a shallow hypothesis: you've said the words,
               | but that's not enough to breathe much 'life' into the
               | concept. It is but the simplest of approximations that
               | can fit into our heads, and such large things (if they
               | could exist) would likely have an entirely different
               | nature that is incomprehensible to us."
               | 
               | > We can't conceive of such a thing but there's no
               | particular a priori reason to suppose it couldn't exist.
               | 
               | That's why I wouldn't call myself an ultrafinitist, but
               | would prefer an agnostic approach. There may be no great
               | _a priori_ reason to suppose it cannot exist, but I
               | similarly do not see any such reason it must
               | _necessarily_ exist. We empirically notice that our
               | formalism works for numbers small enough to work with,
               | and we pragmatically round it off to  "this formalism is
               | true", but one could argue that surprising claims about
               | huge numbers need stronger support than mere pragmatism.
        
             | Dylan16807 wrote:
             | > that's one of the freakiest things about things like the
             | Busy Beaver function
             | 
             | Every sentence ever spoken and every view ever looked at is
             | also a number. It's not a freaky thing about "things like"
             | busy beaver, it's a freaky thing about the concept of
             | information.
             | 
             | But even though everything is a number, saying "it's crazy
             | that a number can be X" is usually someone making a
             | mistake, using the everyday concept of numbers in their
             | head. If you replace "a number" with "some text and code
             | and data", people wouldn't say it's surprising that "some
             | text and code and data" can be unprovable in ZFC.
             | 
             | Technically a photograph is a number, but _primarily_ it 's
             | something else. BB(748) is the same, technically a number
             | but primarily it's a series of detailed computer
             | calculations.
        
               | gnramires wrote:
               | > Every sentence ever spoken and every view ever looked
               | at is also a number. It's not a freaky thing about
               | "things like" busy beaver, it's a freaky thing about the
               | concept of information.
               | 
               | I'd say that's a bit of a wrong or misleading statement.
               | I think the correct version is "everything[1] can be
               | _encoded_ as a number ". The concept of number is a very
               | particular concept! It's pretty absurd to say "a
               | screwdriver is a number" or "a word is a number". That is
               | true for the peano axiomatization of numbers; but to me
               | in particular, I believe numbers are a generalization
               | (and formalization) of the idea or concept of quantity.
               | There's a particular idea that refers to say 'two'
               | apples, the quantity of apples. A word is not a quantity,
               | it's a different concept. Even though each of them could
               | be encoded as a number somehow!
               | 
               | [1]: Everything that we believe to be finite and of
               | interest, that is. We don't know presently anything that
               | could be used in reality (a music, picture, etc.) that
               | can't in principle be encoded as a large enough number.
               | 
               | I think this is quite interesting, because this encoding
               | is critical, and it completes the system. You essentially
               | need a machine to turn things into numbers and numbers
               | into things; and this is unavoidable. You can actually
               | encode this machine itself with numbers! This number
               | (which encodes this transcoding machine) can even be
               | decoded by its own machine! But we cannot actually avoid
               | the machine itself, some actual realization in the real
               | world, because any number, in order to represent
               | something, can only be translated by one "machine" (which
               | can be essentially a computer, or a mind, etc.).
               | 
               | Instead of thinking of machines, you can also think of
               | conventions. So you can have a convention that say the
               | number '5' encodes the concept 'word', or maybe it simply
               | encodes the string of letters "word" ("w"+"o"+"r"+"d").
               | But the convention interpretation isn't complete, because
               | you still need someone, or something, to interpret this
               | convention in practice and potentially turn concepts into
               | reality, or simply manipulate those concepts in
               | significant and useful ways.
               | 
               | Some more examples: (1) you can encode objects by
               | describing a series of solid operations, essentially CAD
               | modelling, so you have numbers that represent solids. The
               | machine that interprets this number and is able to
               | translate it for example into a picture, a series of
               | instructions to be interpreted by a 3d printer, of
               | performs operations (inferences) about the relevant solid
               | model (for example, a structural analysis) is your
               | "machine", i.e. your software, without which a number, or
               | string of bits by itself doesn't mean anything (except
               | the quantity associated with that binary number,
               | perhaps), and again this encoding or number is
               | essentially arbitrary, it could be very different. (2) a
               | JPEG file for example encodes an image that is read by a
               | software stack (jpeg decoder+picture viewer+operating
               | system+display driver) and forwarded to your monitor to
               | be viewed as a pixel array. Again the string of bits
               | associated with any image could in principle represent
               | anything else representable.
               | 
               | Information (Shannon information in particular) simply
               | implies the encoding possible.
               | 
               | It's really interesting that a lot of the time we are
               | performing essentially translations between different
               | representations of a thing: a series of bits into states
               | of pixels on a screen (a picture), [a series of bits]
               | into a 3d printed object, into a visualization of an
               | object on a screen, etc. (one way), or a reading of a
               | camera sensor (photograph) into a series of bits, a
               | conception of an object (3d modelling), a conception of a
               | story (writing), etc. (the other way). We of course can
               | (and must for them to be built of course) conceptualize
               | those "machines" themselves (e.g. the software part),
               | represent them in some way (our encoding), and then turn
               | this representation into a realization of those machines
               | (a software, a piece of hardware, or just a
               | representation convention, etc.).
               | 
               | In other words, the mind or computer itself is always an
               | integral part of the process, and information in a vacuum
               | doesn't represent anything necessarily.
               | 
               | Finally, most of what we do is some kind of translation,
               | inference, and construction -- everything to assist our
               | lives. Of course some "machines" are capable of
               | generating new concepts, those are very interesting
               | "machines" :)
        
               | Dylan16807 wrote:
               | > I'd say that's a bit of a wrong or misleading
               | statement. I think the correct version is "everything[1]
               | can be encoded as a number". The concept of number is a
               | very particular concept! It's pretty absurd to say "a
               | screwdriver is a number" or "a word is a number". That is
               | true for the peano axiomatization of numbers; but to me
               | in particular, I believe numbers are a generalization
               | (and formalization) of the idea or concept of quantity.
               | There's a particular idea that refers to say 'two'
               | apples, the quantity of apples. A word is not a quantity,
               | it's a different concept. Even though each of them could
               | be encoded as a number somehow!
               | 
               | Well if we're using a more narrow view, then "BB(748)"
               | isn't a number, it's an encoding of a partial algorithm.
               | And it still shouldn't be surprising that an algorithm
               | might be unprovable in ZFC.
               | 
               | The actual number, the _quantity_ , is quite easy to
               | write down inside ZFC. And so is the beaver turing
               | machine itself. The hard part is knowing which of the
               | 748-state machines _is_ the beaver.
        
           | dtech wrote:
           | It's as much a number as 12
        
             | lupire wrote:
             | Only if you believe that a number you can't count is a
             | number. You can believe that, but it's a leap.
        
               | falcor84 wrote:
               | Couldn't you make the same argument for sqrt(2), or
               | better yet for zero [0]?
               | 
               | [0] https://en.wikipedia.org/wiki/Zero:_The_Biography_of_
               | a_Dange...
        
               | Dylan16807 wrote:
               | For sqrt(2) I can tell you the order of magnitude and
               | output as many digits as you want. I think that's plenty
               | specific for this use case.
               | 
               | For zero I can not only do that, I can also count to it
               | if you let me count both up and down, which seems like a
               | very simple ask.
        
               | falcor84 wrote:
               | But that's the thing - each generation struggles with
               | whether some new thing is a number. We're typically very
               | inclusive, accepting imaginary numbers and even weirder
               | things like surreal numbers, which we definitely can't
               | count.
               | 
               | But as someone in this generation, I see a good argument
               | for rejecting the big busy beaver numbers, which are
               | provably outside of the realm of calculating with all the
               | resources of our universe's runtime, from being fully
               | accepted as numbers, any more than the first
               | uninteresting number [0].
               | 
               | [0]
               | https://en.wikipedia.org/wiki/Interesting_number_paradox
        
           | Scarblac wrote:
           | There is a finite number of Turing machines of size 748. The
           | number of them that eventually halt is thus also finite, and
           | BB(748) is the highest number of steps in the finite list of
           | how many steps each took to halt. It has to be a number.
           | 
           | We just can't prove which number it is, we don't know which
           | of the machines halt.
        
           | gylterud wrote:
           | A constructive mathematician would indeed deny that BB(748)
           | is a well defined number. One could define it as a predicate
           | on natural numbers, but lest we find a contradiction in ZFC
           | we cannot hope to constructively prove that it holds for any
           | number.
        
           | bmacho wrote:
           | Let S be a statement. S is called _semidecidible_ (also:
           | Turing recognizable, most commonly  "recursively enumerable",
           | abbreviated as "r.e.", but I hate that one) if there is a
           | Turing machine that halts if and only if S is true.
           | 
           | With this definition, we can say that "ZFC is inconsistent"
           | is semidecidible: you run a program that searches for a
           | contradiction.
           | 
           | The question BB(748) =/= 1000 is similarly semidecidable. You
           | can run a program that _will_ rule out 1000 if it is not
           | BB(748).
           | 
           | So they are in the same "category", at least regarding their
           | undecidability.
           | 
           | Also, if you turn "ZFC is consistent" into a number: {1 if
           | ZFC is consistent; 0 if ZFC is inconsistent}, you will see,
           | that BB(748) is not very much different, both are defined
           | (well, equivalently) using the halting of Turing machines,
           | or, the result of an infinite search.
        
         | Xcelerate wrote:
         | It boggles my mind that we ever thought a small amount of text
         | that fits comfortably on a napkin (the axioms of ZFC) would
         | ever be "good enough" to capture the arithmetic truths or
         | approximate those aspects of physical reality that are
         | primarily relevant to the endeavors of humanity. That the
         | behavior of a six state Turing machine might be unpredictable
         | via a few lines of text does not surprise me in the slightest.
         | 
         | As soon as Godel published his first incompleteness theorem, I
         | would have thought the entire field of mathematics would have
         | gone full throttle on trying to find more axioms. Instead, over
         | the almost century since then, Godel's work has been treated
         | more as an odd fact largely confined to niche foundational
         | studies rather than any sort of mainstream program (I'm aware
         | of Feferman, Friedman, etc., but my point is there is
         | significantly less research in this area compared to most other
         | topics in mathematics).
        
           | azan_ wrote:
           | > As soon as Godel published his first incompleteness
           | theorem, I would have thought the entire field of mathematics
           | would have gone full throttle on trying to find more axioms.
           | 
           | But why? Godel's theorem does not depend on number of axioms
           | but on them being recursively enumerable.
        
             | tliltocatl wrote:
             | Godel's theorem shows that you need an infinite number of
             | axioms to describe reality (given that available reality
             | isn't finite), so any existing axiomatic system isn't
             | enough.
        
               | azan_ wrote:
               | Well, obviously we could simply take every true sentence
               | of Peano arithmetic as an axiom to obtain a consistent
               | and complete system, but if we think in that spirit, then
               | almost every mathematician in the world is working on
               | finding a better set of axioms (because every proof would
               | either give us new axiom or show that something should
               | not be included as axiom), right?
        
               | Xcelerate wrote:
               | > obviously we could simply take every true sentence of
               | Peano arithmetic as an axiom to obtain a consistent and
               | complete system
               | 
               | If you're talking about every true sentence in the
               | _language of PA_ , then not all such sentences are
               | derivable via the theory of PA. If you are talking about
               | the theorems of PA, then these are missing an infinite
               | number of true statements in the language of PA.
               | 
               | Harvey Friedman's "grand conjecture" is that virtually
               | every theorem that working mathematicians actually
               | publish can already be proved in Elementary Function
               | Arithmetic (much weaker than PA in fact). So the majority
               | of mathematicians are not pushing the boundaries of the
               | existing foundational theories of mathematics, although
               | there is certainly plenty of activity regardless.
        
             | Xcelerate wrote:
             | Right, Hilbert's goal was (loosely speaking) to "find a
             | finitely describable formal system" sufficient to "capture
             | all truths". When Godel showed that can't be done, that
             | shouldn't imply we just stop with the best theory we have
             | so far and call it a day--it means there are an infinite
             | number of more powerful theories (with necessarily longer
             | minimal descriptions) waiting to be discovered.
             | 
             | In fact, both Godel and Turing worked on this problem quite
             | a bit. Godel thought we might be able to find some sort of
             | "meta-principle" that could guide us toward discovering an
             | ever increasing hierarchy of more powerful axioms, and
             | Turing's work on ordinal progressions followed exactly this
             | line of thinking as well. Feferman's completeness theorem
             | even showed that all arithmetical truths could be
             | discovered via an infinite process. (Now of course this
             | process is not finitely axiomatizable, but one can
             | certainly extract some useful finite axioms out of it --
             | the strength of PA after all is equivalent to the recursive
             | iteration up to e_0 of 'Q_{n+1} = Q_n + Q_n is consistent'
             | where Q_0 is Robinson arithmetic).
        
           | czbot wrote:
           | Within ZFC one can prove that any two models of second order
           | PA are isomorphic. ZFC proves that PA is consistent. ZFC is
           | good enough to capture arithmetical truth.
        
             | cevi wrote:
             | Unfortunately no, ZFC isn't good enough to capture
             | arithmetical truth. The problem is that there are
             | nonstandard models of ZFC where every single model of
             | second-order PA within is itself nonstandard. There are
             | even models of ZFC where a certain specific computer
             | program, known as the "universal algorithm" [1], solves the
             | halting problem for all standard Turing machines.
             | 
             | https://jdh.hamkins.org/the-universal-algorithm-a-new-
             | simple...
        
               | czbot wrote:
               | ZFC allows models of second order PA and proves that
               | those models are all isomorphic. Within each model of ZFC
               | there is no such thing as a nonstandard model of second
               | order PA. One can only think it is nonstandard by looking
               | from outside the model, no? What theorem of second order
               | PA is ZFC unable to prove?
               | 
               | This is similar to how there are countable models of ZFC
               | but those models think of themselves as uncountable. They
               | are countable externally and not internally.
        
               | cevi wrote:
               | The consistency of ZFC is (presumably) a theorem of
               | second order PA, and ZFC is unable to prove it (unless
               | ZFC is inconsistent).
        
               | czbot wrote:
               | Indeed yes. But in a sense within ZFC one can say what N
               | is given the categorical nature of second order PA. Each
               | model of ZFC will have, up to isomorphism, one model of
               | N.
        
           | hyperpape wrote:
           | This ignores the fact that it is not so easy to find natural
           | interesting statements that are independent of ZFC.
           | 
           | Statements that are independent of ZFC are a dime a dozen
           | when doing foundations of mathematics, but they're not so
           | common in many other areas of math. Harvey Friedman has done
           | interesting work on finding "natural" statements that are
           | independent of ZFC, but there's dispute about how natural
           | they are. https://mathoverflow.net/questions/1924/what-are-
           | some-reason...
           | 
           | In fact, it turns out that a huge amount of mathematics does
           | not even require set theory, it is just a habit for
           | mathematicians to work in set theory.
           | https://en.wikipedia.org/wiki/Reverse_mathematics.
        
             | Xcelerate wrote:
             | Yeah, I'm quite familiar with Friedman's work. I mentioned
             | him and his Grand Conjecture in another comment.
             | 
             | > This ignores the fact that it is not so easy to find
             | natural interesting statements that are independent of ZFC.
             | 
             | I'm not ignoring this fact--just observing that the sheer
             | difficulty of the task seems to have encouraged
             | mathematicians to pursue other areas of work beside
             | foundational topics, which is a bit unfortunate in my
             | opinion.
        
               | hyperpape wrote:
               | I agree most working mathematicians have limited interest
               | in foundational topics. To me, that seems harmless
               | enough.
               | 
               | > approximate those aspects of physical reality that are
               | primarily relevant to the endeavors of humanity.
               | 
               | This is the comment that made me think that you were
               | saying we needed more work on foundations for math as it
               | is used in the sciences, and that doesn't match my
               | understanding. Did I read it differently than you meant
               | it?
        
           | throwaway81523 wrote:
           | > It boggles my mind that we ever thought a small amount of
           | text that fits comfortably on a napkin (the axioms of ZFC)
           | would ever be "good enough" to capture the arithmetic truths
           | or approximate those aspects of physical reality that are
           | primarily relevant to the endeavors of humanity.
           | 
           | ZFC is way overpowered for that.
           | https://mathoverflow.net/questions/39452/status-of-harvey-
           | fr...
        
             | Xcelerate wrote:
             | I don't understand your post. You're linking to a
             | discussion about the same conjecture I mentioned in another
             | comment 11 hours prior to your comment. Did you mean to
             | link something else?
        
               | throwaway81523 wrote:
               | I didn't notice your other post mentioning the
               | conjecture. Anyway, one thing it might mean is that we
               | humans have a very limited understanding of mathematics.
        
         | tromp wrote:
         | What makes BB(748) independent of ZFC is not its value, but the
         | fact that one of the 748-state machines (call it TM_ZFC_INC)
         | looks for an inconsistency (proof of FALSE) in ZFC and only
         | halts upon finding one.
         | 
         | Thus, any proof that BB(748) = N must either show that
         | TM_ZF_INC halts within N steps or never halts. By Godel's
         | famous results, neither of those cases is possible if ZFC is
         | assumed to be consistent.
        
           | Scarblac wrote:
           | I don't understand, surely if we assume ZFC is consistent
           | then it's obvious that it won't halt? Even if its consistency
           | can't be proven, neither can its inconsistency, so it won't
           | halt. Or is _that_ only provable outside of ZFC?
           | 
           | I guess it's also hard when we have an _arbitrary_ Turing
           | machine and have to prove that what it 's doing isn't
           | equilavent to trying to prove an undecibable statement.
        
             | tromp wrote:
             | If we assume ZFC to be consistent, then Godel's 2nd
             | incompleteness theorem tells us that it cannot prove its
             | own consistency. So in particular it cannot prove than
             | TM_ZFC_INC will never halt.
        
             | LegionMammal978 wrote:
             | If you believe that ZF is consistent, then you believe that
             | the machine cannot halt (assuming you trust its
             | construction). But you cannot write a _proof in ZF_ that
             | the machine cannot halt. Such a proof must include a new
             | axiom  "ZF is consistent", or some stronger axiom.
        
           | Diggsey wrote:
           | I think what's most unintuitive is that most (all?)
           | "paradoxes" or "unknowables" in mathematics involve
           | infinities. When limiting ourselves to finite whole numbers,
           | paradoxes necessarily disappear.
           | 
           | BB(748) is by definition a finite number, and it has some
           | value - we just don't know what it is. If an oracle told us
           | the number, and we ran TM_ZFC_INC that many steps we would
           | know for sure whether ZFC was consistent or not based on
           | whether it terminated.
           | 
           | The execution of the turing machine can be encoded in ZFC, so
           | it really is the _value_ of BB(748) that is the magic
           | ingredient. Somehow even knowledge of the _value_ of this
           | finite number is a more potent axiomatic system than any we
           | 've developed.
        
             | zmgsabst wrote:
             | You'd know the value in a more powerful system than ZFC (as
             | it includes such an oracle) -- but you can already reason
             | about ZFC in a more powerful system.
             | 
             | We already have more powerful systems, but what causes the
             | inability to self-reason is exactly that power: only first
             | order logic can prove its own consistency. Once you get
             | powerful enough to model arithmetic, you can build
             | statements with self-referential weirdness.
             | 
             | I don't see it as a paradox, but as growth: a sufficiently
             | rich system can pose questions which suggest a richer
             | system -- and thereby scaffold up the universe hierarchy.
        
             | raincole wrote:
             | BB(748) is a finite number, but I'd argue its magic also
             | comes from infinites: the fact some Turing Machines run
             | forever and never halt.
        
               | joelthelion wrote:
               | Is it? If it's not possible to prove that it's the best
               | solution to bb(748), does it even exist in any meaningful
               | way?
        
               | raincole wrote:
               | I'm not sure what you mean. First of all BB(n) is a
               | function so it has value(s).
               | 
               | And in theory we can prove BB(748)=X, where X is a plain
               | big natural number, as long as we just assume ZFC is
               | consistent. It's _practically_ impossible, but not
               | _fundamentally_ impossible like proving Con(ZFC) in ZFC
               | itself.
        
               | gpm wrote:
               | Proving BB(748)=X for some concrete X in ZFC is
               | _equivalent_ to proving Con(ZFC) in ZFC.
        
               | raincole wrote:
               | Yes, but I'm not "proving BB(748)=X in ZFC" in my
               | previous comment.
               | 
               | I clearly stated:
               | 
               | > as long as we assume ZFC is consistent
               | 
               | In other words, I'm talking about proving BB(748)=X in
               | ZFC+Con(ZFC), which is not fundamentally impossible. It's
               | practically impossible simply because you need to reason
               | out the sheer amount of TMs with 748 states.
        
               | gpm wrote:
               | Is there reason to believe that there's not a similarly
               | sized turing machine that halts iff Con(ZFC + Con(ZFC))
               | (which is independent of ZFC+Con(ZFC) by godel's)?
               | 
               | Certainly there's some sized machine that does that... it
               | seems to me that all you're doing is playing games with
               | adding axioms to maybe change the exact value of "748"...
               | and I don't even see that you've established that you've
               | successfully changed it.
        
               | raincole wrote:
               | Well, yes, my previous comment was sloppy. Of course it's
               | also possible that 748 is such a high upper limit that we
               | can add a lot of axioms to ZFC and BB(748) is still
               | independent to it. We just don't know it.
        
               | raincole wrote:
               | (Late Edit: the above comment was rather sloppy. I meant
               | that we _don 't know_ if it's impossible to prove
               | BB(748)=X in ZFC+Con(ZFC). It's not necessarily possible
               | either. We just haven't ruled out the possibility.)
        
             | waluigi wrote:
             | It's even more counterintuitive than you let on! If you are
             | working in ZFC along with the axiom "ZFC is consistent"
             | then there's no issue: just a normal number[1]. Where
             | things get _really_ strange is in ZFC plus the axiom "ZFC
             | is inconsistent".
             | 
             | This already sounds like an inconsistent theory, but
             | surprisingly isn't: Godel's second incompleteness theorem
             | directly gives us that Con(ZFC) is independent, so there
             | are models that validate both Con(ZFC) and ~Con(ZFC). The
             | models that validate ~Con(ZFC) are very confused about what
             | numbers are: from the models perspective, there is a number
             | corresponding to a Godel code for the supposed proof of
             | inconsistency, but from the external view this is a
             | "nonstandard number": it's not not a finite numeral!
             | 
             | Getting back to BB(748): what does this look like in a
             | model of ZFC + ~Con(ZFC)? We can prove that the machine
             | internal to the model will find that astronomically large
             | Godel code, so BB(748) will be a nonstandard number. In
             | other words, you can tell if a 748 state machine will
             | terminate in this model: you've just got to run it for a
             | number of steps that's larger than every finite numeral!
             | 
             | [1]: unless there's some machine that with 748 that
             | enumerates theorems of ZFC+Con(ZFC) but that's a different
             | discussion.
        
             | edanm wrote:
             | > BB(748) is by definition a finite number, and it has some
             | value - we just don't know what it is. If an oracle told us
             | the number, and we ran TM_ZFC_INC that many steps we would
             | know for sure whether ZFC was consistent or not based on
             | whether it terminated.
             | 
             | This doesn't sound right to me.
             | 
             | You _can_ prove that ZFC is consistent. You could do it
             | today, with or without the magic number, using a stronger
             | axiom system. If an Oracle told you that BB(748) = 100 or
             | whatever, that _would_ constitute proof that ZFC is
             | consistent.
             | 
             | But it wouldn't negate the fact that BB(748) is independent
             | of ZFC, because you haven't proved _within the axioms of
             | ZFC_ that ZFC is consistent, which is what makes it
             | independent.
             | 
             | > I think what's most unintuitive is that most (all?)
             | "paradoxes" or "unknowables" in mathematics involve
             | infinities. When limiting ourselves to finite whole
             | numbers, paradoxes necessarily disappear.
             | 
             | I might be missing something, but all of these assertions
             | deal with finite whole numbers, not infinity. Unless you
             | count a Turing machine running forever an infinity, in
             | which case, it seems counterintuitive to me that encoding a
             | while loop that runs forever somehow makes paradoxes
             | appear.
        
               | Diggsey wrote:
               | > This doesn't sound right to me.
               | 
               | Which bit?
               | 
               | > You can prove that ZFC is consistent. You could do it
               | today, with or without the magic number, using a stronger
               | axiom system.
               | 
               | Right but then just replace ZFC with that stronger system
               | and you're back where you started - the point is that
               | whatever the "strongest" system is that we've yet
               | considered, BB(N) for sufficiently large N is stronger
               | than that - and in all likelihood N can be much smaller
               | than 748 for all such systems we've yet conceived, since
               | we are not great at efficiently encoding things in turing
               | machines.
               | 
               | > If an Oracle told you that BB(748) = 100 or whatever,
               | that would constitute proof that ZFC is consistent.
               | 
               | The number alone is not the proof - you'd still need to
               | actually run the corresponding turing machine to finish
               | the proof.
               | 
               | > But it wouldn't negate the fact that BB(748) is
               | independent of ZFC, because you haven't proved within the
               | axioms of ZFC that ZFC is consistent, which is what makes
               | it independent.
               | 
               | Normally when we say some predicate P is independent of
               | some axiomatic system it means we could add a new axiom
               | to the system (P or !P) that would produce a new system
               | that is still consistent.
               | 
               | BB(N) being "independent of ZFC" is a very different
               | statement - it doesn't mean we are free to pick different
               | values of BB(N). It's easy to prove this:
               | 
               | 1. Let's say there are two possible values of BB(748) -
               | V1 and V2 such that V2 > V1 and both are consistent with
               | ZFC.
               | 
               | 2. Simulate every possible 748 state turing machine for
               | V2 steps.
               | 
               | 3. See if any one terminated after more than V1 steps.
               | 
               | 4. If they did, then V1 is inconsistent with ZFC -
               | contradiction. If they did not, then V2 is inconsistent
               | with ZFC - contradiction (since at least one turing
               | machine must terminate after exactly V2 steps).
               | 
               | This entire process takes finite time since there are
               | finitely many 748 state turing machines and V1 and V2 are
               | also finite.
               | 
               | So what does it even mean to say that BB(748) is
               | independent of ZFC? BB(N) is not even a predicate so it
               | definitely feels like a category error to say it's
               | independent.
               | 
               | We certainly can't prove that a candidate value is
               | correct within ZFC, but given any "overestimate" of
               | BB(748) we can prove that it's wrong:
               | 
               | 1. Let's say we have VC - an estimate of BB(748) that's
               | too large.
               | 
               | 2. Simulate every possible 748 state turing machine for
               | VC steps.
               | 
               | 3. If no turing machine terminated after exactly VC
               | steps, then VC is wrong.
        
               | panpog wrote:
               | There is only one integer k that we can actually write
               | down (given much more paper than could fit in the
               | universe) such that ZFC+ "BB(748)=k" is consistent.
               | However, given that same k, ZFC+ "BB(748)[?]k" is also
               | consistent. ZFC+ "BB(748)[?]k" has theorems that can be
               | thought of as it being wrong about what "finite" means.
        
           | woopsn wrote:
           | Does the fact that BB(k)=N is provable up to some k < 748
           | mean that all halting problems for machines with k states are
           | answered by a proof in ZFC?
        
           | edanm wrote:
           | > Thus, any proof that BB(748) = N must either show that
           | TM_ZF_INC halts within N steps or never halts. By Godel's
           | famous results, neither of those cases is possible if ZFC is
           | assumed to be consistent.
           | 
           | Isn't it more accurate to say that any proof that BB(748) = N
           | _in ZFC_ must either show that TM_ZF_INC halts within N
           | steps, or never halts?
           | 
           | Meaning, it's totally possible to prove that BB(748) = N, it
           | just can't be done within the axioms of ZFC?
        
         | LegionMammal978 wrote:
         | Let _X_ =  "1 if ZF is consistent, 0 otherwise". Then the
         | statements " _X_ = 0 " and " _X_ = 1 " are independent of ZF.
         | Whether the definition of _X_ is a satisfactory definition of a
         | particular number is a question of mathematical philosophy.
         | 
         | BB(748) is very similar, in that I'd call it a 'definition'
         | independent of ZF rather than a 'number' independent of ZF.
        
         | eapriv wrote:
         | It's not "an uncomputable number".
        
         | drdeca wrote:
         | No individual number is uncomputable. There's no pair of a
         | number and proof in ZFC that [that number] is the value of
         | BB(748). And, so, there's no program which ZFC proves to output
         | the value of BB(748). There is a program that outputs BB(748)
         | though, just like for any other number.
        
           | boothby wrote:
           | Individual numbers can be uncomputable! For example, take
           | your favorite enumeration of Turing machines, (T1, T2...) and
           | write down a real number in binary where the first bit is 0
           | if T1 halts and 1 otherwise, second bit is 0 if T2 halts...
           | clearly this number is real and between 0 and 1, but it
           | cannot be computed in finite time.
        
             | Vecr wrote:
             | If it had a finite size it would be computable.
        
             | drdeca wrote:
             | Pardon, I meant natural number. I should have specified.
        
             | Scarblac wrote:
             | That's a number in R, obviously most of them are
             | uncomputable (there is a countable number of Turing
             | machines).
             | 
             | But for every natural number n there is a trivial Turing
             | machine that just prints n and then halts.
        
           | cvoss wrote:
           | I think your mistake is your claim that BB(748) is a natural
           | number. For you to know that, you would necessarily have to
           | know an upper bound for the number of steps it takes for the
           | BB-748 machine (whichever machine it is) to halt. But you
           | definitely don't know that.
           | 
           | Related: It's incorrect to claim that each machine either
           | halts or doesn't halt. To know that that dichotomy holds
           | would require having a halting problem algorithm.
        
             | drdeca wrote:
             | I don't know it _in a constructive sense_ , sure.
             | 
             | It's still true though. I'm not wrong.
        
         | bo1024 wrote:
         | Many replies don't seem to understand Godel and independence
         | (and one that might is heavily downvoted). Cliff notes:
         | 
         | * ZFC is a set of axioms. A "model" is a structure that
         | respects the axioms.
         | 
         | * By Godel, we know that ZFC proves a statement if and only if
         | the statement is true in all models of ZFC.
         | 
         | * Therefore, the statement "BB(748) is independent of ZFC" is
         | the same as the statement "There are two different models of
         | ZFC where BB(748) are two different numbers.
         | 
         | * We can take one of these to be the "standard model"[1] that
         | we all think of when we picture a Turing Machine. However, the
         | other would be a strange "non-standard" model that includes
         | finite "natural numbers" that are not in the set {0,1,2,3,...}
         | and it includes Turing Machines that halt in "finite" time that
         | we would not say halt at all in the standard model.
         | 
         | * So BB(748) is indeed a number as far as the standard model is
         | concerned, the problem only comes from non-standard models.
         | 
         | TL;DR this is more about the fact that ZFC axioms allow weird
         | models of Turing Machines that don't match how we think Turing
         | Machines usually work.
         | 
         | [1] https://en.wikipedia.org/wiki/Non-
         | standard_model_of_arithmet...
        
           | bo1024 wrote:
           | I would edit my last line to say: weird models of numbers
           | that don't match how we think "halts in finite steps" usually
           | works.
        
         | red75prime wrote:
         | > It boggles my mind that a number (an uncomputable number,
         | granted) like BB(748) can be "independent of ZFC".
         | 
         | It's BB(n) that is incomputable (that is there's no algorithm
         | that outputs the value of BB(n) for arbitrary n).
         | 
         | BB(748) is computable. It's, by definition, a number of ones
         | written by some Turing machine with 748 states. That is this
         | machine computes BB(748).
         | 
         | > It feels like a category error or something.
         | 
         | The number itself is just a literally unimaginably large
         | number. Independence of ZFC comes in when we try to prove that
         | this number is the number we seek. And to do that you need
         | theory more powerful than ZFC to capture properties of a Turing
         | machine with 748 states.
        
         | LPisGood wrote:
         | BB(748) is a natural number, and _all_ natural numbers are
         | computable.
        
           | ted_dunning wrote:
           | There is definitely a function f such that f() = n for all n
           | [?] N.
           | 
           | But there is also a function g that you cannot prove whether
           | g() = n.
           | 
           | Important distinction.
           | 
           | This means that somebody could claim that the value of
           | BB(748) = n but you cannot be sure if they are correct (but
           | you might be able to show they are wrong).
        
         | throwaway81523 wrote:
         | The truth value of the continuum hypothesis is either 1 or 0
         | (at least from a platonistic perspective). But, it is proven to
         | be independent of ZFC. No huge numbers involved, just a single
         | bit whose value ZFC doesn't tell you.
        
       | sedatk wrote:
       | > Also, the left-superscript means tetration, or iterated
       | exponentiation: for example, 1510 means 10 to the 10 to the 10
       | and so on 15 times.
       | 
       | I thought it was a typo. First time I encounter tetration.
        
         | griffzhowl wrote:
         | Continuing the theme of iteration: it was the first time I
         | encountered pentation
        
           | tialaramex wrote:
           | One of the reasons I like the use of the number line in
           | schools is that on the line it's more obvious when you're
           | shown addition and multiplication and then later
           | exponeniation that this is a _pattern_. With the number line,
           | two natural questions arise and, hopefully by the time you
           | 're taught exponentiation the Math teacher knows enough math
           | to confidently affirm the answer to both. Yes, it keeps going
           | like this forever, that's called Hyperoperation. And yes, we
           | did (probably) skip one, it's known as Successor-of and you
           | were probably not explicitly shown this operator but it's the
           | near end of that infinite succession.
           | 
           | When arithmetic is introduced just as a way to, for example,
           | count money, it's more directly practical in the moment, but
           | you're not seeing the larger pattern.
        
             | Nevermark wrote:
             | Don't forget identity. Its range is small but important!
        
               | tialaramex wrote:
               | Fair!
        
         | lbourdages wrote:
         | I've seen it before, but it was using Knuth's up-arrow notation
         | [1], which I like because it generalizes easily.
         | 
         | [1] https://en.wikipedia.org/wiki/Knuth's_up-arrow_notation
        
       | NooneAtAll3 wrote:
       | If you want to learn about actual Busy Beaver results, I suggest
       | reading https://www.sligocki.com/ instead
       | 
       | Unlike Aaronson, he actually is on the forefront of Busy Beaver
       | research, and is one of the people behind the
       | https://bbchallenge.org website
        
         | moralestapia wrote:
         | >Unlike Aaronson, he actually is on the forefront of Busy
         | Beaver research [...]
         | 
         | Extremely bad _ad hominem_ , I enjoyed Aaronson's read, nothing
         | wrong with it.
        
           | lupire wrote:
           | That's not _ad hominem_ at all.
        
           | refulgentis wrote:
           | Gently, seconding peer: that is not ad hominem :)
           | 
           | Colloquially, I understand it's easy to think it means
           | "saying something about someone that could be interpreted
           | negatively" because that's the context it is read in it when
           | it is used.
           | 
           | The meaning is saying a logical argument is incorrect because
           | of who wrote the argument.
        
             | charcircuit wrote:
             | But the comment is not just saying something negative.
             | 
             | It is implying that claims from the article like "Then,
             | three days ago, Tristan wrote again to say that mxdys has
             | improved the bound again, to BB(6)>9_2_2_2" are not real
             | results. The justification for these not being real results
             | is solely based off whether author is actually on the
             | forefront of research.
        
               | refulgentis wrote:
               | I think you're touching on something important here.
               | 
               | OP isn't making a ad hominem fallacy in a logical
               | argument sense - it's not saying "Aaronson is wrong
               | because he's not a frontline researcher."
               | 
               | But you're absolutely right to feel uncomfortable with
               | their approach. There's something off-putting about
               | dismissing someone's reporting of research developments,
               | even if you prefer more comprehensive coverage, or
               | there's more interesting things to say.
               | 
               | The thing is, if that's ad hominem, so is _any
               | recommendation preferring one second-hand reporting over
               | another_ -- ex.  "if you want the _actual_ news, read
               | Tucker, not Krugman " isn't an ad hominem towards
               | Krugman.
               | 
               | Another example we see often on HN: saying "you should
               | read the actual paper instead of this pop science" is a
               | quite frequent, quite agreeable, and yet dull,
               | contribution on say, a Quanta article. Yet, I imagine we
               | agree this isn't an ad hominem.
               | 
               | The real issue might be that OP conflates two different
               | things: being a primary researcher versus being a good
               | science communicator who accurately reports on others'
               | work.
               | 
               | Both roles have value, and questioning whether someone
               | has filled one role doesn't necessarily invalidate their
               | ability to fill the other.
               | 
               | (this helped me understand my odd frustration with the
               | dull comments on science articles: I emotionally engage
               | with it as being mean / out of bounds, but its true, and
               | in reality, what I'm frustrated with is there could
               | always be a more detailed article, or even paper, but yet
               | we all must publish)
        
               | charcircuit wrote:
               | >ex. "if you want the actual news, read Tucker, not
               | Krugman" isn't an ad hominem towards Krugman.
               | 
               | But how you justify that could be one. If you are just
               | attacking the person instead of their reporting I would
               | call that ad hominem.
        
             | moralestapia wrote:
             | The wording implies that Aaronson does not know what he's
             | talking about.
             | 
             | >If you want to learn about _actual_ Busy Beaver results
             | [...]
             | 
             | This is saying there is no discussion of the results in the
             | article, which is not true.
             | 
             | >Unlike Aaronson, he actually is on the forefront of Busy
             | Beaver research [...]
             | 
             | This implies Aaronson has no (or lesser) authority on the
             | subject and suggests we should listen to somebody else who
             | purportedly has more.
             | 
             | Nowhere in @NooneAtAll3's comment is there an argument made
             | against/for the contents of the article, an example of that
             | would be:
             | 
             | "Aaronson mentions X but this is not correct because Y" or
             | something along those lines.
             | 
             | Instead, the comment, in it's full extent, is either
             | discrediting (perhaps unintentionally) and/or appealing to
             | the authority of people involved. That's _ad hominem_.
        
         | tedunangst wrote:
         | Can you elaborate on what's wrong with this post?
        
         | lupire wrote:
         | https://www.sligocki.com/ hasn't posted since April, and the
         | very first link on that blog is a link to... Scott Aaronson.
        
           | refulgentis wrote:
           | Could I bother you for some more info?
           | 
           | I spent 5 minutes trying to verify any link in the post above
           | links to Scott Aaronson, or mentions him, and found nothing.
           | :\ (both the siglocki, and when I found nothing there, the
           | busy beaver site)
        
             | alexeldeib wrote:
             | The "first" link (after the home button) on bbchallenge is
             | the header bar link to https://bbchallenge.org/story which
             | cites Aaronson in the first sentence (double first!). I
             | would not describe it like OP for someone trying to find
             | the actual link ;)
             | 
             | "One Collatz Coincidence", the 2nd story on the blog, also
             | mentions Aaronson
        
         | renewiltord wrote:
         | I don't get it. What's wrong with the post? And
         | https://arxiv.org/abs/1605.04343 is interesting, no?
        
         | dloranc wrote:
         | Maybe Scott isn't at the forefront of the research by some
         | standards, but I still consider him a prominent figure in the
         | field. Independence of ZFC, Busy Baver Frontier paper, "Who Can
         | Name the Bigger Number?" essay. He did a lot to popularise the
         | topic and posed some interesting ideas or conjectures (Beeping
         | Busy Beavers for example).
        
       | charcircuit wrote:
       | >imagine you had 10,000,000_10 grains of sand. Then you could ...
       | well, uh ... you could fill about 10,000,000_10 copies of the
       | observable universe with that sand. I hope that helps people
       | visualize it!
       | 
       | People can't visualize numbers that big. There's more ways to
       | express numbers than just counting them. For example a single
       | grain of sand has infinite states it can be in (there are an
       | infinite amount of real numbers), so you could say a single grain
       | of sand could represent BB(6). Combinations can grow
       | exponentially, so that may be something useful to try and express
       | it.
        
         | Xcelerate wrote:
         | At some point big numbers become much more about the
         | consistency strength of formal systems than "large quantities".
         | 
         | I.e., how well can a system fake being inconsistent before that
         | fact it discovered? An inconsistent system faking consistency
         | via BB(3) will be "found out" much quicker than a system faking
         | consistency via BB(6). (What I mean by faking consistency is
         | claiming that all programs that run longer than BB(n) steps for
         | some n never halt.)
        
         | unsnap_biceps wrote:
         | I'm confused about this example, isn't the count of grains of
         | sand equal to the count of observable universes so it'd be a
         | single grain of sand per universe?
        
           | heftig wrote:
           | The "about" does a lot of heavy lifting in this example.
           | Dividing 10,000,000_10 by the number of grains that fit into
           | one universe doesn't change it much. The 10,000,000 would get
           | smaller somewhere in the deep depths of the decimal fraction.
        
         | Dylan16807 wrote:
         | If the universe rounds to the nearest Planck unit, then a grain
         | of sand suddenly has not all that many states.
         | 
         | Using infinite precision to make things seem tractable is
         | sleight of hand in my book. Stick with integers when you're
         | describing scale.
        
       | MichaelDickens wrote:
       | It's known that BB(14) is bigger than Graham's number, but this
       | new finding leads me to believe that BB(7) is probably bigger
       | than Graham's number. Intuitively, the technology required to go
       | from pentation to Graham's number feels simpler than the
       | technology required to go from `47,176,870` to `2 <pentate> 5`.
        
         | tromp wrote:
         | Thanks for sharing; your post would fit well as an answer to
         | mine about Graham's number...
        
       | phs wrote:
       | So what is the richest logic whose proofs can be enumerated with
       | only a five state TM?
        
         | tromp wrote:
         | That entirely depends on how you want to interpret a finite
         | binary string as an enumeration of logic proofs?!
        
         | LegionMammal978 wrote:
         | While that question depends on what you count as an
         | 'enumeration', there's the related question of "What's the
         | richest logic that cannot prove the halting status of all
         | 5-state TMs?" That is, what's the richest logic that some
         | 5-state TM's halting status is independent of?
         | 
         | I've pondered that version of the question a bit, but I
         | couldn't get very far due to my lack of expertise in first-
         | order logic. What I do know is that Skelet #17 [0] is one of
         | the toughest machines to prove non-halting on a mathematical
         | level [1], so any theory sufficient to prove that Skelet #17
         | doesn't halt is likely sufficient to decide the rest of the
         | 5-state machines.
         | 
         | [0] https://bbchallenge.org/1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA
         | 
         | [1] https://arxiv.org/abs/2407.02426
        
       | tromp wrote:
       | People on the bbchallenge Discord server are keen to speculate on
       | how many Turing Machine states are needed to surpass Graham's
       | Number, which is vastly larger than the 2^^2^^2^^9 achieved by
       | the latest BB(6) champion.
       | 
       | We know from the functional busy beaver [1] that Graham behaviour
       | can come surprisingly early; a 49-bit lambda term suffices. There
       | are only 77519927606 closed lambda terms of at most that size
       | [2], compared to 4^12*23836540=399910780272640 unique 6-state
       | Turing Machines [3].
       | 
       | With the achievement of pentation in only 6 states, several
       | people now believe that 7 states should suffice to surpass
       | Graham's. I would still find that rather surprising. A few days
       | ago, I made a large bet with one of them on whether we would see
       | proof of BB(7)>Graham's within the next 10 years.
       | 
       | What do people here think?
       | 
       | [1] https://oeis.org/A333479
       | 
       | [2] https://oeis.org/A114852
       | 
       | [3] https://oeis.org/A107668
        
         | gpm wrote:
         | I can't pretend to be an expert, but I'll argue BB(7) is
         | probably larger than Graham's number.
         | 
         | BB has to grow faster than any computable sequence. What
         | exactly that means concretely for BB(7) is... nothing other
         | than handwaving... but it sort of means it needs to walk up the
         | "operator strength" ladder very quickly... it eventually needs
         | to grow faster than any computable operator we define
         | (including, for example, up-arrow^n, and up-arrow^f(n) for any
         | computable f).
         | 
         | My gut feeling is that the growth between 47 million and
         | 2^^2^^2^^9 is qualitatively larger than the growth between
         | 2^^2^^2^^9 and graham's number in terms of how strong the
         | operator we need is (with gramah's number being g_64 and g here
         | being roughly one step "above" up_arrow^n). So probably we
         | should have BB(7)>Graham's number.
        
           | pinkmuffinere wrote:
           | Apologies if this feels adversarial, but I think your
           | informal proof has an error, and I think I can explain it!
           | 
           | Your proof rests primarily on this assertion:
           | 
           | > BB has to grow faster than any computable sequence.
           | 
           | This is almost true! BB(n) has to grow faster than any
           | computable sequence _defined by an n-state Turing machine_.
           | That last part is really important. (Note that my restatement
           | is probably incorrect too, it is just correct enough to point
           | out the important flaw I saw in your statement). This means
           | that up-arrow^f(n) _can_ be larger than BB(n) -- up-
           | arrow^f(n) is not restricted by a Turing machine at all. As
           | an easy example, consider f(n) = BB(n)^2.
           | 
           | You may still be right about BB(7) being bigger than Graham's
           | number, even if your proof is not bulletproof
        
             | adgjlsfhk1 wrote:
             | one of the things that does come out of BB is that
             | BB(n)^2>>BB(n+c) for some very small constant c (I would be
             | surprised if c>2)
        
               | pinkmuffinere wrote:
               | Sure, but the example I'm providing is just meant to
               | illustrate that BB(n) is not greater than arbitrary f(n).
               | I'm not trying to provide the biggest number, I'm trying
               | to illustrate that the sketched-out proof is incorrect.
               | If you want me to provide a bigger number, I suppose
               | another easy example is to define f(n) = BB(BB(n)).
               | 
               | Edit: Oh sorry, I see I misread the direction of your
               | greater than signs. Leaving comments as-is though,
               | hopefully that results in the least confusion
        
               | adgjlsfhk1 wrote:
               | oops, my greater than signs are in the wrong direction.
               | specifically, for any computable function f, there exists
               | some constant c such that f(BB(n))<<BB(n+c)
        
             | gpm wrote:
             | Math's a cooperative endeavor, I want to know if I'm wrong!
             | 
             | I'm not sure I understand the distinction you're trying to
             | make though, and I'm not sure it's right...
             | 
             | The argument that BB has to grow faster than any computable
             | sequence is that if we have a computable f(n) where for all
             | n f(n) > BB(n) then we can solve the halting problem by
             | simulating turing machines of size n for f(n) steps and
             | checking if they halt. Even if we can't prove f(n) > BB(n)
             | the mere existence of this f would mean we could solve the
             | halting problem (even though we couldn't prove we had done
             | so).
             | 
             | I agree my "proof" (intuition really) rests on that
             | assertion.
             | 
             | > As an easy example, consider f(n) = BB(n)^2.
             | 
             | This, like BB(n), isn't computable?
        
               | pinkmuffinere wrote:
               | Thanks for the good attitude!
               | 
               | Ah, I didn't realize 'computable' had a specific meaning
               | in this domain -- showing the limits of my experience a
               | bit. After looking at the wikipedia page and rereading
               | your sketch, I think it is true that
               | 
               | > it eventually needs to grow faster than any computable
               | operator we define
               | 
               | I'm not sure if this has implications about how quickly
               | BB() grows compared to the "operator strength" ladder
               | though? It's familiar/convenient to refer to tetration,
               | pentation, etc as f() for convenience, but this is just
               | notational -- not related to computability. When
               | comparing BB(n) and tetration(n), pentation(n), etc(n), I
               | don't think there is really anything that can be said
               | 'easily' about which values are larger. BB(n) will be
               | larger than anything that can be computed in n steps. But
               | pentation(n) is not necessarily computable in n steps, it
               | may take much more. We may find pentation(n) > BB(n) for
               | all n greater than some threshold. I might be
               | misunderstanding a logical step here though that connects
               | them?
        
               | throwaway81523 wrote:
               | > We may find pentation(n) > BB(n) for all n greater than
               | some threshold.
               | 
               | No, that is impossible. Tetration, pentation, etc. are
               | all computable sequences and BB grows faster than any
               | computable sequence. So you have the > sign where you
               | really want a < sign.
        
               | meindnoch wrote:
               | >BB(n) will be larger than anything that can be computed
               | in n steps
               | 
               | Who said anything about "n steps"?
               | 
               | BB(n) is about an n-state Turing machine, not "n steps".
        
             | btilly wrote:
             | No, the original was correct.
             | 
             | Any computable sequence S(n) must be computed by a specific
             | finite program of fixed length.
             | 
             | Once n gets big enough, BB(n) will include the function
             | S(2^n), and therefore will exceed that computable sequence.
             | 
             | Given computable sequences may exceed BB(n) for a finite
             | number of terms. But eventually BB(n) will outgrow them,
             | and will never look back.
        
               | pinkmuffinere wrote:
               | Just replying to say you're right! Thanks!
        
           | pinkmuffinere wrote:
           | I can't edit my original comment anymore, but replying to say
           | I went on a Wikipedia binge and I think you're right. Thanks
           | for humoring me and helping me learn!
        
             | gpm wrote:
             | :)
        
       | d_silin wrote:
       | Any time I see such results from computation complexity theory, I
       | realize that any current zeitgeist of "super-intelligent AI are
       | gods" is complete bullshit.
       | 
       | You can convert every atom of observable Universe into a
       | substrate for supercomputer, you can harness energies of
       | supermassive black holes to power it, but running a humble BB(6)
       | to halting state would be forever out of its reach.
        
         | istjohn wrote:
         | That strawman never stood a chance.
        
       | ryandrake wrote:
       | > For those tuning in from home, here BB(6) is the 6th Busy
       | Beaver number, i.e. the maximum number of steps that a 6-state
       | Turing machine with a {0,1} alphanet can take before halting,
       | when run on an initially all-0 input tape.
       | 
       | Oh! Of course! That sure clears things up for this non-expert.
       | This is clearly a hardcore blog for people who have been doing
       | this kind of research for decades. Kind of awesome to stumble
       | upon something so unapologetically dense and jargony and written
       | for a very specific audience!
        
         | clbrmbr wrote:
         | The definition there is standard undergraduate computer science
         | theory. Maybe not standard for software engineering though.
        
         | Bjartr wrote:
         | That should be enough for someone with an undergrad CS
         | education to at least get a sense of what's going on if they
         | haven't encountered the busy beaver problem before.
         | 
         | Is it niche jargon, absolutely, but to say it's only accessible
         | to people who have put in decades is selling yourself short.
        
           | ryandrake wrote:
           | Hmm, interesting. It's been 30 years since my engineering
           | degree (not CS) and I'd have to look up what a Turing machine
           | is. I think I remember one professor briefly mentioned it as
           | "This is something the CS majors care deeply about but nobody
           | else in the industry does." Where I was, the CS degree was
           | essentially a math degree dressed up in a hoodie.
        
             | Bjartr wrote:
             | > This is something the CS majors care deeply about but
             | nobody else in the industry does
             | 
             | Correct, the industry cares a lot more about Software
             | Engineering than Computer Science.
             | 
             | > CS degree was essentially a math degree dressed up in a
             | hoodie.
             | 
             | To a first approximation, that's what it's supposed to be.
             | CS is a field of mathematics. It's not a trade school
             | course.
        
       | vismit2000 wrote:
       | Scott Aaronson | How Much Math Is Knowable? [Harward CMSA]:
       | https://www.youtube.com/watch?v=VplMHWSZf5c
       | 
       | Recently on HN (couple of months ago):
       | https://news.ycombinator.com/item?id=43776477
        
       ___________________________________________________________________
       (page generated 2025-06-29 23:01 UTC)