{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:31Z","timestamp":1761596911112},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[1992,9,1]],"date-time":"1992-09-01T00:00:00Z","timestamp":715305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch Math Logic"],"published-print":{"date-parts":[[1992,9]]},"DOI":"10.1007\/bf01627504","type":"journal-article","created":{"date-parts":[[2005,5,8]],"date-time":"2005-05-08T16:54:18Z","timestamp":1115571258000},"page":"305-317","source":"Crossref","is-referenced-by-count":7,"title":["Remarks on Herbrand normal forms and Herbrand realizations"],"prefix":"10.1007","volume":"31","author":[{"given":"Ulrich","family":"Kohlenbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2140\/pjm.1979.84.1","volume":"84","author":"M.J. Beeson","year":"1979","unstructured":"[B] Beeson, M.J.: Goodman's theorem and beyond. Pac. J. Math.84, 1\u201316 (1979)","journal-title":"Pac. J. Math."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"574","DOI":"10.2307\/2272035","volume":"41","author":"N. Goodman","year":"1976","unstructured":"[G76] Goodman, N.: The theory of the G\u00f6del functionals. J. Symb. Logic41, 574\u2013582 (1976)","journal-title":"J. Symb. Logic"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"23","DOI":"10.2307\/2271946","volume":"43","author":"N. Goodman","year":"1978","unstructured":"[G78] Goodman, N.: Relativized realizability in intuitionistic arithmetic of all finite types. J. Symb. Logic43, 23\u201344 (1978)","journal-title":"J. Symb. Logic"},{"key":"CR4","volume-title":"Introduction to metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"[K1] Kleene, S.C.: Introduction to metamathematics. Amsterdam: North-Holland 1952"},{"key":"CR5","first-page":"241","volume":"16","author":"G. Kreisel","year":"1951","unstructured":"[Kr51, 52] Kreisel, G.: On the interpretation of non-finitist proofs, I and II. J. Symb. Logic16, 241\u2013267 (1951);17, 43\u201358 (1952)","journal-title":"J. Symb. Logic"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"103","DOI":"10.4064\/fm-39-1-103-127","volume":"39","author":"G. Kreisel","year":"1952","unstructured":"[Kr52a] Kreisel, G.: On the concepts of completeness and interpretation of formal systems. Fundam. Math.39, 103\u2013127 (1952).","journal-title":"Fundam. Math."},{"key":"CR7","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0049-237X(08)71876-7","volume-title":"Proc. of the Herbrand symposium (Marseille, 1981)","author":"G. Kreisel","year":"1982","unstructured":"[Kr82] Kreisel, G.: Finiteness theorems in arithmetic: an application of Herbrand's theorem for\u03a3 2-formulas. In: Stern, J. (ed.). Proc. of the Herbrand symposium (Marseille, 1981), pp. 39\u201355, Amsterdam: North-Holland 1982"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19680140702","volume":"14","author":"G. Kreisel","year":"1968","unstructured":"[Kr-L] Kreisel, G., Levy, A.: Reflection principles and their use for establishing the complexity of axiomatic systems. Z. Math. Logik Grundlagen Math.14, 97\u2013142 (1968)","journal-title":"Z. Math. Logik Grundlagen Math."},{"key":"CR9","series-title":"Lect. Notes Math.","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0060871","volume-title":"Extensional G\u00f6del functional interpretation. A consistency proof of classical analysis","author":"H. Luckhardt","year":"1973","unstructured":"[Lu73] Luckhardt, H.: Extensional G\u00f6del functional interpretation. A consistency proof of classical analysis. Lect. Notes Math. vol. 306. Berlin Heidelberg New York: Springer 1973"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"234","DOI":"10.2307\/2275028","volume":"54","author":"H. Luckhardt","year":"1989","unstructured":"[Lu89] Luckhardt, H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symb. Logic54, 234\u2013263 (1989)","journal-title":"J. Symb. Logic"},{"key":"CR11","first-page":"459","volume-title":"Intuitionism and Proof Theory","author":"C. Parsons","year":"1970","unstructured":"[P70] Parsons, C.: On a number-theoretic choice schema and its relation to induction. In: Kino, A., Myhill, J., Vessley, R.E. (eds.). Intuitionism and Proof Theory, pp. 459\u2013473. Amsterdam: North-Holland 1970"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1017\/S0022481200127069","volume":"36","author":"C. Parsons","year":"1971","unstructured":"[P71] Parsons, C.: On a number-theoretic choice schema II (abstract). J. Symb. Logic36, 587 (1971)","journal-title":"J. Symb. Logic"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"466","DOI":"10.2307\/2272731","volume":"37","author":"C. Parsons","year":"1972","unstructured":"[P72] Parsons, C.: Onn-quantifier-induction. J. Symb. Logic37, 466\u2013482 (1972)","journal-title":"J. Symb. Logic"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"867","DOI":"10.1016\/S0049-237X(08)71124-8","volume-title":"Handbook of mathematical Logic","author":"H. Schwichtenberg","year":"1977","unstructured":"[Sch] Schwichtenberg, H.: Proof theory: some applications of cut-elimination. In: Barwise, J. (ed.). Handbook of mathematical Logic, pp. 867\u2013895. Amsterdam: North-Holland 1977"},{"key":"CR15","volume-title":"Mathematical logic","author":"J.R. Shoenfield","year":"1967","unstructured":"[Sh] Shoenfield, J.R.: Mathematical logic. New York: Addison-Wesley 1967"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0168-0072(85)90030-2","volume":"28","author":"W. Sieg","year":"1985","unstructured":"[Si85] Sieg, W.: Fragments of arithmetic. Ann. Pure Appl. Logic28, 33\u201371 (1985)","journal-title":"Ann. Pure Appl. Logic"},{"key":"CR17","unstructured":"[Si87] Sieg, W.: Provably recursive functionals of theories with K\u00f6nig's lemma. Rend. Semin. Mat. Torino. Faxicolo speciale 75\u201392 (1987)"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF01621477","volume":"30","author":"W. Sieg","year":"1991","unstructured":"[Si91] Sieg, W.: Herbrand analyses. Arch. Math. Logic30, 409\u2013441 (1991)","journal-title":"Arch. Math. Logic"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1016\/S0049-237X(08)71689-6","volume-title":"Formal systems and recursive functions","author":"W.W. Tait","year":"1965","unstructured":"[Ta] Tait, W.W.: Infinitely long terms of transfinite type. In: Crossley, J.N., Dummett, M.A.E. (eds.). Formal systems and recursive functions, pp. 176\u2013185. Amsterdam: North-Holland 1965"},{"key":"CR20","series-title":"Lect. Notes Math.","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","volume-title":"Metamathematical investigation of intuitionistic arithmetic and analysis","author":"A. S. Troelstra","year":"1973","unstructured":"[Tr] Troelstra, A. S.: Metamathematical investigation of intuitionistic arithmetic and analysis. (Lect. Notes Math., vol. 344). Berlin Heidelberg New York: Springer 1973"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01627504.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01627504\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01627504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T05:34:22Z","timestamp":1683092062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01627504"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":20,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["BF01627504"],"URL":"https:\/\/doi.org\/10.1007\/bf01627504","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}