Abstract

Kirby and Paris have exhibited combinatorial algorithms whose computations always terminate, but for which termination is not provable in elementary arithmetic. However, termination of these computations can be proved by adding an axiom first introduced by Goodstein in 1944. Our purpose is to investigate this axiom of Goodstein, and some of its variants, and to show that these are potentially adequate to prove termination of computations of a wide class of algorithms. We prove that many variations of Goodstein's axiom are equivalent, over elementary arithmetic, and contrast these results with those recently obtained for Kruskal's theorem