\documentclass{rtaloop}
\rtalabel{hydra}

\begin{document}
\begin{solvedproblem}{E. A. Cichon}{\cite{C90:london}}{April 1991}

\begin{abstract}
Must any termination {\em ordering\/} used for proving termination of the
\emph{Battle of Hydra and Hercules}-system have the Howard ordinal as its
order type?
\end{abstract}

The following system \cite{DJ90:htcs}, based on the
``Battle of Hydra and Hercules'' in \cite{KP82:lms},
is terminating, but not provably so in Peano Arithmetic:
\begin{eqnarray*}
h(z,e(x)) & \rightarrow & h(c(z),d(z,x))\\
d(z,g(0,0)) & \rightarrow & e(0)\\
d(z,g(x,y)) & \rightarrow & g(e(x),d(z,y))\\
d(c(z),g(g(x,y),0)) & \rightarrow & g(d(c(z),g(x,y)),d(z,g(x,y)))\\
g(e(x),e(y)) & \rightarrow & e(g(x,y))
\end{eqnarray*}
Transfinite ($\epsilon_0$-) induction is required for a proof of termination.
Must any termination {\em ordering\/} have the Howard ordinal as its order
type, as conjectured in \cite{C90:london}?


\begin{remark}
  If the notion of termination ordering is formalized by using ordinal
  notations with variables, then a termination proof using such
  orderings yields a slow growing bound on the lengths of derivations.
  If the order type is less than the Howard-Bachmann ordinal then, by
  Girard's Hierarchy Theorem, the derivation lengths are provably
  total in Peano Arithmetic.  Hence a termination proof for this
  particular rewrite system for the Hydra game cannot be given by such
  an ordering [Andreas Weiermann, personal communication].
\end{remark}

\begin{remark}
  This has been answered to the negative by Georg
  Moser~\cite{moser:aaecc2009}, by giving a reduction order that is
  compatible with the above rewrite system, and whose order type is at
  most $\epsilon_0$ (the proof theoretic ordinal of Peano arithmetic).
\end{remark}



\end{solvedproblem}
\end{document}