> it is always possible to compute BB(k) for a specific and arbitrary k

How do you do that once k is large enough that it admits Turing machines whose halting behavior is independent of our axioms?

BB(k) for a specific k is just a number. Ao just write it to the output. Proofing correctness is different from „computing“ and not required here.

> BB(k) for a specific k is just a number.

That's not as obvious as you might think. The value of BB(800) is independent of ZFC. So it isn't "just a number" if you're working in ZFC.

Hmm... As ZFC specifically cannot identify that number as special (at least as relates to the Busy Beaver function), maybe it is quite specifically "just a number"!

Ah, so pointing out that the number itself, being an integer, is computable even though the function isn't. Makes sense.

Perhaps you need larger and larger sets of axioms as k increases.

This is fascinating to me, because Turing machines can in principle be manifested as physical objects. It feels like you shouldn’t need axioms if you have the thing sitting in front of you, but on the other hand how else are you supposed to prove something doesn’t halt?

Still, if you have two axiomatic systems that disagree, what does that mean? Surely you can just run the machine in question for a certain number of steps to determine which system is right.

Ah, the issue is that one system may be able to prove the correct answer but it remains independent for the other system.

> it is always possible to compute BB(k) for a specific and arbitrary k

but wouldn't this be equivalent to solve the Halting Problem?

No, because the halting problem requires implementing a function that can compute whether any other function halts. It has to work for any possible function you give it. You can, of course, compute whether some functions halt. Two easy ways to do so are to observe that it halts or observe an infinite loop.

Isn’t the crux of the issue that you can’t “observe” an infinite loop?

No, the crux of the issue is that you can't observe every infinite loop.

But if you know BB(n) for any n then you can just make run a program of length n for BB(n) steps. If after BB(n) steps it hasn't halted you know that the program will loop forever. Since you can do that for any arbitrary program then you could solve the halting problem.

If you recall from predicate logic, these two statements are not the same:

1) For all Turing Machines A, there exists a Turing Machine M such M can compute whether A halts.

2) There exists a Turing Machine M such that for all Turing Machines A, M can compute whether A halts.

Statement 1 is true, statement 2 is false.

You can apply a similar reasoning to BB(n) or your notion of Omega. For any particular choice of n, there is an algorithm that can compute BB(n) and similarly for any arbitrary precision p, there is an algorithm that can compute Omega up to that precision.

None of this is to be taken that there exists an algorithm that can compute BB(n) for all n, or that there exists an algorithm that can compute Omega up to precision p for all p.

But imagine that we could compute BB(n) for any n, even if we need to use a different algorithm for each n. Then, we could build the mapping n -> BB(n). But the existence of this mapping is forbidden by the unsolvability of the Halting Problem, isn't it?

> But imagine that we could compute BB(n) for any n, even if we need to use a different algorithm for each n.

This is itself uncomputable; therefore

> Then, we could build the mapping n -> BB(n).

This mapping is not computable.

Edit as I'm rate-limited:

What I mean is, informally, the incomputability of the algorithm to select the correct algorithm to compute BB(n) is sufficient to make that mapping uncomputable.

However, that does not mean that an algorithm to compute BB(n) for a specific n does not exist. (Trivially, it does; "output BB(n)".)

yes, this is why I said

> the existence of this mapping is forbidden

:)

No you can't conclude this and in fact the more general principle is that being able to prove P(0), P(1), P(2), etc... does not mean that it's also possible to prove P(n) for all n. The property of a formal system for which this does follow is known as Omega completeness, but Peano arithmetic and ZFC more broadly are both Omega-incomplete systems, hence there are propositions for which P(0), P(1), P(2)... can all individually be proven and yet it is not possible to prove P(n) for all n.

Wikipedia touches on this subject with an article on omega-consistent systems, which is a very closely related property:

https://en.wikipedia.org/wiki/%CE%A9-consistent_theory

And this gives a very brief description of Omega completeness:

https://encyclopediaofmath.org/wiki/Omega-completeness

> it is always possible to compute BB(k) for a specific and arbitrary k. This is a very subtle detail.

That's not subtle at all. Any finite number or string can be computed by a program consisting of a single very long print statement.

Fair enough, one misconception I always hear from people learning about Godel's incompleteness theorem or the halting problem is that it means there exist algorithms where we can never know if it halts or not. Like there's some limit to math that makes it impossible for us to know whether a particular algorithm just keeps running forever or will eventually stop.

No such algorithm exists, no such example exists because for any particular algorithm it's always possible to determine whether it halts or not (at least in principle). It might not be practical, the proof might be incredibly difficult, but math does not have any kind of intrinsic limitation that prevents us from proving whether a specific algorithm halts.

Nice observation. Unless you’re missing something that seems to kind of shoot down the main point.

The post and it’s analysis are still interesting, but it should probably be updated else a lot of people might take away this key point into their memory as they think about computability.

No, you cannot compute BB(k) for a given k. https://scottaaronson.blog/?p=2725

I love that article but that does not state what you are claiming it does. What that states is that there exists a k (whose upper bound is 8000) whose solution is independent of ZFC. That does not mean it can't be computed.

In the very comment section of that blog post someone brings this issue up, and Scott himself says:

