[waluigi]

It’s even more counterintuitive than you let on! If you are working in ZFC along with the axiom “ZFC is consistent” then there’s no issue: just a normal number[1]. Where things get really strange is in ZFC plus the axiom “ZFC is inconsistent”.

This already sounds like an inconsistent theory, but surprisingly isn’t: Godel’s second incompleteness theorem directly gives us that Con(ZFC) is independent, so there are models that validate both Con(ZFC) and ~Con(ZFC). The models that validate ~Con(ZFC) are very confused about what numbers are: from the models perspective, there is a number corresponding to a Godel code for the supposed proof of inconsistency, but from the external view this is a “nonstandard number”: it’s not not a finite numeral!

Getting back to BB(748): what does this look like in a model of ZFC + ~Con(ZFC)? We can prove that the machine internal to the model will find that astronomically large Godel code, so BB(748) will be a nonstandard number. In other words, you can tell if a 748 state machine will terminate in this model: you’ve just got to run it for a number of steps that’s larger than every finite numeral!

[1]: unless there’s some machine that with 748 that enumerates theorems of ZFC+Con(ZFC) but that’s a different discussion.