Abstract

Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano (1889) arithmetic. We present an encoding of Goodstein’s theorem as a termination problem of a finite rewrite system. Using a novel implementation of algebras based on ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by Touzet (1998) of the battle of Hercules and Hydra as well as a (corrected) encoding by Beklemishev (2006) of the Worm battle, two further systems which have been out of reach for automatic tools, until now. Based on our ideas of implementing ordinal algebras we also present a new approach for the automation of elementary interpretations for termination analysis.

BibTeX

@article{HZSWAM-JSC15,
  author    = "Harald Zankl and Sarah Winkler and Aart Middeldorp",
  title     = "Beyond Polynomials and {P}eano Arithmetic -- Automation of
               Elementary and Ordinal Interpretations",
  journal   = "Journal of Symbolic Computation",
  volume    = 69,
  pages     = "129--158",
  year      = 2015,
  doi       = "110.1016/j.jsc.2014.09.033"
}