{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T11:29:58Z","timestamp":1777548598451,"version":"3.51.4"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2017,5,19]],"date-time":"2017-05-19T00:00:00Z","timestamp":1495152000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["SFRH\/BPD\/93278\/2013"],"award-info":[{"award-number":["SFRH\/BPD\/93278\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s00153-017-0555-6","type":"journal-article","created":{"date-parts":[[2017,5,18]],"date-time":"2017-05-18T23:40:40Z","timestamp":1495150840000},"page":"523-539","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A herbrandized functional interpretation of classical first-order logic"],"prefix":"10.1007","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8693-7210","authenticated-orcid":false,"given":"Fernando","family":"Ferreira","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1447-9764","authenticated-orcid":false,"given":"Gilda","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,19]]},"reference":[{"key":"555_CR1","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/S0049-237X(98)80020-7","volume-title":"Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics","author":"J Avigad","year":"1998","unstructured":"Avigad, J., Feferman, S.: G\u00f6del\u2019s functional (\u201cDialectica\u201d) interpretation. In: Buss, S.R. (ed.) Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, pp. 337\u2013405. North Holland, Amsterdam (1998)"},{"issue":"4","key":"555_CR2","doi-asserted-by":"crossref","first-page":"1100","DOI":"10.2178\/jsl\/1254748682","volume":"74","author":"J Avigad","year":"2009","unstructured":"Avigad, J., Towsner, H.: Functional interpretation and inductive definitions. J. Symb. Log. 74(4), 1100\u20131120 (2009)","journal-title":"J. Symb. Log."},{"key":"555_CR3","unstructured":"Borges, A.: On the herbrandised interpretation for nonstandard arithmetic. Master\u2019s thesis, Universidade de Lisboa (2016)"},{"key":"555_CR4","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0168-0072(01)00074-4","volume":"114","author":"J Diller","year":"2002","unstructured":"Diller, J.: Logical problems of functional interpretations. Ann. Pure Appl. Log. 114, 27\u201342 (2002)","journal-title":"Ann. Pure Appl. Log."},{"key":"555_CR5","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/BF02025118","volume":"16","author":"J Diller","year":"1974","unstructured":"Diller, J., Nahm, W.: Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archive f\u00fcr mathematische Logik und Grundlagenforschung 16, 49\u201366 (1974)","journal-title":"Archive f\u00fcr mathematische Logik und Grundlagenforschung"},{"key":"555_CR6","doi-asserted-by":"crossref","first-page":"329","DOI":"10.2178\/jsl\/1140641178","volume":"71","author":"F Ferreira","year":"2006","unstructured":"Ferreira, F., Nunes, A.: Bounded modified realizability. J. Symb. Log. 71, 329\u2013346 (2006)","journal-title":"J. Symb. Log."},{"key":"555_CR7","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.apal.2004.11.001","volume":"135","author":"F Ferreira","year":"2005","unstructured":"Ferreira, F., Oliva, P.: Bounded functional interpretation. Ann. Pure Appl. Log. 135, 73\u2013112 (2005)","journal-title":"Ann. Pure Appl. Log."},{"key":"555_CR8","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1007\/s00153-005-0275-1","volume":"44","author":"P Gerhardy","year":"2005","unstructured":"Gerhardy, P., Kohlenbach, U.: Extracting Herbrand disjunctions by functional interpretation. Arch. Math. Log. 44, 633\u2013644 (2005)","journal-title":"Arch. Math. Log."},{"key":"555_CR9","unstructured":"G\u00f6del, K.: \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. dialectica 12, 280\u2013287 (1958). Reprinted with an English translation in [10], pp. 240\u2013251"},{"key":"555_CR10","unstructured":"G\u00f6del, K.: On a hitherto unutilized extension of the finitary standpoint. In: Feferman, S., et al. (eds.) Collected Works, vol. II. Oxford University Press, Oxford (1990)"},{"key":"555_CR11","unstructured":"Shoenfield, J.R.: Mathematical Logic. Addison-Wesley Publishing Company, Boston (1967). Republished in 2001 by AK Peters"},{"issue":"1","key":"555_CR12","first-page":"104","volume":"75","author":"R Statman","year":"1979","unstructured":"Statman, R.: Lower bounds on Herbrand\u2019s theorem. Proc. Am. Math. Soc. 75(1), 104\u2013107 (1979)","journal-title":"Proc. Am. Math. Soc."},{"key":"555_CR13","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W Tait","year":"1967","unstructured":"Tait, W.: Intentional interpretations of functionals of finite type I. J. Symb. Log. 32, 198\u2013212 (1967)","journal-title":"J. Symb. Log."},{"key":"555_CR14","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996)"},{"key":"555_CR15","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics","year":"1973","unstructured":"Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973)"},{"issue":"12","key":"555_CR16","doi-asserted-by":"crossref","first-page":"1962","DOI":"10.1016\/j.apal.2012.07.003","volume":"163","author":"B Berg van den","year":"2012","unstructured":"van den Berg, B., Briseid, E., Safarik, P.: A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Log. 163(12), 1962\u20131994 (2012)","journal-title":"Ann. Pure Appl. Log."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-017-0555-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-017-0555-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-017-0555-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T01:29:11Z","timestamp":1501723751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-017-0555-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,19]]},"references-count":16,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["555"],"URL":"https:\/\/doi.org\/10.1007\/s00153-017-0555-6","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,19]]}}}