{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T17:51:39Z","timestamp":1676483499445},"reference-count":13,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8958,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1989,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.2307\/2274742","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:31:33Z","timestamp":1146940293000},"page":"779-794","source":"Crossref","is-referenced-by-count":3,"title":["Extensions of arithmetic for proving termination of computations"],"prefix":"10.1017","volume":"54","author":[{"given":"Clement F.","family":"Kent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard R.","family":"Hodgson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200041517_ref008","doi-asserted-by":"crossref","unstructured":"Loebl M. and Matou\u0161ek J. , On undecidability of the weakened Kruskal theorem, in [Si87], pp. 275\u2013280.","DOI":"10.1090\/conm\/065\/891253"},{"key":"S0022481200041517_ref001","doi-asserted-by":"crossref","unstructured":"Buchholz W. and Wainer S. , Provably computable functions and the fast growing hierarchy, in [Si87], pp. 179\u2013198.","DOI":"10.1090\/conm\/065\/891248"},{"key":"S0022481200041517_ref009","volume-title":"Mathematical theory of computation","author":"Manna","year":"1974"},{"key":"S0022481200041517_ref011","volume-title":"An introduction to formal program verification","author":"Mili","year":"1985"},{"key":"S0022481200041517_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"S0022481200041517_ref006","first-page":"33","volume":"9","author":"Goodstein","year":"1944","journal-title":"On the restricted ordinal theorem"},{"key":"S0022481200041517_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"S0022481200041517_ref002","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1983-0687646-0"},{"key":"S0022481200041517_ref010","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611970388"},{"key":"S0022481200041517_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"S0022481200041517_ref007","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/14.4.285"},{"key":"S0022481200041517_ref013","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/065\/891258"},{"key":"S0022481200041517_ref005","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200041517","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:51:31Z","timestamp":1558281091000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200041517\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,9]]},"references-count":13,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,9]]}},"alternative-id":["S0022481200041517"],"URL":"https:\/\/doi.org\/10.2307\/2274742","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,9]]}}}