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

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

• It became BB(1919) after some work. – Asaf Karagila Mar 8 at 0:09
• I think the underlying question is why would the value of any $BB(n)$ be independent of ZFC. One reason is that you can have Turing machines that halt if and only if there is an inconsistency in ZFC. For instance, the machine attempts to list all proofs, and stops as soon as one of these proofs is a proof of an inconsistency, in which case it may, say, output a code for such a proof. Say you can do this with $n$ states. If ZFC is consistent, such a machine never halts, so it is not used in the computation of $BB(n)$, but if ZFC is inconsistent, the machine matters for this value; – Andrés E. Caicedo Mar 8 at 0:24
• moreover, presumably any code for such a proof would be rather enormous, so this would certainly affect the value of $BB(n)$. – Andrés E. Caicedo Mar 8 at 0:25

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) can never be proven with ZFC.
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.
• Actually, there's a way to write down that number: Just give the specification of the Turing machine implementing the corresponding Busy Beaver. This is constructive, because given that description you can, through a deterministic process, determine in finite time the number (just run the Busy Beaver; it is by definition a Turing machine that halts). And the description of a $7918$-state Turing machine may be large, but certainly not too large to write down in the observable universe. – celtschk Mar 8 at 7:12