It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.
replies(12):
Thus, any proof that BB(748) = N must either show that TM_ZF_INC halts within N steps or never halts. By Gödel's famous results, neither of those cases is possible if ZFC is assumed to be consistent.
BB(748) is by definition a finite number, and it has some value - we just don't know what it is. If an oracle told us the number, and we ran TM_ZFC_INC that many steps we would know for sure whether ZFC was consistent or not based on whether it terminated.
The execution of the turing machine can be encoded in ZFC, so it really is the value of BB(748) that is the magic ingredient. Somehow even knowledge of the value of this finite number is a more potent axiomatic system than any we've developed.
We already have more powerful systems, but what causes the inability to self-reason is exactly that power: only first order logic can prove its own consistency. Once you get powerful enough to model arithmetic, you can build statements with self-referential weirdness.
I don’t see it as a paradox, but as growth: a sufficiently rich system can pose questions which suggest a richer system — and thereby scaffold up the universe hierarchy.