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):
I'm well aware that BB(748) is an integer definable in classical logic. My claim is that "integer definable in classical logic" does not actually correspond well to what people mean by "number" in almost any other setting when pushed to extremes such as this.