Extensions of arithmetic for proving termination of computations

Journal of Symbolic Logic 54 (3):779-794 (1989)
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2274742
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,349
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles
Added to PP index

Total downloads
24 ( #216,351 of 2,193,673 )

Recent downloads (6 months)
3 ( #95,976 of 2,193,673 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature