Laver table computations and an algorithm that is not known to terminate in ZFC 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&lt;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&lt;2n? In other words, the program terminates if and only if it finds an n with 1*32&lt;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&lt;2n. However, there is no known proof that 1*32&lt;2n in ZFC. Furthermore, it is known that the least n where 1*32&lt;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.
Binary Lambda Calculus, 215 bits (27 bytes)

\io. let
  zero = \f\x. x;
  one = \x. x;
  two = \f\x. f (f x);
  sixteen = (\x. x x x) two;
  pred = \n\f\x. n (\g\h. h (g f)) (\h. x) (\x. x);
  laver = \mx.
    let laver = \b\a. a (\_. mx (b (laver (pred a))) zero) b
    in laver;
  sweet = sixteen;
  dblp1 = \n\f\x. n f (n f (f x)); -- map n to 2*n+1
  go2 = \mx. laver mx sweet mx (\_. mx) (go2 (dblp1 mx));
in go2 one


compiles to (using software at https://github.com/tromp/AIT)

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010


This solution is mostly due to https://github.com/int-e