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.

"One Collatz Coincidence", the 2nd story on the blog, also mentions Aaronson

The 748/745/643 numbers are just examples of actual machines people have written, using that many states, that halt iff a proof of "false" is found.

At any rate, given the precise k, I believe your intuition is correct. I've heard this called 'proof by simulation' -- if you know a bound on BB(N), you can run a machine for that many steps and then you know if it will run forever. But this property is exactly the intuition for why it grows so fast, and why we will likely never definitively know anything beyond BB(5). BB(6) seems like it might be equivalent to the Collatz conjecture, for example.

It’s still true though. I’m not wrong.

But for every natural number n there is a trivial Turing machine that just prints n and then halts.

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.

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

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

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.

In fact, both Gödel and Turing worked on this problem quite a bit. Gödel 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 ε_0 of ‘Q_{n+1} = Q_n + Q_n is consistent’ where Q_0 is Robinson arithmetic).

https://jdh.hamkins.org/the-universal-algorithm-a-new-simple...

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_{ℱ_{QG}} , determined by the axioms of ℱ_{QG} , such that no statement S with Kolmogorov complexity K(S) > K_{ℱ_{QG}} can be proven within ℱ_{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.

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.

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

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.

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.

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.

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.

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?

Many other numbers and functions are computable, including e, pi, 10^100, etc- these are fundamentally different than BB.

So in what sense is it actually a number? There is no algorithm which can resolve questions such as BB(748) < x given x. That doesn't seem like a number to me!

In fact, for some x, such questions will depend on the consistency of ZFC. All normal math we do is expressible in ZFC, but by incompleteness, ZFC cannot prove it's own consistency or is inconsistent. So, we cannot really ever know the value, we can only ever find lower bounds. Does this seem like a number to you? It's not in the English sense and neither is it in what I would consider a reasonable definition of numbers you actually encounter, the computable numbers. Real numbers are in fact, not very real at all.

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.

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

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

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

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.

The issue is that there is no way within ZFC to determine which value is the smallest.

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 Gödel-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 Gödel numbering.

> 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 Gödel's theorem is easy to prove if you have results about the halting problem. Your first one says that in order to prove Gödel's theorem, you need to establish results about the halting problem.

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.

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.

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?

From within those models Q satisfies all the properties of being a natural number but it's not actually a natural number. Q is some successor of 0, you can add 1 to Q to get another distinct mathematical object, there is some predecessor to Q called P so that P + 1 = Q, etc etc... Q satisfies all the properties within ZFC of being a natural number but it isn't an actual natural number.

Furthermore if ZFC is consistent then it's impossible for any model of ZFC to have BB(4) = 100. ZFC is sufficiently powerful to prove that BB(4) != 100, it is not sufficiently powerful enough to prove that BB(748) = F for some actual natural number F.

What it means specifically? ZFC+~(BB(748)=N) allows to extend definition of the Turing machine to a non-standard number of steps?

Can "BB(748) is undefined" be a provable theorem in ZFC+~(BB(748)=N) instead?

While we know that ZFC+~(BB(748)=N) is consistent, we don't know whether \exist Q!=N where ZFC+(BB(748)=Q) is consistent.

Intuitively I see it as: by adding axiom ~(BB(748)=N), we codify that this formal system isn't powerful enough to describe a Turing machine with 748 states (and probably all the machines with number of states greater than 748).

How could such a definition give rise to such a set with Q in it?

What second order logic does let you do is deal with only one single model, called the categorical model. So instead of having a theory that has a whole bunch of different models including the actual natural numbers along with undesirable models that contain infinitely large values... you can force your theory to have one single model, no more "It's true in this model, but it's false in that other nonstandard model that's getting in the way." So yes in a particular theory of second order logic BB(748) has one single value because there is only one single model.

So problem solved right? Not even close... because that one single categorical model being used to represent the natural numbers may not be the actual natural numbers, the intended natural numbers where every number is actually finite. Having one single categorical model does not imply working with the actual model you intended to work with. Depending on your choice of second order theory you may be operating within a theory where the single categorical model is indeed unbeknownst to you {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} and hence BB(748) is equal to Q and you'll have no way of knowing this before hand since you lack an effective proof system.