Comment by red75prime
8 months ago
> a model where BB(748) = Q is not the actual BB, it's some other function
What it means specifically? ZFC+~(BB(748)=N) allows to extend definition of the Turing machine to a non-standard number of steps?
Can "BB(748) is undefined" be a provable theorem in ZFC+~(BB(748)=N) instead?
While we know that ZFC+~(BB(748)=N) is consistent, we don't know whether \exist Q!=N where ZFC+(BB(748)=Q) is consistent.
Intuitively I see it as: by adding axiom ~(BB(748)=N), we codify that this formal system isn't powerful enough to describe a Turing machine with 748 states (and probably all the machines with number of states greater than 748).
It seems to be even easier: BB codomain is a set of standard natural numbers regardless of which model of ZFS we are using. Therefore BB(748)=Q is false for every non-standard natural number Q.
We can come up with some function BB' that admits that, but it's just a different function.
It seems we can't even define a function with standard domain and non-standard codomain while not using literals for non-standard numbers in its definition.
That is ~(BB(748)=ActualValueOfBB748) is false even if it can't be proven in ZFC. In a sense, busy beaver creates its own mathematical reality.