BusyBeaver(6) Is Quite Large

Re:BusyBeaver(6) Is Quite Large by Scarblac on Saturday June 28, 2025 @03:40PM (#44407526)

I don't understand, surely if we assume ZFC is consistent then it's obvious that it won't halt? Even if its consistency can't be proven, neither can its inconsistency, so it won't halt. Or is that only provable outside of ZFC?

I guess it's also hard when we have an arbitrary Turing machine and have to prove that what it's doing isn't equilavent to trying to prove an undecibable statement.

[ Parent | on HN ]

Re:BusyBeaver(6) Is Quite Large by LegionMammal978 on Saturday June 28, 2025 @03:52PM (#44407627)

If you believe that ZF is consistent, then you believe that the machine cannot halt (assuming you trust its construction). But you cannot write a proof in ZF that the machine cannot halt. Such a proof must include a new axiom "ZF is consistent", or some stronger axiom.

[ Parent | on HN ]

Re:BusyBeaver(6) Is Quite Large by tromp on Saturday June 28, 2025 @03:47PM (#44407582)

If we assume ZFC to be consistent, then Gödel's 2nd incompleteness theorem tells us that it cannot prove its own consistency. So in particular it cannot prove than TM_ZFC_INC will never halt.

[ Parent | on HN ]