{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,3]],"date-time":"2022-08-03T04:39:30Z","timestamp":1659501570242},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2017,9,19]],"date-time":"2017-09-19T00:00:00Z","timestamp":1505779200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s00153-017-0590-3","type":"journal-article","created":{"date-parts":[[2017,9,19]],"date-time":"2017-09-19T12:18:38Z","timestamp":1505823518000},"page":"497-531","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Epsilon substitution for $$\\textit{ID}_1$$ ID 1 via cut-elimination"],"prefix":"10.1007","volume":"57","author":[{"given":"Henry","family":"Towsner","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,19]]},"reference":[{"key":"590_CR1","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/BF01450016","volume":"117","author":"W Ackermann","year":"1940","unstructured":"Ackermann, W.: Zur Widerspruchsfreiheit der Zahlentheorie. Math. Ann. 117, 162\u2013194 (1940)","journal-title":"Math. Ann."},{"key":"590_CR2","unstructured":"Arai, T.: Proof theory for theories of ordinals. Preprints, 1996\u20131997"},{"key":"590_CR3","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s001530100108","volume":"41","author":"T Arai","year":"2002","unstructured":"Arai, T.: Epsilon substitution method for theories of jump hierarchies. Arch. Math. Log. 41, 123\u2013153 (2002)","journal-title":"Arch. Math. Log."},{"issue":"2","key":"590_CR4","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/S0168-0072(02)00112-4","volume":"121","author":"T Arai","year":"2003","unstructured":"Arai, T.: Epsilon substitution method for $${ID_1(\\Pi ^0_1\\vee \\Sigma ^0_1)}$$ I D 1 ( \u03a0 1 0 \u2228 \u03a3 1 0 ) . Ann. Pure Appl. Log. 121(2), 163\u2013208 (2003)","journal-title":"Ann. Pure Appl. Log."},{"issue":"1\u20133","key":"590_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0168-0072(03)00020-4","volume":"122","author":"T Arai","year":"2003","unstructured":"Arai, T.: Proof theory for theories of ordinals. I. Recursively Mahlo ordinals. Ann. Pure Appl. Log. 122(1\u20133), 1\u201385 (2003)","journal-title":"Ann. Pure Appl. Log."},{"issue":"1\u20133","key":"590_CR6","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.apal.2004.01.001","volume":"129","author":"T Arai","year":"2004","unstructured":"Arai, T.: Proof theory for theories of ordinals. II. $$\\Pi _3$$ \u03a0 3 -reflection. Ann. Pure Appl. Log. 129(1\u20133), 39\u201392 (2004)","journal-title":"Ann. Pure Appl. Log."},{"issue":"4","key":"590_CR7","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.2178\/jsl\/1164060450","volume":"71","author":"T Arai","year":"2006","unstructured":"Arai, T.: Epsilon substitution method for $$\\Pi _2^0$$ \u03a0 2 0 -FIX. J. Symb. Log. 71(4), 1155\u20131188 (2006)","journal-title":"J. Symb. Log."},{"key":"590_CR8","first-page":"115","volume":"95","author":"H Bachmann","year":"1950","unstructured":"Bachmann, H.: Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljschr. Naturforsch. Ges. Z\u00fcrich 95, 115\u2013147 (1950)","journal-title":"Vierteljschr. Naturforsch. Ges. Z\u00fcrich"},{"key":"590_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0091894","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies Volume 897 of Lecture Notes in Mathematics","author":"W Buchholz","year":"1981","unstructured":"Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies Volume 897 of Lecture Notes in Mathematics. Springer, Berlin (1981)"},{"issue":"1","key":"590_CR10","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G Gentzen","year":"1936","unstructured":"Gentzen, G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112(1), 493\u2013565 (1936)","journal-title":"Math. Ann."},{"key":"590_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86896-2","volume-title":"Grundlagen der Mathematik","author":"D Hilbert","year":"1970","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik, vol. 2. Springer, Berlin (1970)"},{"key":"590_CR12","doi-asserted-by":"crossref","first-page":"355","DOI":"10.2307\/2272979","volume":"37","author":"WA Howard","year":"1972","unstructured":"Howard, W.A.: A system of abstract constructive ordinals. J. Symb. Log. 37, 355\u2013374 (1972)","journal-title":"J. Symb. Log."},{"key":"590_CR13","volume-title":"Theories for Admissible Sets: A Unifying Approach to Proof Theory, Volume 2 of Studies in Proof Theory. Lecture Notes","author":"G J\u00e4ger","year":"1986","unstructured":"J\u00e4ger, G.: Theories for Admissible Sets: A Unifying Approach to Proof Theory, Volume 2 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples (1986)"},{"key":"590_CR14","doi-asserted-by":"crossref","unstructured":"Mints, G.: Gentzen-type systems and Hilbert\u2019s epsilon substitution method. In: Prawitz, D., Skyrms, B., Westerst\u00e5hl, D. (eds.) Logic, Method and Philosophy of Science, vol. IX, pp. 91\u2013122. Elsevier, Amsterdam (1994)","DOI":"10.1016\/S0049-237X(06)80040-6"},{"key":"590_CR15","doi-asserted-by":"crossref","unstructured":"Mints, G.: Non-deterministic epsilon substitution for $$ID_1$$ I D 1 : effective proof. In: Berger, U., Diener, H., Schuster, P., Seisenberger, M. (eds.) Logic, Construction, Computation, Volume 3 of Ontos Mathematical Logic, pp. 325\u2013342. Ontos Verlag, Heusenstamm (2012)","DOI":"10.1515\/9783110324921.325"},{"key":"590_CR16","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-319-10103-3_17","volume-title":"Gentzen\u2019s Centenary: The Quest for Consistency","author":"G Mints","year":"2015","unstructured":"Mints, G.: Non-deterministic epsilon substitution method for $${ PA}$$ P A and $${ ID}_1$$ I D 1 . In: Kahle, R., Rathjen, M. (eds.) Gentzen\u2019s Centenary: The Quest for Consistency, pp. 479\u2013500. Springer, Berlin (2015)"},{"key":"590_CR17","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-94-017-2109-7_8","volume-title":"Logic and Foundations of Mathematics","author":"G Mints","year":"1999","unstructured":"Mints, G., Tupailo, S.: Epsilon-substitution for the ramified language and $$\\Delta _1^1$$ \u0394 1 1 -comprehension rule. In: Cantinia, A., et al. (eds.) Logic and Foundations of Mathematics, pp. 107\u2013130. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"590_CR18","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/BF01273688","volume":"35","author":"G Mints","year":"1996","unstructured":"Mints, G., Tupailo, S., Buchholz, W.: Epsilon substitution method for elementary analysis. Arch. Math. Log. 35, 103\u2013130 (1996)","journal-title":"Arch. Math. Log."},{"issue":"3\u20134","key":"590_CR19","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF02011638","volume":"21","author":"W Pohlers","year":"1981","unstructured":"Pohlers, W.: Cut elimination for impredicative infinitary systems. I. Ordinal analysis for $${\\rm ID}_{1}$$ ID 1 . Arch. Math. Logik Grundlag. 21(3\u20134), 113\u2013129 (1981)","journal-title":"Arch. Math. Logik Grundlag."},{"key":"590_CR20","volume-title":"Proof Theory: The First Step into Impredicativity. Universitext","author":"W Pohlers","year":"2009","unstructured":"Pohlers, W.: Proof Theory: The First Step into Impredicativity. Universitext. Springer, Berlin (2009)"},{"issue":"5\u20136","key":"590_CR21","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/BF01621475","volume":"30","author":"M Rathjen","year":"1991","unstructured":"Rathjen, M.: Proof-theoretic analysis of $${\\bf KPM}$$ KPM . Arch. Math. Log. 30(5\u20136), 377\u2013403 (1991)","journal-title":"Arch. Math. Log."},{"issue":"4","key":"590_CR22","doi-asserted-by":"crossref","first-page":"468","DOI":"10.2307\/421132","volume":"1","author":"M Rathjen","year":"1995","unstructured":"Rathjen, M.: Recent advances in ordinal analysis: $$\\Pi ^1_2$$ \u03a0 2 1 - $${\\rm CA}$$ CA and related systems. Bull. Symb. Log. 1(4), 468\u2013485 (1995)","journal-title":"Bull. Symb. Log."},{"issue":"3","key":"590_CR23","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s00153-004-0232-4","volume":"44","author":"M Rathjen","year":"2005","unstructured":"Rathjen, M.: An ordinal analysis of parameter free $$\\Pi ^1_2$$ \u03a0 2 1 -comprehension. Arch. Math. Log. 44(3), 263\u2013362 (2005)","journal-title":"Arch. Math. Log."},{"issue":"1","key":"590_CR24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00153-004-0226-2","volume":"44","author":"M Rathjen","year":"2005","unstructured":"Rathjen, M.: An ordinal analysis of stability. Arch. Math. Log. 44(1), 1\u201362 (2005)","journal-title":"Arch. Math. Log."},{"key":"590_CR25","unstructured":"Rathjen, M.: Investigations of subsystems of second order arithmetic and set theory in strength between $$\\Pi _1^1\\text{-CA}$$ \u03a0 1 1 -CA and $$\\Delta ^1_2\\text{-CA }+{\\rm BI}$$ \u0394 2 1 -CA + BI : part I. In: Schindler, R. (ed.) Ways of Proof Theory, Volume 2 of Ontos Mathematical Logic, pp. 363\u2013439. Ontos Verlag, Heusenstamm (2010)"},{"key":"590_CR26","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511581007","volume-title":"Subsystems of Second Order Arithmetic. Perspectives in Logic","author":"SG Simpson","year":"2009","unstructured":"Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn. Cambridge University Press, Cambridge (2009)","edition":"2"},{"key":"590_CR27","doi-asserted-by":"crossref","first-page":"299","DOI":"10.2307\/1970691","volume":"86","author":"G Takeuti","year":"1967","unstructured":"Takeuti, G.: Consistency proofs of subsystems of classical analysis. Ann. Math. 86, 299\u2013348 (1967)","journal-title":"Ann. Math."},{"issue":"4","key":"590_CR28","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s00153-004-0241-3","volume":"44","author":"H Towsner","year":"2005","unstructured":"Towsner, H.: Epsilon substitution for transfinite induction. Arch. Math. Log. 44(4), 397\u2013412 (2005)","journal-title":"Arch. Math. Log."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-017-0590-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-017-0590-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-017-0590-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,3]],"date-time":"2022-08-03T00:51:45Z","timestamp":1659487905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-017-0590-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,19]]},"references-count":28,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["590"],"URL":"https:\/\/doi.org\/10.1007\/s00153-017-0590-3","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,19]]}}}