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_{0}, where n_{0} 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.)