What does it mean for a number to be independent of ZFC?

Question

Since the definition of the Busy Beaver function by Radó in 1962, an interesting open question has been what [is] the smallest value of $n$ for which $BB(n)$ is independent of ZFC set theory.

Source: the first sentence of the abstract of the paper A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory, with the part in bold added by me (I think it was a typo, they likely forgot the "is").

They proceed to prove that such $n$ is at most 7918.

But $BB(7918)$ is a number, right? So what does it mean for a number to be independent of ZFC?

---

Bonus question: how much is $BB(7918)$?

Answer 1

Sure, $BB(7918)$ is some number. But it is provably beyond the capabilities of ZFC to figure out which number that is, or even an upper bound for that number.

Specifically, given any (very large, but constructively described) integer $D$, the statement $BB(7918)<D$ can never be proven with ZFC.

As to the bonus question, I've been fascinated with large number notation for a long time. Up-arrow notation, side-arrow notation, Graham's number and the Ackerman function are all cool, and combining them gives some truly mind-bogglingly large numbers. And, of course, one could always invent new, more powerful notation.

Even using recursive functions like the arrow notations mentioned above and the Ackerman function, and constructing new notation like those, I personally believe that there isn't enough room in the observable universe to describe a number anywhere close to $BB(7918)$. And even if it were possible, it's not like we could prove it.

Answer 2

To my understanding, that BB(x) is an uncomputable functions which means there's not a general solution to tell what is BB(x) in ZFC. And for specific BB like BB(1) and BB(2), etc. there's proof that they are equal to some number, but there's no universal proof for any BB(x). Then it's not hard to interpret that some BB may be proved to equal to some number in ZFC, while some BB cannot. And that statement says that for x>=7918, we cannot find a proof that BB(x) equals to a number. While ZFC we can only say that number exists.

Think of ZFC as a machine that can decide some statements whether it's ture or not, like 1=2 (false) or 1<0 (true), while we give a statement that D<BB(7918) is just out of its capatiblity and it cannot give you an answer, though BB(7918) indeed exist.