[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 
Originator: E. A. Cichon [Cic90]
Date: April 1991
Summary: Must any termination ordering used for proving termination of the Battle of Hydra and Herculessystem have the Howard ordinal as its order type?
The following system [DJ90], based on the “Battle of Hydra and Hercules” in [KP82], is terminating, but not provably so in Peano Arithmetic:

Transfinite (є_{0}) induction is required for a proof of termination. Must any termination ordering have the Howard ordinal as its order type, as conjectured in [Cic90]?
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 HowardBachmann 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].
This has been answered to the negative by Georg Moser [Mos09], by giving a reduction order that is compatible with the above rewrite system, and whose order type is at most є_{0} (the proof theoretic ordinal of Peano arithmetic).
[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 