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)|
References found in this work BETA
No references found.
Citations of this work BETA
Analytic Combinatorics, Proof-Theoretic Ordinals, and Phase Transitions for Independence Results.Andreas Weiermann - 2005 - Annals of Pure and Applied Logic 136 (1):189-218.
Similar books and articles
Kolmogorov Complexity for Possibly Infinite Computations.Verónica Becher & Santiago Figueira - 2005 - Journal of Logic, Language and Information 14 (2):133-148.
The Strength of Nonstandard Methods in Arithmetic.C. Ward Henson, Matt Kaufmann & H. Jerome Keisler - 1984 - Journal of Symbolic Logic 49 (4):1039-1058.
Strong Termination for the Epsilon Substitution Method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (4):1193-1205.
How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem Almost to Robinson's Arithmetic Q.Dan E. Willard - 2002 - Journal of Symbolic Logic 67 (1):465-496.
Added to index2009-01-28
Total downloads21 ( #235,778 of 2,164,578 )
Recent downloads (6 months)1 ( #347,948 of 2,164,578 )
How can I increase my downloads?