Outdated Archival Version

These pages are not updated anymore. They reflect the state of 20 August 2005. For the current production of this journal, please refer to http://www.math.psu.edu/era/.

%_ **************************************************************************
%_ * The TeX source for AMS journal articles is the publisher's TeX code    *
%_ * which may contain special commands defined for the AMS production      *
%_ * environment.  Therefore, it may not be possible to process these files *
%_ * through TeX without errors.  To display a typeset version of a journal *
%_ * article easily, we suggest that you either view the HTML version or    *
%_ * retrieve the article in DVI, PostScript, or PDF format.                *
%_ **************************************************************************
%  Author Package
%% Translation via Omnimark script a2l, March 20, 1997 (all in one day!)

\controldates{2-APR-1997,2-APR-1997,2-APR-1997,2-APR-1997}
\documentclass{era-l}
\issueinfo{3}{4}{January}{1997}
\dateposted{April 9, 1997}
\pagespan{28}{37}
\PII{S 1079-6762(97)00020-6}


%% Declarations:

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\theoremstyle{plain}
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{proposition}[definition]{Proposition}


%% User definitions:

\newcommand{\cala}{{\mathbf A}}
\newcommand{\calp}{{\mathbf P}}
%\newcommand{\LD}{{\rm (LD)}}
%%  argument form of \LD in amstex source: /
\newcommand{\Lavlaws}{{\rm(LL)}}
%%  argument form of \Lavlaws in amstex source: /
\newcommand{\critfunc}{{\text {\rm cr}}}
\newcommand{\crit}[1]{{\critfunc ({#1})}}
\newcommand{\tLequiv}[1]{\equiv ^{#1}}
%%  argument form of \tLequiv in amstex source: #1/
\newcommand{\id}{\text {\rm id}}
\newcommand{\cf}{\operatorname {cf}}
\newcommand{\E}{{\mathcal E}}
\newcommand{\Ord}{{\mathcal O}}
\newcommand{\natnum}{{\mathbb N}}
\newcommand{\appless}[2]{#1({<}#2)}


\begin{document}

\title{Left-distributive embedding algebras}
\author{Randall Dougherty}
\address{Department of Mathematics, Ohio State University,
Columbus, OH 43210}
\email{rld@math.ohio-state.edu }
\author{Thomas Jech}
\address{Pennsylvania State University, 215 McAllister Building,
University Park, PA 16802}
\email{jech@math.psu.edu }
%\issueinfo{3}{1}{}{1997}
\copyrightinfo{1997}{American Mathematical Society}
\subjclass{Primary 20N02; Secondary 03E55, 08B20}
\begin{abstract}
We consider algebras with one binary operation~$\cdot $ and one generator,
satisfying the left distributive law $a\cdot (b\cdot c)=(a\cdot b)\cdot (a\cdot c)$; such algebras have been shown to have surprising
connections with set-theoretic large cardinals and with braid groups.
One can construct a sequence of finite left-distributive algebras~$A_{n}$,
and then take a limit to get an infinite left-distributive
algebra~$A_{\infty }$ on one generator.  Results of Laver and Steel
assuming a strong large cardinal axiom imply that $A_{\infty }$~is free;
it is open whether the freeness of~$A_{\infty }$ can be proved without the
large cardinal assumption, or even in Peano arithmetic.  The main result
of this paper is the equivalence of this problem with the existence of
a certain left-distributive algebra of increasing functions on natural
numbers, called an {\em embedding algebra}, which emulates some properties
of functions on the large cardinal.  Using this and results of the first
author, we conclude that the freeness of~$A_{\infty }$ is unprovable in
primitive recursive arithmetic.
\end{abstract}
\thanks{The first author was supported by NSF grant number
DMS-9158092 and by a grant from the Sloan Foundation.}
\thanks{The second author was supported by NSF grant number
DMS-9401275.}
\date{December 16, 1996}
\commby{Alexander Kechris}
\keywords{Left-distributive algebras, elementary embeddings, critical
points, large cardinals, primitive recursive arithmetic}
\maketitle



\section{Introduction}\label{sec:1}

We consider algebras with one binary operation~$\cdot $ and one
generator satisfying the left distributive law
$a\cdot (b\cdot c)=(a\cdot b)\cdot (a\cdot c)$.

Such algebras became an object of study when they appeared in a
set-theoretic context: Laver~\cite{10} studied the properties
of an algebra of elementary embeddings arising from an extremely large
cardinal.  He used these properties to prove purely algebraic results
about the free left-distributive algebra on one generator; for instance,
he showed that the word problem for this algebra is decidable.
However, this was under the assumption that a large cardinal exists.

Later Dehornoy~\cite{3} proved these algebraic results
using a completely different construction based on braid groups
and generalizations of them, thus eliminating the large cardinal
hypothesis.  (Perhaps even more surprising, results about
left-distributive algebras have recently been used to prove
theorems about braid groups; see Dehornoy~\cite{4}.)

But further algebraic results were obtainable from the large
cardinal.  Laver~\cite{11} used restrictions of the
original elementary embeddings to produce a sequence of
{\em finite} left-distributive algebras~$A_{n}$; these algebras
can also be constructed directly, without large cardinals.  One can
then take a limit of these algebras to get an infinite left-distributive
algebra~$A_{\infty }$ on one generator.

In the large cardinal context, it turns out that such a limit yields
the original algebra of elementary embeddings, so it is free on one
generator.  So ``$A_{\infty }$~is free'' is another statement about small
(finite or countable) algebras proved from a large cardinal hypothesis.
This statement can be rephrased in purely algebraic form, as an assertion
that certain equations do not imply certain other equations under the
left distributive law.

It is now natural to ask whether the freeness of~$A_{\infty }$ can be
proved without the large cardinal assumption, or even at the level of
basic arithmetic (Dehornoy's proofs can be formalized at that level).
The results we present here provide, to some extent, a negative
answer to this question; we show that the freeness of~$A_{\infty }$
cannot be proved at a low level (Primitive Recursive Arithmetic, or PRA,
which is often referred to as the formal version of Hilbert's
`finitistic reasoning').

The main result of this paper is the equivalence of ``$A_{\infty }$~is free''
with the existence of a certain algebra of increasing functions on
the set~$\natnum $ of natural
numbers.  We introduce {\em embedding algebras}, which are algebras~$(A,
\cdot )$ of increasing functions $a \colon \natnum \to \natnum $ endowed with
a binary operation~$\cdot $.  The axioms for embedding algebras state
that the operation~$\cdot $ is left-distributive and that, if
$\crit {a}$~is the least number moved by~$a$ (assuming $a$~is not the identity),
then $\crit {a\cdot b} = a(\crit {b})$.  If a nontrivial embedding algebra
(one which contains a function other than the identity) exists, then
$A_{\infty }$ is free; conversely, we construct a nontrivial embedding
algebra under the assumption that $A_{\infty }$ is free.

The first author proved~\cite{5} that the elementary embeddings
from the large cardinal above yield numerical functions which
grow faster than any primitive recursive function, and hence
cannot be proved to exist in~PRA.  The properties of embedding
algebras allow us to emulate this construction and produce
the same fast-growing functions.  Therefore, the existence
of nontrivial embedding algebras, and hence the freeness of~$A_{\infty }$,
cannot be proved in~PRA.

In Sections \ref{sec:2} to \ref{sec:5} we outline the main results. Full proofs
will appear elsewhere~\cite{7}.

\section{Free left-distributive algebras and elementary embeddings}\label{sec:2}

We consider algebras with one binary operation~$\cdot $ generated by a
single element that we denote by the symbol~$1$.  We shall often
write $ab$ instead of $a\cdot b$, and use the convention that
$abc=(ab)c$.

The {\em left distributive law} is the identity
\begin{equation*}a(bc)=ab(ac).
\tag{LD}\label{tagld}
\end{equation*}
Let $W=W_{\cala }$ be the set of all words built up from~$1$ using
the operation $\cdot $. Denote by~$\equiv $ (or by~$\equiv _{\cala }$)
the equivalence relation on~$W$ given by:
$a\equiv b$ iff the equation $a=b$ is a consequence of~\eqref{tagld}.
Then $\cala =W/{\equiv }$ is the free left-distributive algebra on one
generator.

For the rest of this section, let $(A,\cdot )$ be a left-distributive
algebra generated by~$1$.  We will summarize the relevant known
results on such algebras.

\begin{definition}\label{dfn2.1} 
For $a,b \in A$, say that $a$~is a {\em left subterm} of~$b$,
or $a<_{L}b$, if, for some $c_{1},\dots ,c_{k}$ ($k>0$), $b=ac_{1}\dotsm c_{k}$.
\end{definition}


Clearly the relation~$<_{L}$ is transitive.

\begin{theorem}[Dehornoy {\cite{1}}]\label{thm2.2} On the free algebra~$\cala $,
the relation~$<_{L}$ is connected: for all $a,b\in \cala $, either
$a= b$ or $a<_{L}b$ or $b<_{L}a$.
\end{theorem}


It follows that $<_{L}$~is connected in any monogenic
(i.e., generated by one element)
left-distributive algebra~$(A,\cdot )$.  Therefore, $<_{L}$~is
a strict linear ordering of~$A$ if and only if it is irreflexive,
i.e., $a \not <_{L} a$ for all~$a$.

\begin{lemma}[Dehornoy {\cite{1}}]\label{lem2.3} 
If the relation $<_{L}$ on~$A$ is
irreflexive, then $(A,\cdot )$~is free and satisfies left cancellation.
\end{lemma}


\begin{theorem}[Dehornoy {\cite{3}}]\label{thm2.4} There is an algebra
$(A,\cdot )$
on which $<_{L}$ is irreflexive.
Consequently, the free algebra is linearly ordered
by~$<_{L}$ and satisfies left cancellation.
\end{theorem}


These results were also proved by Laver~\cite{10} under a large
cardinal assumption (see below).

All of the steps in Dehornoy's proofs are accomplished by explicit
recursions and inductions, and the recursions are in fact primitive recursions. 
Therefore, these results can be proved in a very basic theory of arithmetic,
such as Primitive Recursive Arithmetic (PRA).  PRA is formalized 
in a language containing function symbols for all possible function
definitions using the constant $0$, the successor function ${}'$,
composition, and primitive recursion; it has axioms stating that the
function symbols satisfy their definitions, and that $0' \ne 0$, and
a rule of inference allowing induction on quantifier-free formulas.
(See Sieg~\cite{12} for more details.)  This theory is among the
weakest of the commonly studied fragments of arithmetic.  It is not hard
to show that the methods used to prove the above results can be formalized in
this theory.

Now consider algebras with two binary operations $\cdot $ and~$\circ $.
We use the conventions $ab\circ c=(ab)\circ c$ and $a\circ bc=a\circ (bc)$.
Let $W_{\calp }$ be the set of all words built up from~$1$ using both
operations, and let $\calp $ be the free algebra on one generator under
the identities:
\begin{equation*}\begin{gathered}
a\circ (b\circ c)=(a\circ b)\circ c, \\
(a\circ b)c=a(bc), \\
a(b\circ c)=ab\circ ac, \\
a\circ b=ab\circ a.
\end{gathered}\tag{LL}\label{tagll}
\end{equation*}
Then $\calp = W_{\calp }/ \equiv _{\calp }$, where
$a\equiv _{\calp }b$ iff the equation $a=b$ is a consequence of~\eqref{tagll}.
Note that \eqref{tagld} ~is provable from~\eqref{tagll}:
\begin{equation*}a(bc)=(a\circ b)c=(ab\circ a)c=ab(ac).
\end{equation*}

The motivation for axioms~\eqref{tagll}  comes from large cardinal theory.
Let $V_{\lambda }$
be the collection of all sets of rank less than~$\lambda $, where
$\lambda $~is a limit ordinal. If $\E $~is the set of all
elementary
embeddings from~$V_{\lambda }$ to~$V_{\lambda }$, then one can `almost'
define a binary operation~$\cdot $ on~$\E $
by: $j \cdot k$
is the result of applying~$j$ to~$k$.  This does not quite work, because
$k$~is too large to be in the domain of~$j$.  Instead, one can
break~$k$ into pieces which are small enough for~$j$ to digest,
and recombine the results:
\begin{equation*}j\cdot k = \bigcup _{\alpha < \lambda } j(k \cap V_{\alpha }).
\end{equation*}
Then $j \cdot k$ will also be in~$\E $, and it is easy to show that
the operation~$\cdot $ is left-distributive and, together with
the operation~$\circ $ of composition, satisfies~\eqref{tagll}.

If $j$~is a nontrivial elementary embedding from~$V_{\lambda }$
to~$V_{\lambda }$, let $(A_{j},{\cdot })$ and~$(P_{j},{\cdot },{\circ })$
be the subalgebras of~$(\E ,{\cdot })$ and~$(\E ,{\cdot },{\circ })$
generated by~$j$.
Laver~\cite{10} shows, among other
things, that
$(A_{j},\cdot )$ and $(P_{j},\cdot ,\circ )$ are respectively the free monogenic
left-distributive algebra and the free monogenic algebra satisfying
axioms~\eqref{tagll}.

Again, we summarize some known facts about algebras~$(P,\cdot ,\circ )$.

Clearly an algebra satisfying~\eqref{tagll}  yields an algebra
satisfying~\eqref{tagld}, simply by dropping the second operation
(and taking a subalgebra, if we want the result to be monogenic).
But one can move in the other direction as well:

\begin{proposition}[Laver {\cite{10}}, Dehornoy {\cite[Prop.
2]{2}}]\label{prop2.5} Any algebra~$(A,{\cdot })$
satisfying \eqref{tagld}  can be extended and expanded to an algebra
$(P,{\cdot },{\circ })$ satisfying\/~\eqref{tagll}.\end{proposition}


\begin{proposition}\label{prop2.6}
Let\/ $(P,{\cdot },{\circ })$ be an algebra
satisfying\/~\eqref{tagll}  and generated by\/~$1$, and let\/~$(A,{\cdot })$ be
the subalgebra of\/~$(P,{\cdot })$ generated by\/~$1$.  Then\/ $(P,{\cdot },{\circ })$~is a free\/ \eqref
{tagll}-algebra if and only if\/ $(A,{\cdot })$~is a free
left-distributive algebra. \end{proposition}


The proof of Propostion~2.6 can be carried out in~PRA.

Now consider the algebras $A_{j}$ and~$P_{j}$ of elementary embeddings. For each
nontrivial elementary embedding~$a$ from~$V_{\lambda }$ to itself, let~$\crit {a}$
be the {\em critical point} of~$a$, i.e., the least ordinal moved by~$a$. Let
$\Gamma $ be the set of all ordinals which are critical points of elements
of~$A_{j}$.
We note that
\begin{equation*}\crit {ab} = a(\crit {b}),\qquad \crit {a \circ b} = \min (\crit {a},\crit {b}).
\end{equation*}
Consequently, the critical point of every $a \in P_{j}$ is in~$\Gamma $, and
every $a \in P_{j}$ maps~$\Gamma $ into~$\Gamma $.

\begin{theorem}[Laver and Steel {\cite{11}}]\label{thm2.7}
The set\/~$\Gamma $ has order type $\omega $. \end{theorem}


\begin{theorem}[Laver {\cite{11}}]\label{thm2.8} For every $a,b \in A_{j}$, if
$a \ne b$, then $a(\gamma )\ne b(\gamma )$ for some $\gamma \in \Gamma $.
\end{theorem}


One can adjoin to $P_{j}$ the identity
embedding~$\id $. The extended algebra still satisfies axioms~\eqref{tagll}, as
well as these rules:
\begin{equation*}\id \cdot a = a,\quad a\cdot \id =\id ,\quad a\circ \id =
\id \circ a=a.
\end{equation*}

\section{A limit of finite left-distributive algebras}\label{sec:3}

In this section, we describe, for each natural number~$n$, an algebra~$A_{n}$ on 
$\{0,1,\dots ,2^{n}-1\}$ with a binary operation
$*_{n}$ satisfying the left distributive law.  We also describe a
second operation~$\circ _{n}$ on this set so that the resulting
two-operation algebra~$P_{n}$ satisfies~\eqref{tagll}.  
We then construct limit algebras $(A_{\infty },{\cdot })$ 
and $(P_{\infty },{\cdot },{\circ })$. 

The construction of these finite algebras is due to Laver; Wehrung proved some
additional properties of them.  The proof of
the following theorem has been reconstructed independently by
several people, including the authors.

\begin{theorem}[mostly Laver]\label{thm3.1}
There are unique operations $*_{n}$ and $\circ _{n}$ on the set
$A_{n}=P_{n}=\{0,1,\dots ,2^{n}-1\}$
such that the axioms\/~\eqref{tagll}  hold and, for all $a \in P_{n}$,
\begin{equation*}a*_{n} 1 = a+1 \bmod 2^{n}.
\end{equation*}
\end{theorem}


The operation~$*_{n}$ can be defined by an explicit double recursion
(which is more naturally performed over $\{1,2,\dots ,2^{n}\}$
rather than $\{0,1,\dots ,2^{n}-1\}$); then $\circ _{n}$~can be defined
by the formula $a \circ _{n} b = (a *_{n} (b+1)) - 1$, where the addition
and subtraction are performed modulo~$2^{n}$.
The theorem is then proved by multiple inductions.  Along the way,
one obtains additional results: reduction modulo~$2^{n}$ is a
homomorphism from~$P_{m}$ onto~$P_{n}$ for $m \ge n$; and, for each
$a \in A_{n}$, the sequence $a*_{n} 0, a *_{n} 1, \dotsc $ is periodic
with period~$2^{k}$ for some $k \le n$ depending on~$a$.

The element~$0$ of~$P_{n}$ plays the role that the
identity embedding played at the end of Section~\ref{sec:2}: 
\begin{equation*}0*a=a,\quad a*0=0,\quad a\circ 0=0\circ a=a.
\end{equation*}
The element~$1$ is the generator of~$A_{n}$ and~$P_{n}$ (for $n > 0$).

Recall that $W_{\cala }$ and~$W_{\calp }$ are the
sets of words built up from~$1$ using~$\cdot $ and using~$\cdot ,\circ $,
respectively.  For $m > 0$, let $w_{m} \in W_{\cala }$ be the
product $1 \cdot 1 \cdot \ldots \cdot 1$ with $m$~$1$'s,
associated to the left as usual.  (In fact, it is often convenient to
just write~$m$ for~$w_{m}$ when the context makes this clear.  Note
that $w_{m}$~evaluates to~$m$ in~$A_{n}$ whenever $m < 2^{n}$.)
Also, let $u_{k} \in W_{\cala }$~be the product
$1 \cdot (1 \cdot \dots (1 \cdot 1)\dots )$
of $(k+1)$~$1$'s associated to the right.

The algebras~$A_{n}$ have a natural purely algebraic definition:
Wehrung~\cite{13} (see also Dr\'{a}pal~\cite{8})
showed that $A_{n}$~is the free algebra on one generator~$1$
subject to the left distributive law and the equation
$w_{2^{n}}\cdot 1 = 1$ (i.e., $w_{2^{n}+1} = 1$).
If $m$~is not a power of~$2$, then the free algebra
subject to~\eqref{tagld}  and the equation $w_{m}\cdot 1 = 1$ works out
to be~$A_{n}$, where $2^{n}$~is the largest power of~$2$ which
divides~$m$.

For every word $a\in W_{\calp }$ and every $n\geq 0$, let $[a]_{n}$ be the
value of $a$ in $P_{n}$.  Consider the equivalence relation $\equiv _{\infty }$
defined by: \begin{equation*}\text{$a \equiv _{\infty }b$ iff $[a]_{n}=[b]_{n}$ for all
$n\geq 0$.} \end{equation*} Let $A_{\infty }$ and $P_{\infty }$ be, respectively, the
quotients by $\equiv _{\infty }$ of $W_{\cala }$ and $W_{\calp }$.  Then $\cdot $
and~$\circ $ are well defined on the quotients, and $(A_{\infty },{\cdot })$
and~$(P_{\infty },{\cdot },{\circ })$ are generated by~$1$; also, they satisfy
\eqref{tagld}  and~\eqref{tagll}, respectively, because $A_{n}$ and~$P_{n}$ do.  (In fact,
an equivalent definition for $A_{\infty }$ and~$P_{\infty }$ is that they are
the subalgebras generated by~$1$ of the inverse limits of the algebras
$A_{n}$ and~$P_{n}$, respectively.)  Moreover, $A_{\infty }\subseteq P_{\infty }$.

\begin{theorem}\label{thm3.2}  The following are equivalent:
\begin{itemize}
\item[(i)]  $(A_{\infty },\cdot )$ is a free left-distributive algebra.
\item[(ii)]  $(P_{\infty },\cdot ,\circ )$ is a free\/ \eqref{tagll}-algebra.
\item[(iii)]  $<_{L}$ on $A_{\infty }$ is irreflexive.
\item[(iv)]  For every $a\in W_{\cala }$,
there is an $n$ such that $[a]_{n}\neq 0$.
\item[(v)]  For every $k\geq 1$, there is an $n$ such that $[1 \cdot w_{k}]_{n}\neq 0$.
\item[(vi)]  For every $k\geq 0$, there is an $n$ such that $[u_{k}]_{n}\neq 0$.
\item[(vii)]  For every $k\geq 0$, there is an $m > 0$ such that\/
\eqref{tagld}  together with the equation $w_{m} \cdot 1 = 1$ does\/ {\rm not}
imply the equation $u_{k} \cdot 1 = 1$.
\end{itemize}\end{theorem}


All steps of the proof can be formalized in Primitive Recursive Arithmetic,
so Theorem~\ref{thm3.2} is a theorem of PRA.

\section{Embedding algebras}\label{sec:4}

In this section, we consider algebras of increasing functions
from~$\natnum $ to~$\natnum $ which imitate the behavior of the algebra
of elementary embeddings from Laver~\cite{10} on ordinals.
The existence of such algebras turns out to be equivalent to the
properties in Theorem~\ref{thm3.2}. Moreover, this equivalence can be proved
(and formulated) in Primitive Recursive Arithmetic.

The algebras have the form~$(A,{\cdot })$, where $A$~is a collection of
strictly increasing functions from~$\natnum $ to~$\natnum $
and $\cdot $~is a binary operation on~$A$ (which we often denote
by juxtaposition).  The axioms for the algebra will include
the axiom~\eqref{tagld}.

Let $\id $ be the identity function on~$\natnum $.  If
$f\colon \natnum \to \natnum $ is strictly increasing and different
from~$\id $, let $\crit {f}$ be the least~$n$ such that $f(n)>n$ (the {\em critical point\/} of~$f$).  This is analogous to the
standard definition for nontrivial elementary embeddings
$j\colon V_{\lambda }\to V_{\lambda }$: the critical point
of~$j$ is the least ordinal moved by~$j$.

\begin{definition}\label{dfn4.1} An {\em embedding algebra}
is a structure~$(A,{\cdot })$, where $A$~is a collection of
strictly increasing functions from~$\natnum $ to~$\natnum $, ${\cdot }$~is a
left-distributive binary operation on $A$, 
and for every $a, b \in A$ with $b\neq \id $, $\crit {a\cdot b}=a(\crit {b})$.
\end{definition}


The set~$A$ need not contain the identity function, but one can extend
the operation~$\cdot $ to $A \cup \{\id \}$ in a natural way: $a\cdot \id =
\id $, $\id \cdot a = a$.  An embedding algebra is called {\em nontrivial\/}
if it has an element other than~$\id $.

We will also need to work with a more abstract and elaborate
form of embedding algebra, including much of the machinery
Laver constructs for algebras of elementary embeddings.

\begin{definition}\label{dfn4.2}
A {\em two-sorted embedding algebra} consists of a nonempty
set~$\E $ (the `embeddings,' for which we will use variables $a,b,\dotsc $) and
a nonempty set~$\Ord $ (the `ordinals,' for which we will use variables
$\alpha ,\beta ,\dotsc $), together with binary operations $\cdot $ and~$\circ $
on~$\E $, a binary relation~$\le $ on~$\Ord $, a constant $\id \in \E $, an
application
operation $a,\beta \mapsto a(\beta )$ (which will often be written
without parentheses) from $\E \times \Ord $ to~$\Ord $, a function
$\critfunc \colon \E {-}\{\id \} \to \Ord $, and a ternary relation ${\equiv }
\subseteq \E \times \Ord \times \E $, satisfying the following axioms:
\begin{itemize}
\item[$\bullet $] The relation~$\le $ is a linear ordering of~$\Ord $.
\nopagebreak \item[$\bullet $] Embeddings are strictly increasing monotone functions:
\begin{equation*}\beta < \gamma \quad \text{implies} \quad a\beta < a\gamma ,
\qquad \text{and} \qquad a\beta \ge \beta .\end{equation*}
\item[$\bullet $] For all $a \ne \id $, $a(\crit {a}) > \crit {a}$.
\item[$\bullet $] The operation~$\circ $ represents composition:
$(a\circ b)\gamma = a(b\gamma )$.
\item[$\bullet $] The constant~$\id $ represents the identity:
\begin{equation*}\id (\gamma ) = \gamma , \qquad a \cdot \id = \id , \qquad \text{and} \qquad \id \cdot a = a \circ \id = \id \circ a = a.\end{equation*}
\item[$\bullet $] The axioms~\eqref{tagll}  hold.
\item[$\bullet $] For each~$\gamma $, $\tLequiv {\gamma }$ is an equivalence
relation
on~$\E $ which respects $\cdot $ and~$\circ $; also, if $\gamma \le \delta $ and
$a \tLequiv {\delta } b$, then $a \tLequiv {\gamma } b$.
\item[$\bullet $] If $a \tLequiv {\gamma } b$ and $a\delta <\gamma $, then
$a\delta = b\delta $.
\item[$\bullet $] For any $a \ne \id $, $a \tLequiv {\crit {a}} \id $.
\item[$\bullet $] Coherence: $a \tLequiv {\gamma } b$ implies
$ca \tLequiv {c\gamma } cb$.
\end{itemize}\end{definition}


Again, such an algebra is called nontrivial if there is an embedding
other than~$\id $.  Note that the important ordinals are the
critical points, those ordinals
of the form~$\crit {a}$ for some embedding~$a$; if we simply
deleted all the other ordinals from~$\Ord $, we would still have
a two-sorted embedding algebra.

The results of Laver~\cite{10} show that one can make the set of all
elementary embeddings from~$V_{\lambda }$ to itself into a two-sorted
embedding algebra by letting $\Ord $ be the set of limit ordinals less
than~$\lambda $ and defining $\tLequiv {\gamma }$
to be Laver's $\overset {{\gamma }}{=}$.  Conversely, many of Laver's arguments
about elementary embeddings and their critical points use
only the properties of a two-sorted embedding algebra.

If desired, one can restrict $\E $ to the embeddings obtained from
a single embedding $j\ne \id $ using $\cdot $ and $\circ $
(along with~$\id $), to get a two-sorted
embedding algebra generated by a single embedding.  From now on,
we will call a two-sorted embedding algebra {\em monogenic} if its
embeddings are generated from a single non-identity embedding via
$\cdot $ and~$\circ $.

The main result of this paper is the following theorem.

\begin{theorem}\label{thm4.3}  The following are equivalent:
\begin{itemize}
\item[(i)]  $(A_{\infty },\cdot )$ is a free left-distributive algebra.
\item[(ii)]  There exists a nontrivial embedding algebra.
\item[(iii)]  There exists a nontrivial two-sorted embedding algebra
in which the ordinals have order type~$\omega $.
\end{itemize}\end{theorem}


In order to prove Theorem~\ref{thm4.3}, we need to perform a number of the
arguments of Laver~\cite{11} in the context of two-sorted
embedding algebras.
This is straightforward for arguments involving only the operations
which are built into these algebras, but some arguments use additional
features of elementary embeddings.  In particular, a few arguments
use ordinals of the form $\appless {a}{\gamma }$, defined to be the least ordinal
greater than $a(\beta )$ for all $\beta < \gamma $.  For this purpose,
we will define an even more elaborate algebra which includes this operation,
and
show that such algebras can be constructed from ordinary two-sorted
embedding algebras; this will allow us to use this new operation
to prove facts about the original algebra.

\begin{definition}\label{dfn4.4} An {\em extended two-sorted embedding algebra}
is a two-sorted embedding algebra (with embedding
set~$\E $ and ordinal set~$\Ord $), together with two new operations,
a cofinality function ${\cf }\colon \Ord \to \Ord $ and a mapping from
$\E \times \Ord $ to~$\Ord $ for which we use the notation $a,\gamma \mapsto \appless {a}{\gamma }$, satisfying the following additional axioms:
\begin{gather*}
a(\appless {b}{\gamma }) = \appless {ab}{a\gamma }; \\
\appless {a}{\appless {b}{\gamma }} = \appless {(a \circ b)}{\gamma }; \\
\appless {a}{\gamma }\le a\gamma ; \\
\text{if}\quad \gamma <\delta , \quad \text{then}\quad a\gamma <\appless {a}{\delta };\\
\text{if}\quad a \tLequiv {\gamma } b \quad \text{and}\quad \appless {a}{\delta }\le \gamma , \quad \text{then}\quad \appless {a}{\delta }= \appless {b}{\delta }; \\
\cf (\crit {a}) = \crit {a}; \\
\cf (\appless {a}{\gamma }) = \cf \gamma ; \\
\cf (a\gamma ) = a(\cf \gamma ); \\
\cf \gamma \le \gamma ; \\
\text{if}\quad a(\cf \gamma ) = \cf \gamma , \quad \text{then}\quad \appless {a}{\gamma }= a\gamma .
\end{gather*}
\end{definition}


Again it is not hard to verify that the axioms for an extended two-sorted
embedding algebra hold in the case where $\E $ is the set of elementary
embeddings on~$V_{\lambda }$ and $\Ord $ is the collection of limit ordinals less
than~$\lambda $~\cite{11}.  

The following is a crucial technical result:
 
\begin{theorem}\label{thm4.5} Suppose that we are given a two-sorted embedding
algebra, in which every ordinal is a critical point.
Then the algebra can be extended to a new two-sorted embedding algebra
with the same embedding set, on which the required additional operations
can be defined so as to give an extended two-sorted embedding algebra.
\end{theorem}


Theorem~\ref{thm4.5} can be used to transfer various arguments from the context
of elementary embeddings to that of two-sorted embedding algebras.
One example is the following result, which is proved by
following Laver's proof of Theorem~\ref{thm2.8}.

In a two-sorted embedding algebra, let $j \neq \id $ be some 
embedding, and let $A_{j}$ be the set of embeddings generated from~$j$
by the operation~$\cdot $ (so each $a \in A_{j}$ is given by
a word in~$W_{\cala }$ evaluated at~$j$).

\begin{theorem}\label{thm4.6} Assume that the set of all critical points
of elements of $A_{j}$ has order type~$\omega $.
If $a$ and~$b$ are distinct elements of~$A_{j}$, then there is
a critical point\/~$\gamma $ such that $a(\gamma ) \ne b(\gamma )$.
 \end{theorem}


We now outline the proof of Theorem~\ref{thm4.3}.
First, suppose that $A_{\infty }$~is free, and hence all of the
statements in Theorem~\ref{thm3.2} hold.  We build a two-sorted embedding
algebra with embedding set $\calp \cup \{\id \}$ and
ordinal set~$\natnum $, as follows.  For $a \in \calp $,
define $\crit {a}$ to be the least~$n$ such that
$[a]_{n+1} \ne 0$, or, equivalently, the largest~$n$ such that
$[a]_{n} = 0$.  Let $a(n) = \crit {a\cdot w_{2^{n}}}$, and
define $a \tLequiv {n} b$ to mean that $[a]_{n} = [b]_{n}$
(where we put $[\id ]_{n} = 0$).  Then one can prove from the
properties of the finite algebras~$A_{n}$ that these definitions
meet the requirements of a two-sorted embedding algebra.

Next, suppose we have a nontrivial two-sorted embedding algebra
in which the ordinals have order type~$\omega $.  We may take the
subalgebra~$A_{j}$ generated by some~$j \ne \nobreak \id $, and then
throw away all ordinals that are not critical points of members of~$A_{j}$.
The remaining ordinals still have order type~$\omega $,
so we can relabel them as the natural numbers.  By
Theorem~\ref{thm4.6}, distinct embeddings yield distinct functions
from~$\natnum $ to~$\natnum $; the resulting set of functions,
with the binary operation~$\cdot $ transferred from the set of embeddings,
forms an embedding algebra.

On the other hand, if we have a nontrivial embedding algebra, then we
can turn it into a two-sorted embedding algebra.  The set of ordinals
will be the set of critical points of the embeddings (which has
order type~$\omega $, since it is an infinite subset of~$\natnum $).
Proposition~\ref{prop2.5} lets us extend the set of embeddings to admit a
composition operation; the result of applying composite embeddings
$a\circ b$ to ordinals is defined by the obvious formula $(a \circ b)(n)
= a(b(n))$.  With more work, one can define suitable equivalence
relations~$\tLequiv {n}$ and show that all the axioms of a two-sorted
embedding algebra hold.

Finally, again assuming we have a nontrivial two-sorted embedding algebra
in which the ordinals have order type~$\omega $, we can imitate
the arguments of Laver~\cite{11} for constructing the finite
algebras in the first place, to show that statement~(iv)
of Theorem~\ref{thm3.2} is true, and hence $A_{\infty }$~is free.
The only part of this argument that cannot be carried out
in two-sorted embedding algebras is the proof of
the Laver-Steel result (Theorem~\ref{thm2.7} here), so we have made
this a hypothesis instead.  This completes the proof outline.

In the process of proving Theorem~\ref{thm4.3}, we also obtain the
following uniqueness result for monogenic embedding algebras.

\begin{theorem}\label{thm4.7} If\/ $(A,{\cdot })$ is a monogenic embedding
algebra for which every natural number is a critical point, then
$(A,{\cdot })$ is the embedding algebra constructed
from the algebras~$A_{n}$ as above.
\end{theorem}


Similarly, any monogenic two-sorted embedding algebra in which
the ordinals have order type~$\omega $ and are all critical points must
be isomorphic to the one constructed from the algebras~$A_{n}$.

\section{The strength of ``$A_{\infty }$ is free''}\label{sec:5}

Laver's proof of the irreflexivity of the free left distributive algebra
on one generator assumed the existence of a nontrivial elementary
embedding from~$V_{\lambda }$ to itself; this is an extremely strong large
cardinal hypothesis.  (Actually, Laver had noted that the assumption
can be reduced to the existence of an $n$-huge cardinal for each
natural number~$n$.)  The possibility that the irreflexivity property
was strong enough to require large cardinal assumptions for its proof
remained until Dehornoy proved the property without such assumptions
(in fact, using only Primitive Recursive Arithmetic).

We now consider the statement ``$A_{\infty }$~is free'' (and its equivalent
versions).  Laver~\cite{11} showed that this statement also
follows from the existence of a nontrivial elementary embedding $j \colon V_{\lambda }\to V_{\lambda }$.  (In fact, one might consider ``$A_{\infty }$~is
free'' to be the algebraic content of the set-theoretic Theorem~\ref{thm2.7}.)
Laver (personal communication) has noted, and the authors
have confirmed, that one can use the method of proof of Theorem~\ref{thm2.7}
while working with only an $n$-huge embedding, to get a correspondingly
weaker result; hence, the freeness of~$A_{\infty }$ follows from the
existence of an $n$-huge cardinal for each natural number~$n$.

However, unlike the irreflexivity of the free algebra, the
freeness of~$A_{\infty }$ cannot be proved without some
`strong' hypothesis:

\begin{theorem}\label{thm5.1} The statement ``$A_{\infty }$~is free'' is not
provable in Primitive Recursive Arithmetic. \end{theorem}


Of course, we assume throughout that PRA is itself consistent.

It is a well-known result from proof theory (see Sieg~\cite{12})
that the only recursive functions that can be proved to be total using
only~PRA are the primitive recursive functions.  Therefore, to prove
Theorem~\ref{thm5.1}, it will suffice to show that 
$\text{PRA}{+}$\ref{thm3.2}(vi) proves
the totality of a recursive function~$F$ which is not primitive recursive.

For each natural number~$n$, let $F(n)$ be the largest~$m$ such that
$[u_{n}]_{m} = 0$, where $u_{n}$ is the word
$1\cdot (1\cdot (\dots (1\cdot 1)\dots ))$ with $n+1$~$1$'s.  It
follows from~\ref{thm3.2}(vi) that $F$~is a total recursive function.

This function can be characterized in another way in terms of the
monogenic embedding algebra or two-sorted embedding algebra
constructed from the finite algebras.  Let $j$ be the
generating embedding, and let $\Gamma $ be the set of all
critical points of embeddings in the algebra.  Among these critical
points are a special sequence $\kappa _{0}<\kappa _{1}<\kappa _{2}<\dotsb $
called the {\em critical sequence} of~$j$: $\kappa _{0} = \crit {j}$
and $\kappa _{n+1} = j(\kappa _{n})$.  Then $F(n)$~is the number
of members of~$\Gamma $ lying below~$\kappa _{n}$.

The main result of Dougherty~\cite{5} shows that, in the context
of elementary embeddings from~$V_{\lambda }$ to~$V_{\lambda }$,
the function~$F$ defined as in the preceding paragraph
grows faster than the Ackermann function, and hence cannot be
primitive recursive.  However, the methods used in that proof
use only the properties of embeddings that follow immediately
from the axioms of an embedding algebra or two-sorted embedding algebra.
(In fact, all of
the proofs in Dougherty~\cite{5} can be carried out
in any extended two-sorted embedding algebra.)  Therefore,
the same growth estimates apply to the embedding algebra
constructed from the finite algebras, and this requires
only the assumption that $A_{\infty }$~is free.  Therefore,
this assumption is too strong to be proved in~PRA.

In a sense, the function~$F$ gives a measure of the
proof-theoretic strength of the statement ``$A_{\infty }$~is free.''
This can be stated precisely as follows.

\begin{proposition}\label{prop5.2} Any recursive function which is provably
total in\/ {\rm PRA${}+{}$}``$A_{\infty }$~is free'' must grow more slowly
than~$F_{m}$ for some~$m$, where $F_{0} = F$ and $F_{m+1}$~is the iteration
of~$F_{m}$ (starting at\/~$1$, say; that is, $F_{m+1}(n) = F_{m}^{n}(1)$).
\end{proposition}


There remain a number of open problems related to these algebras.
The main one, of course, is the exact strength of the statement
``$A_{\infty }$~is free''; the gap between ``more than PRA'' and
``there is an $n$-huge cardinal for each~$n$''
is rather large.  More recent results about the finite algebras~$A_{n}$
\cite{6}, \cite{8}, \cite{9} may be steps toward
a proof without large cardinals that $A_{\infty }$~is free,
but the full situation is not at all clear.


\bibliographystyle{amsplain}
\begin{thebibliography}{99}

\bibitem{1}
P. Dehornoy, {\em Sur la structure des gerbes libres}, C. R. Acad.
Sci. Paris S\'{e}r. I Math. {\bf 309} (1989), 143--148.
\MR{90j:20146}
\bibitem{2}
\bysame , {\em The adjoint representation of
left distributive structures}, Comm. Algebra {\bf 20} (1992), 1201--1215.
\MR{93a:20108} 
\bibitem{3}
\bysame , {\em Braid groups and left distributive
operations}, Trans. Amer. Math. Soc. {\bf 345} (1994), 115--150.
\MR{95a:08003}
\bibitem{4}
\bysame , {\em From large cardinals to braids via
distributive algebra}, J. Knot Theory Ramifications {\bf 4} (1995), 33--79.
\MR{96g:20056}
\bibitem{5}
R. Dougherty, {\em Critical points in an algebra of
elementary embeddings}, Ann. Pure Appl. Logic {\bf 65} (1993), 211--241.
\MR{95i:03117}
\bibitem{6}
\bysame , {\em Critical points in an algebra of
elementary embeddings, II}, Logic: from Foundations
to Applications (W. Hodges {\em et al.}, eds.), Clarendon, Oxford, 1996, pp.~103--136.
\CMP{97:06}
\bibitem{7}
R. Dougherty and T. Jech, {\em Finite left-distributive
algebras and embedding algebras}, Adv. Math. (to appear).
\bibitem{8}
A. Dr\'{a}pal, {\em Homomorphisms of primitive
left distributive groupoids}, Comm. Algebra {\bf 22\linebreak} (1994), 2579--2592.
\MR{95c:20107}
\bibitem{9}
\bysame , {\em Persistence of cyclic left distributive
algebras}, J. Pure Appl. Algebra {\bf 105} (1995), 137--165.
 \MR{96m:20113}
\bibitem{10}
R. Laver, {\em The left distributive law and the
freeness of an algebra of elementary embeddings}, Adv. Math. {\bf 91} (1992), 209--231.
\MR{93b:08008}
\bibitem{11}
\bysame , {\em On the algebra of elementary
embeddings of a rank into itself}, Adv. Math. {\bf 110} (1995), 334--346.
\MR{96c:03098}
\bibitem{12}
W. Sieg, {\em Fragments of arithmetic}, Ann.
Pure Appl. Logic {\bf 28} (1985), 33--71.
\MR{86g:03099}
\bibitem{13}
F. Wehrung, {\em Gerbes primitives}, C. R. Acad.
Sci. Paris S\'{e}r. I Math. {\bf 313} (1991), 357--362.
\MR{92i:08004}
\end{thebibliography}

\end{document}