[LegionMammal978]

> How do we know that there would be consistency issues or Σ₁-soundness issues?

From Gödel's second incompleteness theorem, no consistent first-order recursively-axiomatizable theory (i.e., a theory that can have its proofs validated by a Turing machine) can prove its own consistency. Thus, to prove that your current theory (e.g., ZFC) is consistent, you must move to a stronger one (e.g., Aleph*). But then you can't prove the consistency of that without an even stronger theory, and so on. Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories.

> Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this?

Not really, other than some of my own ramblings on the bbchallenge Discord server. But it's not that long:

Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols, and checks whether it shows that a particular n-state machine halts. The TM then simulates all of the proven halters to see how long they run. By assumption, the longest-running machine M is included in this list. So this TM can compute BB(n), which is an impossibility. Therefore, the function f(n) cannot exist.

As a corollary, since it's "uncomputably difficult" to prove that the longest-running machine halts at all, it's no less difficult to fully establish the value of BB(n).

[srcreigh]

> Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories.

There is similar issue with even ZFC and PA. It’s not really a dealbreaker imo.

> Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols

The issue with that argument is that the TM which enumerates every valid proof can’t exist in the first place.

If you fix an axiomatic theory, it’s already known that the theory has a limit.[1]

If every theory has a limit, you need countably infinitely many axiomatic theories together to prove BB(n) for all n. So there’s no TM which can even enumerate all the proofs, since a TM must have finite states, and thus can’t enumerate infinitely many proof systems.

(In fact for similar reasons I believe a Halt program, which has infinite states but which works for all TMs with finite states, platonically exists. It’s an emulator and an infinitely long busy beaver number lookup table. The diagonalization argument doesn’t apply, since the infinite Halt doesn’t accept itself as input.

This Halt would have countably many states since each busy beaver number is finitely calculated and there’s only countably many of them.)

So it’s not clear that f(n) is uncomputable. If f(n) is the symbol count and not the binary encoded length of the symbols, it even seems that it’s trivially bounded by some constant for all n. The proof could be one symbol the meaning of which is encoded in the theory.

It is a fascinating question though. I’m sure there is some function of axiomatic theory proof checker TM size and binary encoded proof length which does grow with n. It’s unclear if it would be uncomputable though.

The consequence of it being uncomputable is that the universe doesn’t have the resources to even encode the theory and/or represent it’s proofs.

In fact I suppose even as long as it grows at all, there would be a limit to BB(n) which can be possibly determined. Very fascinating

[1]: page 5 https://www.scottaaronson.com/papers/bb.pdf

[LegionMammal978]

> There is similar issue with even ZFC and PA. It’s not really a dealbreaker imo.

We obtain PA from our basic intuitions about how the standard integers work, derived from empirical evidence. Everything past that involves increasing levels of intuition. So to continue it indefinitely, you must postulate an infinite amount of correct intuition, in some magical fashion that can never be captured in a computer. You can claim unlimited ingenuity all you want, but there's no a priori reason that it should indefinitely yield the truth, especially when it goes far, far past what our finite empiricism can provide.

We just haven't hit these limits yet, since very weak inductive theories are still sufficient for proving BB(5): we don't even need the full power of PA yet for our non-halting proofs. Thus why it looks like it should be so easy.

> If you fix an axiomatic theory, it’s already known that the theory has a limit.[1]

Not quite. Fix some consistent axiomatic theory T which proves PA. Then there will be infinitely many TMs which do not halt (in the standard model), but T cannot prove that they cannot halt, due to incompleteness. (Therefore T cannot settle the BB(n) question past a certain point, as Aaronson correctly says.)

But for every TM that does halt (in the standard model), T can prove that it halts, and the proof is to list out a trace of the TM's execution. Thus, every halting machine of every length has a halting proof in T.

The only benefit of a more powerful theory T is that it can "compress" this maximal BB(n)-sized proof into something more physically managable. But once we fix a certain T, we find (by my earlier argument) that it can only compress the proof so far, and the compressed size still must be an uncomputable function.

We can also see this by a forward argument, instead of by contradiction. Suppose that we'll accept any halting proof in a theory T. Then we can write a TM that lists through all proofs in T that are smaller than some bound N. (Notice that this is a finite set, since I've put an upper bound on it!) Then, for every proof that is a valid halting proof, the TM runs the corresponding machine. Then, the TM will halt, and its halting time will be greater than the halting time of any machine that can be proven to halt in T within N symbols. Set N to Graham's number (which is easily definable), and now the halting proof of the TM in T will not fit in our light cone.

(Notice how our TM clearly halts if T is Σ₁-sound! But since T cannot prove its own Σ₁-soundness, it doesn't have any way to prove our TM halting other than by the brute-force method.)

> In fact for similar reasons I believe a Halt program, which has infinite states but which works for all TMs with finite states, platonically exists. It’s an emulator and an infinitely long busy beaver number lookup table. The diagonalization argument doesn’t apply, since the infinite Halt doesn’t accept itself as input.

In that case, you just end up with the well-known oracle halting problem, where you equip a TM with access to this "infinite-state" machine. Then the problem is that you have a more powerful model of computation, but still with no way of solving its own halting problem. Much like how a consistent theory can only prove the consistency of weaker theories, not its own consistency.

> So it’s not clear that f(n) is uncomputable. If f(n) is the symbol count and not the binary encoded length of the symbols, it even seems that it’s trivially bounded by some constant for all n. The proof could be one symbol the meaning of which is encoded in the theory.

Of course I'm fixing a particular theory and a particular alphabet of constant size, the alternative would be absurd. The important part is about the ultimate behavior as n varies.

[srcreigh]

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.

[LegionMammal978]

> We don’t need a printout of grahams number computation to know a TM which computes it halts. why impose that here?

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.

[srcreigh]

Thanks for explaining this, it truly is fascinating.

This appears to be an argument that almost every axiomatic theory isn't Σ₁-sound. So I can only ask a few things:

1. How do I even learn about Σ₁-soundness? I've tried for 30 minutes now to search for it.

2. Is my impression correct? Does this argument show that for ex ZFC is not Σ₁-sound? If not, which axiomatic theories exactly fall into this trap?