[Aeium]

So, one thing that we know from Godel is that there are true statements that cannot be proven.

What if a similar proof is made for a Beaver? That a specific beaver is constructed such that

1: It probably never halts 2: Proving that it never halts is a paradox

Something like that. If assignment of BB number for BB of that size depends on that proof, then the BB value doesn't exist.

And what else would it depend on? How could a smaller number be selected when larger potential numbers cannot be ruled out?

[umanwizard]

> What if a similar proof is made for a Beaver?

Then we will never be able to find the Nth beaver number for the corresponding N.

That doesn’t mean it is undefined or uncomputable. It actually has nothing to do with it. There is a computer program that prints out the number of hairs on my head. Doesn’t matter that you will never know how to write that program.

Again, uncomputable is being used in a technical sense here which is why I asked you what definition of “computable” you’re using.

[Aeium]

> Then we will never be able to find the Nth beaver number for the corresponding N.

This is pretty clearly what people are asking about when asking if BB(6) is "uncomputable" then.

I understand (now) the point about the specific meaning of the term of art "uncomputable". If you want to speak precisely on the topic, it's not the right question to ask.

But it still seems like the question, "will we ever be able to find out the Nth beaver number", is the more interesting question.

So, we can define ZFC axioms that classify the beavers we can know together with the beavers we cannot know. So what? Then that is just skipping the interesting question. Maybe that just means for this specific problem that is not the best construction to decide to use to classify them?

I would be more interested in a classification that would assign one label to beavers we could possibly hope to calculate, and another for beavers where the calculation is impossible.

[elijaht]

“Probably doesn’t halt” is ill defined, it either halts or it doesn’t. In either case, computability of that number is completely separate from whether we can prove that number is BB(N) or decide whether a given beaver halts. Additionally, the way the busy beaver function is defined ensures it has a defined integer output. Computability is just our ability to construct a machine which would print out that number. We can clearly do that for any integer