Laver tables and “unprovable” statements

20 February 2009 at 4:51 pm 4 comments

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 \star on a set of numbers, and fill a square table with the outcomes of this operation. The required property of this operation is a \star (b \star c) = (a \star b) \star (a \star c). This operation does not share properties with our usual operations, which are often associative of commutative. Suppose the set of numbers is \{0, 1, ..., n-1\} and that 1 acts on the right by shifts : i \star 1 = i+1 and (n-1) \star 1 = 0. Then all columns of the table are determined by the following rule: (0 \star 2) = (0 \star 1) \star (0 \star 1) = 2, and so on so that 0 \star x = x. The trick is that (n-1) \star (k+1) = ((n-1) \star k) \star 0, which is 0 by induction on k. The same method gives the value of i \star j 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 p \star q for increasing q is obtained by iterating \bullet \star (p+1) 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 1 \star k i.e. the least value of k such that 1 \star k = 1 \star 0 =  0. 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 n = 2^9 = 512, 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 \lambda form a rank V_\lambda (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, \lambda 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 f[g] is obtained by applying f to the logical definition of g. For example f[g](f(x)) = f(g(x)). Since applying f to something means applying f to everything (not only variables as with usual morphisms, but also operations), we also have f[g[h]] = f[g][f[h]] so if $\latex f \star g$ denotes f[g],
f \star (g \star h) = (f \star g) \star (f \star h) which is the left-distributivity axiom.

Given an elementary embedding, define f_0 = \mathrm{Id} and f_{n+1} = f_n[f], and an operation p \star q = r on numbers between 1 and N by an equivalence relation f_p[f_q] \simeq f_r. 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.

Entry filed under: algebra, combinatorics, english, logic. Tags: , , , , .

Ten constructions of the cohomology of varieties Rational approximations of √2

4 Comments Add your own

  • 1. Antrire  |  4 March 2010 at 5:56 pm


    “The annoying fact is that it is not possible to prove using elementary arithmetic techniques (Peano arithmetic) that this period can go over 16. Actually, this non-existence of proof can be rigorously proved.”

    Could you give a reference to this unprovability result? Thanks a lot!

    • 2. remyoudompheng  |  4 March 2010 at 8:29 pm

      I gave a link to an article of P. Dehornoy which gives an idea of why it is so: it roughly says that if you could prove that the period goes to infinity, you would have to manipulate integers so large that no reasoning in terms of elementary arithmetic could possibly generate them, which is a contradiction.

      • 3. Antrire  |  4 March 2010 at 10:21 pm

        Thanks. But Dehornoy’s article only proves that the function is not provably total in Primitive Recursive Arithmetic, which is significantly weaker than Peano Arithmetic. For example, the Ackermann function is not primitive recursive, but its totality is provable in PA.

        • 4. remyoudompheng  |  5 March 2010 at 7:36 am

          Then I think I misquoted the paper: I updated my post accordingly.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Trackback this post  |  Subscribe to the comments via RSS Feed



%d bloggers like this: