[Math] “Simpler” statements equivalent to Con(PA) or Con(ZFC)

Question

Given any reasonable formal system F (e.g., Peano Arithmetic or ZFC), we all know that one can construct a Turing machine that runs forever iff F is consistent, by enumerating the theorems of F and halting if it ever proves 0=1.

However, what interests me here is that the "obvious" such Turing machine will be an extremely complicated one. Besides the axioms of F, it will need to encode the symbols and inference rules of first-order logic, which (among other things) presumably requires writing a parser for context-free expressions. If you actually wrote the Turing machine out, it might have millions of states! Even in a high-level programming language, the task of writing a program that enumerates all the theorems of ZFC is not one that I'd casually give as homework.

Notice that this situation stands in striking contrast to that of universal Turing machines, which we've known since the 1960s how to construct with an extremely small number of states (albeit usually at the price of a complicated input encoding). It also contrasts with the observation that very small Turing machines can already exhibit "complicated, unpredictable" behavior: for example, the 5th Busy Beaver number is still unknown, and it seems like a plausible guess that the values of (say) BB(10) or BB(20) are independent of ZFC.

Thus my question:

Is any "qualitatively simpler" class of computer programs known, which can be proved to run forever iff ZFC is consistent? Here, by "qualitatively simpler," I mean doing something that looks much more straightforward than enumerating all the first-order consequences of the ZFC axioms, but that can nevertheless be proved by some nontrivial theorem to be equivalent to such an enumeration. Feel free to replace ZFC by ZF, PA, or any other system to which Gödel's Theorem applies if it makes a difference.

This question is clearly related to the well-known goal of finding "natural" or "combinatorial" statements that are provably independent of PA of ZFC, but it's not identical. For one thing, I don't demand that your statement have any independent mathematical interest—just that the computer program corresponding to your statement be easier to write than a program that enumerates all ZFC-theorems!

One concrete goal would be to find the smallest n for which you can prove that the value of BB(n) (the nth Busy Beaver number) is independent of ZFC. (It's clear that BB(n) is independent of ZFC for all n≥n₀, where n₀ is the number of states in a Turing machine that enumerates all ZFC-proofs and halts if it proves 0=1.)

As a first step, though, I'll be delighted to learn of any theorem that simplifies the task of writing proof-enumerating programs. (Even if the programs are still expressed in a high-level formalism, and are still horrendously complicated when compiled down to Turing machines.)

Answer 1

The discussion in the comments has helped clarify your question for me. I believe that it is closely related to the following remark by Harvey Friedman:

I am convinced that trying to take consistency statements like Con(ZFC + measurable cardinals) or Con(ZFC + rank into itself), Con(ZF + inaccessible rank into itself), etc., and force them into smaller and smaller Turing machines not halting, with demonstrable equivalence in an extremely weak system, is an open ended project, in the practical sense, that will create a virtually unlimited opportunity, in the practical sense, for a stream of ever and ever deeper mathematical ideas. Ideas that could come from unexpected sources, ideas that could have independent deep ramifications, ideas that -- well who knows what to expect. The benchmark is completely clear - how many quadruples? At the very least, deep ideas about set theory and large cardinals, but probably much more diverse deep ideas about, well, the unexpected. Any branch of mathematics whatsoever might prove useful, or even crucial, here. Whereas, we don't think that "any branch of mathematics" might be useful in logic problems, normally. This is different.

Other relevant postings from the FOM archives may be found here and here.

So Friedman's work, that Andres Caicedo alluded to in the comments, is probably the closest thing to what you want. I don't know of any other people who are working actively on this kind of project.

As a side remark, I believe that your intuition is correct that there is some kind of intrinsic "complexity" to the statement "ZFC is consistent," and roughly speaking it is because the totality of mathematical knowledge is a "complex" entity.