A relatively small turing machine whose behavior is independent of set theory

Since the definition of the Busy Beaver function by Rado in 1962, an interesting open question has been what the smallest value of n for which BB(n) is independent of ZFC set theory. Is this n approximately 10, or closer to 1,000,000, or is it even larger? In this paper, we show that it is at most 7,918 by presenting an explicit description of a 7,918-state Turing machine Z with 1 tape and a 2-symbol alphabet that cannot be proved to run forever in ZFC (even though it presumably does), assuming ZFC is consistent. The machine is based on work of Harvey Friedman on independent statements involving order-invariant graphs. In doing so, we give the first known upper bound on the highest provable Busy Beaver number in ZFC. We also present a 4,888-state Turing machine G that halts if and only if there is a counterexample to Goldbach’s conjecture, and a 5,372-state Turing machine R that halts if and only if the Riemann hypothesis is false. To create G, R, and Z, we develop and use a higher-level language, Laconic, which is much more convenient than direct state manipulation.