Laver tables and “unprovable” statements
Laver tables are combinatorial objets whose definition is surprisingly simple. However, they do have somewhat weird properties, which come from their relationship with questions of set theorists (namely, how do elementary embeddings of models of set theory behave). It also have connections with braid group theory, which I do not know. The Wikipedia article gives the basic facts, a survey by Patrick Dehornoy will give relevant bibliography, and friends of mine wrote an undergraduate thesis on the subject (in French).
The most basic definition of Laver tables is the Cayley table of a self-distributive binary operation. This means we define an exotic operation on a set of numbers, and fill a square table with the outcomes of this operation. The required property of this operation is . This operation does not share properties with our usual operations, which are often associative of commutative. Suppose the set of numbers is and that 1 acts on the right by shifts : and . Then all columns of the table are determined by the following rule: , and so on so that . The trick is that , which is 0 by induction on k. The same method gives the value of by induction on j. However, the resulting operation will not be self-distributive unless n is a power of 2.
For a given number p, the sequence for increasing q is obtained by iterating and is thus periodic, with period a power of two (since repeating it n times returns back to p. Laver’s conjecture concerns the period of i.e. the least value of k such that . The small Haskell program below will compute this :
import List type LD = [[Int]] showLaver n = unlines $ map (unwords . map show) (genLaver n) genLaver :: Int -> LD genLaver n = l where l = reverse [ let sx = (x+1) `mod` n -- Itération de *(x*1) à partir de (x*1) lx = take n (iterate (\r -> (l!!r)!!sx) sx) in (last lx):(init lx) | x Maybe Int period t = lookup 0 (zip (tail (t!!1)) [1..n-1]) where n = length t main = do s <- getLine -- putStr . showLaver $ read s putStr "Period " putStr $ show $ period (genLaver (read s))
We see that the period is 2 when n=4, while it is 4 when n is 8 or 16, and 8 when n is between 25=32 and 28=256. Starting from , the period is 16 (actually my computer would explode for n>2048). Now if you are easily taken down by headaches, I recommend you do not read the following, and if you are a specialist, I beg pardon for any confusions I may have done.
The annoying fact is that it is not possible to prove using elementary arithmetic techniques (primitive recursive arithmetic) that this period can go over 16. Actually, this non-existence of proof can be rigorously proved. Another example of this phenomenon is the finiteness of Goodstein sequences, which cannot be proved by ordinary arithmetic, but can be proved using properties of ordinals, which are objects of usual mathematics. However, if I remember correctly, it is algorithmically possible to find a formula for the number of steps needed to terminate a Goodstein sequence (which is a really huge number). However, the difference here is that the proof of termination of Goodstein sequences involves ordinary mathematics, while it is possible to prove the period of Laver tables goes to infinity, but this involves intricate mathematical logic, and rather disputable assumptions. A worse reality is that even if there is a Laver table with period 32, nobody will ever be able to see it, nor to compute its size, because of the size of the known lower bound is even huger than the number appearing in Goodstein sequences (then why do we care ?).
The original reason why Laver tables appeared was the study of elementary embeddings. For this suppose you have a good mathematical universe, and consider in this universe well-founded sets : the empty set is well-founded, and we define inductively well-founded sets to be sets whose elements are well-founded sets. A well-founded set has a depth which can also be defined inductively as the least ordinal bigger than the depth of its elements. The sets of finite depth are just finite sets, and sets with depth bounded by a given ordinal form a rank (it’s probably more complicated actually). Occasionnally, a rank might be a model of set theory, which means you can reproduce all mathematics of ZFC axioms using only these sets. Unfortunately, incompleteness theorems forbid to prove this is possible using regular mathematics, would not be big enough. Probably even more infortunate is the fact that the only known proof of Laver’s theorem relies on the existence of such an embedding.
An elementary embedding is a “logical morphism” of a rank into itself, i.e. a function j which maps sets having given logical properties to sets having the same properties (in particular, if y is the power set of x, then j(y) is the power set of j(x)). Elementary embeddings can be “logically composed” in the following way : if f and g are elementary embeddings, then g has some definition, and is obtained by applying f to the logical definition of g. For example . Since applying f to something means applying f to everything (not only variables as with usual morphisms, but also operations), we also have so if $\latex f \star g$ denotes ,
which is the left-distributivity axiom.
Given an elementary embedding, define and , and an operation on numbers between 1 and N by an equivalence relation . This operation satisfies the self-distributivity axiom, and Laver defines a sequence of equivalence relations which allow to recover Laver tables of any size. Proving that their period goes to infinity then amounts to prove that some iterate of f cannot be equivalent to f for all equivalence relations: this is the content of Laver’s theorem, which states that two iterates are equivalent for all relations if and only if they are equal.