News for hackers. Stuff that matters.
Re:BusyBeaver(6) Is Quite Large by red75prime on Monday June 30, 2025 @03:43AM (#44420542)
> 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 ZFC+(BB(748)=Q) is consistent.

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.