Re:BusyBeaver(6) Is Quite Large
by red75prime on Tuesday July 01, 2025 @07:56AM
(#44432981)
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.
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 ZFC+(BB(748)=Q) is consistent.