"Yes, fine, you’re right, there’s not a single “boundary between the knowable and the knowable.” What there is, is more like a concentric series of boundaries, with signs warning you that as you proceed outward you need to take on bolder and bolder axioms (which might be large-cardinal axioms and might be something else). What’s significant about going beyond ZFC is just that, by that point, you’ve clearly passed the first of those boundaries."

Suppose BB(8000) could be computed: 1) Compute BB(8000). 2) Run the program specified in the article until it either halts or it runs for BB(8000)+1 steps. 3) We then know if the program ever halts, and then have a proof within ZFC whether or not ZFC is sound.

No, what you will have is a proof that ZFC is sound but that proof will not be within ZFC. That proof will rely on additional axioms that are extensions to ZFC.

Well, OK, I suppose you could add something like 'BB(8000) is 6,' but once you go beyond ZFC, you're going beyond anything required for computation as we know it.

No this is also wrong. You would not be able to add an axiom like 'BB(8000) is 6' or just any arbitrary value without introducing an inconsistency. The reason for the independence of BB(8000) from ZFC is precisely because there is some non-standard model of arithmetic for which a Turing Machine halts in that non-standard model but does not halt in the standard model.

The only axioms you could introduce to ZFC that would not introduce an inconsistency would be one that eliminates that non-standard model of arithmetic without also eliminating the standard model of arithmetic.

https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

None of this requires going beyond any kind of notion of computation and any value that is computed for one such extension would necessarily have to be the same value among all consistent extensions of ZFC. It's not like you could have one extension of ZFC where BB(8000) is X and another extension where BB(8000) is Y without one of those extensions being inconsistent.

There are plenty of extensions to ZFC that add new axioms for the sake of exploring niche mathematical ideas. ZFC is nice in that it's easily motivated and can serve as a well understood foundation whose proofs can be stated without reference to additional hypotheses. It also satisfies an unbelievably broad set of mathematics, but mathematicians studying set theory often extend ZFC with additional axioms such as large cardinal axioms, Neumann/Bernays/Godel (NBG) set theory is another common extension, Kelley Morse (KM) set theory. The latter two extensions are even able to prove the consistency of ZFC. As I referenced in Scott's quote, BB(8000) is almost certainly computable by adopting one of the large cardinal axioms.

> it is always possible to compute BB(k) for a specific and arbitrary k

This is not true.

There is a number N where BB(n) is incomputable for all n > N. This fact tie back to being able to solve the Halting Problem, in various clever ways if you knew BB(n).

The value of BB(744) depends on whether the Riemann Hypothesis is true or false. This means that it cannot be computed in general. The Riemann Hypothesis being either true or false are both consistent with ZFC. The value of BB(748) depends on the self-consistency of ZFC.

> it is always possible to compute BB(k) for a specific and arbitrary k.

It is not. There are a few proofs, most notably the fact that you'd have to solve the halting problem to find BB(k) for an arbitrary k. But the more interesting proof is when looking at the growth of the number of states required for larger BB(k)'s. You end up with a pretty cool contradiction[1] by constructing a very special Turing machine.

[1] http://www.coopersnotes.net/docs/langmach/CHAP10%20Busy%20Be... (pg. 403)

I feel like even after I point out the subtlety, people just read right past it and still don't recognize it.

Nothing in your source contradicts anything I've said.

> Don't think this article is correct when it says that Omega can't be computed to arbitrary precision, it certainly can be.

It's not computable in this sense: there's no algorithm that given n returns Omega with n bits of precision, for any n. I think this qualifies as saying it cannot be computed to arbitrary precision :)

But I understand your point -- the language here is tricky.

Trying to make things clearer: Every program that does halt can be proven to halt -- simply run the program until it halts, if we assume it halts then you get its proof for free. However, if we make no assumptions a program may run forever, so we cannot know if it halts. I believe Godel's theorems also imply there must be non-halting programs for which no proof that they do not halt exists. This closes a very interesting loophole: you might, instead of just trying to run every program until it halts, to check every proof to see if it is a valid proof that a given program P does not -- if it exists, you will always find it. But because sometimes P does not halt yet no proof exists, this loophole is closed.

As others have mentioned, indeed I believe 'different algorithm for q > k, but such an algorithm does exist' does not pan out in the sense that we could prove the correctness of such algorithms, even though they do exist! :)

Another interesting angle: you can think that, even if you had an "oracle" that gives the "true" halting value (halts or does not halt), the size of a program that decides (by encoding the oracle values somehow) all halting programs up to n must grow with n. In other words, the halting values are incompressible somehow; if it were the case that the growth was bounded, then there would exist some program P that returns the true halting value of any program (false by Turing). This leads to the notion that non-computable numbers are random (or random-like), because they are fundamentally incompressible in a certain way (and you can't, on average, compress a random string).

Edit: minor corrections

This makes me consider a second loophole: even with, for a given set of axioms, we cannot prove some given P does not halt (Godel's incompleteness theorems). However, that makes us wonder if there can be a procedure that suggests stronger, but still minimal axioms (consistent with say Peano arithmetic or ZFC) and proves them in this new axiomatic basis?

(1) Would this proof be considered acceptable? (or can we devise a system that guarantees found proofs to be acceptable)

(2) Is this procedure feasible?

If anyone has literature on this topic, this is interesting! (an optimistic alternative to incompleteness)