[FOM] Yedidia and Aaronson : Turing machines, Stationary Ramsey, Busy Beaver

[Olivier Gerard]

>From Scott Aaranson's blog, something that will be of interest to
members of the list. It makes explicit reference to Harvey Friedman's work

http://www.scottaaronson.com/blog/

http://www.scottaaronson.com/busybeaver.pdf

>From the abstract:
"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."
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160504/923ff9d6/attachment.html>