{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T12:58:35Z","timestamp":1705064315833},"reference-count":55,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5372,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[1998,11]]},"DOI":"10.1016\/s0168-0072(98)00020-7","type":"journal-article","created":{"date-parts":[[2003,4,23]],"date-time":"2003-04-23T15:00:04Z","timestamp":1051110004000},"page":"93-184","source":"Crossref","is-referenced-by-count":15,"title":["Some results on cut-elimination, provable well-orderings, induction and reflection"],"prefix":"10.1016","volume":"95","author":[{"given":"Toshiyasu","family":"Arai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(98)00020-7_BIB1","doi-asserted-by":"crossref","unstructured":"T. Arai, Variations on a theme by Weiermann, J. Symbol Logic, to appear.","DOI":"10.2307\/2586719"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB2","series-title":"The Lambda Calculus Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB3","article-title":"Separating fragments of bounded arithmetic","author":"Beckmann","year":"1996"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB4","article-title":"Foundations of Constructive Mathematics","volume":"Band 6","author":"Beeson","year":"1985"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB5","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/S0168-0072(96)00045-0","article-title":"Induction rules, reflection principles, and provably recursive functions","volume":"85","author":"Beklemishev","year":"1997","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB6","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0168-0072(94)00056-9","article-title":"Proof-theoretic analysis of termination proofs","volume":"75","author":"Buchholz","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s001530050079","article-title":"An intuitionistic fixed point theory","volume":"37","author":"Buchholz","year":"1997","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB8","article-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies","volume":"vol. 897","author":"Buchholz","year":"1981"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB9","series-title":"Bounded Arithmetic","author":"Buss","year":"1986"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB10","first-page":"1","article-title":"An application of boolean complexity to separation problems in bounded arithmetic","volume":"69","author":"Buss","year":"1994"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB11","series-title":"Proof Theory","first-page":"171","article-title":"Termination orderings and complexity characterizations","author":"Cichon","year":"1993"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB12","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0168-0072(96)00015-2","article-title":"Term rewriting theory for the primitive recursive functions","volume":"83","author":"Cichon","year":"1997","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB13","series-title":"Feasible Mathematics II","first-page":"154","article-title":"First order bounded arithmetic and small boolean circuit complexity classes","author":"Clote","year":"1995"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB14","first-page":"243","article-title":"Rewrite systems","volume":"vol. B","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB15","series-title":"Patras Logic Symp.","first-page":"171","article-title":"Iterated inductive fixed-point theories: Applications to Hancock's conjecture","author":"Feferman","year":"1982"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB16","doi-asserted-by":"crossref","first-page":"379","DOI":"10.2140\/pjm.1975.57.379","article-title":"Provably equality in primitive recursive arithmetic with and without induction","volume":"57","author":"Friedman","year":"1975","journal-title":"Pacific J. Math."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(94)00003-L","article-title":"Elementary descent recursion and proof theory","volume":"71","author":"Friedman","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB18","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/BF01564760","article-title":"Beweibarkeit und Unbeweisbarkeit von Anfangsf\u00e4llen der transfiniten Induktion in der reinen Zahlentheorie","volume":"119","author":"Gentzen","year":"1943","journal-title":"Math. Ann."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB19","series-title":"Logic and Algorithmic, an Internat. Symp. held in Honour of Ernst Specker","first-page":"207","article-title":"Proof-theoretic investigations of inductive definitions","author":"Girard","year":"1982"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB20","volume":"vol. 1","author":"Girard","year":"1987"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.2307\/2271946","article-title":"Relativized realizability in intuitionistic arithmetic of all finite types","volume":"43","author":"Goodman","year":"1978","journal-title":"J. Symbol. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB22","series-title":"Proc. 2nd, ALP","first-page":"347","article-title":"Termination proofs by multiset path orderings imply primitive recursive derivation lengths","volume":"vol. 463","author":"Hofbauer","year":"1990"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB23","doi-asserted-by":"crossref","first-page":"325","DOI":"10.2307\/2270450","article-title":"Transfinite induction and bar induction of type zero and one, and the role of continuity in intuitionistic analysis","volume":"31","author":"Howard","year":"1966","journal-title":"J. Symbol Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB24","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF01627506","article-title":"Bounds for cut elimination in intuitionistic propositional logic","volume":"31","author":"Hudelmaier","year":"1992","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB25","unstructured":"G. J\u00e4ger, R. Kahle, A. Setzer, T. Strahm, The proof-theoretic analysis of transfinitely iterated fixed point theories, submitted."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB26","doi-asserted-by":"crossref","first-page":"1108","DOI":"10.2307\/2275451","article-title":"About the proof-theoretic ordinals of weak fixed point theories","volume":"57","author":"J\u00e4ger","year":"1992","journal-title":"J. Symbol Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB27","unstructured":"G. J\u00e4ger, T. Strahm, Fixed point theories and dependent choice, submitted."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB28","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/BF01352935","article-title":"A note on sharply bounded arithmetic","volume":"33","author":"Johannsen","year":"1994","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB29","series-title":"Bounded arithmetic, propositional logic, and complexity theory","author":"Kraj\u00ed\u010dek","year":"1995"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB30","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1093\/bjps\/IV.14.107","article-title":"A variant to Hilbert's theory of foundations of arithmetic","volume":"4","author":"Kreisel","year":"1953","journal-title":"Brit. J. Phil. Sc."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB31","first-page":"390","article-title":"The status of the first \u03b5-number in first order arithmetic","volume":"25","author":"Kreisel","year":"1960","journal-title":"J. Symbol Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB32","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19680140702","article-title":"Reflection principles and their use for establishing the complexity of axiomatic systems","volume":"14","author":"Kreisel","year":"1968","journal-title":"Z. Math. Logik Grundlagen Math."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB33","series-title":"Selected Papers in Proof Theory","first-page":"17","article-title":"Finite investigations of transfinite derivations","author":"Mints","year":"1992"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB34","series-title":"Selected Papers in Proof Theory","first-page":"153","article-title":"Reflection and transfinite induction","author":"Mints","year":"1992"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB35","series-title":"Elementary Induction on Abstract Structures","author":"Moschovakis","year":"1974"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB36","series-title":"Proof Theory","first-page":"27","article-title":"A short course in ordinal analysis","author":"Pohlers","year":"1993"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB37","unstructured":"C. R\u00fcede, T. Strahm, Transfinitely iterated fixed point theories with intuitionistic logic, in preparation."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB38","first-page":"335","article-title":"A fine structure generated by reflection formulas over primitive recursive arithmetic","volume":"78","author":"Schmerl","year":"1979"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB39","series-title":"Proof Theory","author":"Sch\u00fctte","year":"1977"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB40","first-page":"867","article-title":"Proof theory: some applications of cut-elimination","author":"Schwichtenberg","year":"1977"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB41","series-title":"The Theory of Models","first-page":"342","article-title":"Non-standard models for fragments of number theory","author":"Shepherdson","year":"1965"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB42","first-page":"239","article-title":"\u03a311 and \u03a011 transfinite induction","volume":"80","author":"Simpson","year":"1982"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB43","first-page":"821","article-title":"The incompleteness theorems","author":"Smorynski","year":"1977"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB44","unstructured":"T. Strahm, Autonomous fixed point processes and transfinite fixed point recursion, in preparation."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB45","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0168-0072(95)00029-G","article-title":"Transfinite inducton within Peano arithmetic","volume":"76","author":"Sommer","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB46","first-page":"263","article-title":"A remark on Gentzen's paper \u201cBeweibarkeit und Unbeweisbarkeit von Anfangsf\u00e4llen der transfiniten Induktion in der reinen Zahlentheorie\u201d","volume":"39","author":"Takeuti","year":"1963"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB47","series-title":"Proof Theory","author":"Takeuti","year":"1987"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB48","series-title":"Arithmetic, Proof Theory and Computational Complexity","first-page":"364","article-title":"RSUV isomorphism","author":"Takeuti","year":"1993"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB49","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0168-0072(94)00008-Q","article-title":"Separations of theories in weak bounded arithmeic","volume":"71","author":"Takeuti","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB50","article-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","volume":"vol. 344","author":"Troelstra","year":"1973"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB51","volume":"vol. I","author":"Troelstra","year":"1988"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB52","series-title":"Proof Theory","first-page":"1","article-title":"Basic proof theory","author":"Wainer","year":"1993"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB53","series-title":"Bounding derivation lengths with functions from the slow growing hierarchy","author":"Weiermann","year":"1993"},{"key":"10.1016\/S0168-0072(98)00020-7_BIB54","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/0304-3975(94)00135-6","article-title":"Termination proofs by lexicographic path orderings imply multiply recursive derivation lengths","volume":"139","author":"Weiermann","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(98)00020-7_BIB55","unstructured":"A. Weiermann, Bounding derivation lengths with functions from the slow growing hierarchy, submitted."}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007298000207?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007298000207?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T06:55:26Z","timestamp":1555052126000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007298000207"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,11]]},"references-count":55,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[1998,11]]}},"alternative-id":["S0168007298000207"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(98)00020-7","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[1998,11]]}}}