Extensions of Arithmetic For Proving Termination of Computations
Kent, Clement F. ; Hodgson, Bernard R.
J. Symbolic Logic, Tome 54 (1989) no. 1, p. 779-794 / Harvested from Project Euclid
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.
Publié le : 1989-09-14
Classification: 
@article{1183743017,
     author = {Kent, Clement F. and Hodgson, Bernard R.},
     title = {Extensions of Arithmetic For Proving Termination of Computations},
     journal = {J. Symbolic Logic},
     volume = {54},
     number = {1},
     year = {1989},
     pages = { 779-794},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183743017}
}
Kent, Clement F.; Hodgson, Bernard R. Extensions of Arithmetic For Proving Termination of Computations. J. Symbolic Logic, Tome 54 (1989) no. 1, pp.  779-794. http://gdmltest.u-ga.fr/item/1183743017/