They exist in that it is easy to prove "for ALL x there EXISTS y such that (there EXISTS a Turing machine with at most x states M such that (there EXISTS some n such that M prints y 1's and halts after n steps) AND (for ALL Turing machines with at most x states M, if (there EXISTS some n such that M halts after n steps) then (M prints no more than y 1's after n steps))". I expect you can prove this in systems as weak as Primitive Recursive Arithemetic.

It is true though that various (decidable) proof systems are unable to prove that the Busy Beaver function has any specific value beyond a certain point. However, where that cut-off is varies from proof system to proof system, with stronger proof systems being able to prove more an more values of the Busy Beaver function.

Maybe you find it weird that we can prove (Exists x. P x) without being able to prove P n for any particular numeral n? Welcome to the strange world of classical (i.e. non-constructive) mathematics.

> It is true though that various (decidable) proof systems are unable to prove that the Busy Beaver function has any specific value beyond a certain point.

Isn't the result stronger than that though? The value of BB(30) might be X. Or it might be Y. Neither value would cause any problems.

Thus, "the value" doesn't exist. There is no value that is the value of BB(30).

Yes, what you are saying is indeed the case in the sense that if BB(30)=n for some particular numeral n is independent of whatever proof system we are focusing on, for the sake of argument let's say ZFC, (though 30 feels a a bit on the low side for ZFC), then we can consistently add BB(30)=n or BB(30)≠n as axioms to the system, the same way to can for any other independent statement. And there will be arbitrary large values of n that are independent, so we could add BB(30)=n or we could add BB(30)=m or so forth for any numerals i so long as BB(30)=i is independent of ZFC (or whatever axiom system we are considering).

But! that does not mean that all these systems are sound, for if you add the incorrect value as an axiom, specifically if you add anything but the smallest value 'm' such that BB(30)=m is independent of ZFC, then you are in a similar situation to adding ¬Con(ZFC) whereby you only have non-standard models.

They way this works is that, suppose BB(30)=m for some particular m is independent of ZFC, but BB(30) is not actually equal to m. What we will find is that there is some Turing machine M and some non-standard natural number q such that, while M doesn't actually halt in reality, according to some non-standard model it does halt in 'q' number of steps, and, in this model, when it does halt, it leaves 'm' 1's on the output tape.

That said, your comment did push me towards the limits of my comfort zone, so it might be helpful to double check what I'm saying. I don't see how it could be any other way though.

To elaborate a little further on why BB(30) does have a true value.

If BB(30) truly equals some particular numeral m, then there actually does exist a Turing machine M that has no more than 30 states and does halt with m 1's on its tape. Not only does this machine really exist, but the fact that it halts in this state is true Delta_0 statement, and thus it is trivially provable, you don't even need induction. It is provable in Robinson Arithmetic, it is provable in Peano Arithmetic, and it is provable in ZFC. Thus we have that RA proves "BB(30) ≥ m" and PA proves "BB(30) ≥ m" and ZFC proves "BB(30) ≥ m", etc.

By transitivity each of these systems also proves "BB(30) ≥ m₀" for every numeral m₀ less than m. But if m₁ is a numeral larger than m, it is no longer the case that RA proves "BB(30) ≥ m₁" and PA doesn't prove "BB(30) ≥ m₁" and (assuming ZFC is sound) ZFC doesn't prove "BB(30) ≥ m₁"

Thus we "can tell" what the true value of BB(30) is because it is the greatest value in which RA (or PA or (presumably) ZFC) proves "BB(30) ≥ m" for the numeral m denoting that value. Equivalently the value of BB(30) is the least value m for which RA, PA, or any other sound system, does not prove "BB(30) ≠ m".

We "can tell" this value even if we might not be able prove it in PA, or ZFC, or "ZFC + there exists a Mahlo cardinal". Indeed each different proof system likely can extend the range of BB values that are provable.

If you add an axiom "BB(30) = m" for some particular numeral m as an axiom to ZFC and it is the wrong value of m, you will either get an inconsistent system if "m" is too small, or you will get an unsound system if "m" is too large. In case "m" is to large, the unsound system will wrongly prove that certain Turing machines halt that do not actually halt. Specifically it will falsely prove that the Turing machine that searches for (a Turing machine with no more than 30 states that halts with "m" 1's on it tape) will halt, when such a machine does not actually halt.

Yes they are independent of ZFC but they still exist. From the original article talking about CH which is also independent:

> This independence is sometimes interpreted to mean that these questions have no answer, but most set theorists see that as a profound misconception. They believe the continuum has a precise size; we just need new tools of logic to figure out what that is. These tools will come in the form of new axioms.

I believe the same applies for BBs. They have precise values outside of ZFC but we still cannot ever know them because they are incomputable (??)

> but we still cannot ever know them because they are incomputable (??)

That doesn't mean you can't know them. We know BB(2). It means there is no single algorithm which is capable of yielding them all. But there could, theoretically, be an algorithm for BB(10), a different algorithm for BB(11), etc.

In fact, those individualized algorithms don't exist either.

Yes I was referring to calculating BB(n) for arbitrary n. But certainly these numbers exist even if they’re independent of ZFC (?)