Comment by Scarblac

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.

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.

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

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.

748 is not tight. As given in the article, k=643 is independent of ZFC, and the author speculates that it's possible that something as small as BB(9) could be as well.

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.

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.

If we assume ZFC to be consistent, then Gödel'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.

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.

Right, Hilbert’s goal was (loosely speaking) to “find a finitely describable formal system” sufficient to “capture all truths”. When Gödel 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 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).

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

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?

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

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.

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.

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

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

Nobody can give you that number, because it's way bigger than what can be represented in the universe.

Looking at [3], they seem to argue that the system isn’t complete for the usual Gödel 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_{ℱ_{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.

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.

Pardon, I meant natural number. I should have specified.

If it had a finite size it would be computable.

I don’t know it in a constructive sense, sure.

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

You say the busy beaver function is a function. But I can claim it's not, because you cannot make it constructively- in constructive analysis, all functions are 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.

This integer only exists if you assume classical logic. Otherwise, there is no such integer a priori, and actually there is none in general.

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

Yes, I would say that neither is really a number in the traditional sense of the word, nor in constructive analysis.

Only if you believe that a number you can't count is a number. You can believe that, but it's a leap.