Re:BusyBeaver(6) Is Quite Large
by Strilanc on Saturday June 28, 2025 @07:16PM
(#44408970)
Isn't that incompatible with the models being consistent?
Suppose model A proves BB(748) = X and model B proves BB(748) = Y > X. But presumably the models can interpret running all size 748 Turing machines for Y steps. Either one of the machines halts at step Y (forming a proof within A that BB(748) >= Y contradicting the assumed proof within A that BB(748) = X < Y) or none of the machines halts at step Y (forming a proof within B that BB(748) != Y contradicting the assumed proof within B that BB(748) = Y).
I'm guessing the only way this could ever work would be some kind of nastiness like X and Y aren't nailed down integers, so you can't tell if you've reached them or not, and somehow also there's a proof they aren't equal.
Re:BusyBeaver(6) Is Quite Large
by Kranar on Saturday June 28, 2025 @08:35PM
(#44409368)
The issue is that X and Y are not actual natural numbers. They are mathematical objects that satisfy all the ZFC axioms and Peano arithmetic but are infinitely large. The issue is that ZFC underspecifies natural numbers.
Suppose model A proves BB(748) = X and model B proves BB(748) = Y > X. But presumably the models can interpret running all size 748 Turing machines for Y steps. Either one of the machines halts at step Y (forming a proof within A that BB(748) >= Y contradicting the assumed proof within A that BB(748) = X < Y) or none of the machines halts at step Y (forming a proof within B that BB(748) != Y contradicting the assumed proof within B that BB(748) = Y).
I'm guessing the only way this could ever work would be some kind of nastiness like X and Y aren't nailed down integers, so you can't tell if you've reached them or not, and somehow also there's a proof they aren't equal.