>This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whethe

>This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC. This is a false statement. The fact that BB(745) can't be constructed using ZFC does not mean that it has multiple values. All it means is that there is at least one Turing Machine that never halts but can't be proven to run forever using ZFC, that is it. BB(745) is one specific integer, there is nothing really special about ZFC in this sense, it's just one axiomatic system that happens to be very useful as the foundation of most of the mathematics that is studied, but one could just as easily work with a different axiomatic system instead. There are values of BB(n) that have no construction using Peano arithmetic but do have a construction in ZF, and there are values of BB(n) that do not have a construction in ZF but have one in ZFC, and there are values of BB(n) that do not have a construction in ZFC but do have one in ZFC + Inaccessible Cardinal Axiom, so on so forth. ZFC does not have some kind of authoritative status in the universe of mathematics; it's possible that an alien race is doing mathematics using a far more powerful axiomatic system in which case BB(745) is constructible but BB(7450) is not. >All finite digit sequences can be constructed. A construction is a proof that provides a means of calculating a given value [1]. The set of all theorems that can be enumerated in ZFC do not contain a construction for the value of BB(745). [1] https://en.wikipedia.org/wiki/Constructive_proof https://en.wikipedia.org/wiki/Constructive_proof