|
|
|
|
|
|
by srcreigh
716 days ago
|
|
|
Thanks for typing all that out. It is very fascinating. I’m just not convinced that fixing a theory and disallowing soundness axioms is any practical impairment for discovering busy beaver numbers. Of course things get out of hand, but then why not collect evidence for soundness and let proofs avoid including an actual execution of the TM? We don’t need a printout of grahams number computation to know a TM which computes it halts. why impose that here? Has anybody done a compilation of such a PA proof generating/checking and simulating TM? It must have an enormous number of states and almost certainly wouldn’t be the BB of its cohort. Not including how it should be a similar thing where to prove it’s step count we shouldn’t need to emulate it. |
|
|
Of course, the TM which "computes Graham's number" can trivially be proven to halt, without running it fully.
But it is much harder to show that the TM (let's call it M) which "computes Graham's number, then plugs it into a big halting-proof generator (in a fixed theory T) as an upper bound on the number of symbols, then executes each proven-halting TM in order" also halts.
The problem is, just because a theory T gives a halting proof for a machine, doesn't necessarily mean that it halts. (That is, T isn't necessarily Σ₁-sound.) And if that doesn't hold, then M might run into a "fake halter" that can be proven halting in T, but doesn't truly halt in the standard model. Thus, the only ways to show that M halts are to either establish that T is Σ₁-sound, which can only be done by appealing to a stronger theory, or to run through each of the Graham's number of proofs, which takes astronomically long.
This is similar to an instance of the Berry paradox: if you could easily prove that M halts, then it would have a relatively short halting proof within T. But then it would find its own halting proof, and simulate itself. But then it would simulate itself simulating itself, etc., etc., and never actually halt. So T wouldn't be Σ₁-sound, since M doesn't halt even though you proved that it halts. The only way out of this trap is if M doesn't simulate itself, i.e., it takes more than Graham's number of symbols in its own halting proof in T.