Comment by Dylan16807

> I'd say that's a bit of a wrong or misleading statement. I think the correct version is "everything[1] can be encoded as a number". The concept of number is a very particular concept! It's pretty absurd to say "a screwdriver is a number" or "a word is a number". That is true for the peano axiomatization of numbers; but to me in particular, I believe numbers are a generalization (and formalization) of the idea or concept of quantity. There's a particular idea that refers to say 'two' apples, the quantity of apples. A word is not a quantity, it's a different concept. Even though each of them could be encoded as a number somehow!

Well if we're using a more narrow view, then "BB(748)" isn't a number, it's an encoding of a partial algorithm. And it shouldn't be surprising that an algorithm might be unprovable in ZFC.

The actual number, the quantity, is quite easy to write down inside ZFC. And so is the beaver turing machine itself. The hard part is knowing which of the 748-state machines is the beaver.