The Laver tables provide examples of programs which have not been shown to terminate in the standard axiomatic system of mathematics ZFC but which do terminate when one assumes very large cardinal axioms.
Introduction
The classical Laver tables An
are the unique finite algebras with underlying set {1,...,2n}
and an operation *
that satisfies the identity x * (y * z)=(x * y) * (x * z)
and where x*1=x+1
for x<2n
and where 2n*1=1
.
More information about the classical Laver tables can be found in the book Braids and Self-Distributivity by Patrick Dehornoy.
Challenge
What is the shortest code (in bytes) that calculates 1*32
in the classical Laver tables and terminates precisely when it finds an n
with 1*32<2n
? In other words, the program terminates if and only if it finds an n
with 1*32<2n
but otherwise it runs forever.
Motivation
A rank-into-rank cardinal (also called an I3-cardinal) is an extremely large level of infinity and if one assumes the existence of a rank-into-rank cardinal, then one is able to prove more theorems than if one does not assume the existence of a rank-into-rank cardinal. If there exists a rank-into-rank cardinal, then there is some classical Laver table An
where 1*32<2n
. However, there is no known proof that 1*32<2n
in ZFC. Furthermore, it is known that the least n
where 1*32<2n
is greater than Ack(9,Ack(8,Ack(8,254)))
(which is an extremely large number since the Ackermann function Ack
is a fast growing function). Therefore, any such program will last for an extremely long amount of time.
I want to see how short of a program can be written so that we do not know if the program terminates using the standard axiomatic system ZFC but where we do know that the program eventually terminates in a much stronger axiomatic system, namely ZFC+I3. This question was inspired by Scott Aaronson's recent post in which Aaronson and Adam Yedidia have constructed a Turing machine with under 8000 states such that ZFC cannot prove that the Turing machine does not terminate but is known not to terminate when one assumes large cardinal hypotheses.
How the classical Laver tables are computed
When computing Laver tables it is usually convenient to use the fact that in the algebra An
, we have 2n * x=x
for all x
in An
.
The following code calculates the classical Laver table An
# table(n,x,y) returns x*y in An table:=function(n,x,y) if x=2^n then return y; elif y=1 then return x+1; else return table(n,table(n,x,y-1),x+1); fi; end;
For example, the input table(4,1,2)
will return 12
.
The code for table(n,x,y)
is rather inefficient and it can only compute in the Laver table A4
in a reasonable amount of time. Fortunately, there are much faster algorithms for computing the classical Laver tables than the ones given above.
Ack(9,Ack(8,Ack(8,254)))
is a lower bound for the first table in which the first row has period 32, i.e. where1*16 < 2^n
? \$\endgroup\$ – Peter Taylor May 26 '16 at 22:36table(n,x,y)
, and I think it'll take between 25 and 30 states to set up the constants and the outer loop. The only direct TM representation I can find on esolangs.org is esolangs.org/wiki/ScripTur and it's not really that golfy. \$\endgroup\$ – Peter Taylor May 27 '16 at 22:09