{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T00:15:12Z","timestamp":1719533712143},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["UIDB\/04561\/2020","UIDB\/00408\/2020"],"award-info":[{"award-number":["UIDB\/04561\/2020","UIDB\/00408\/2020"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["UIDP\/00408\/2020","2022.12585.BD"],"award-info":[{"award-number":["UIDP\/00408\/2020","2022.12585.BD"]}]},{"name":"Universidade Aberta"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2024,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene\u2019s initial realizability laid the ground for more sophisticated notions such as Kreisel\u2019s modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion of realizability, namely <jats:italic>herbrandized modified realizability<\/jats:italic>. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed <jats:italic>star combinatory calculus<\/jats:italic>, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic.<\/jats:p>","DOI":"10.1007\/s00153-024-00917-6","type":"journal-article","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T20:18:00Z","timestamp":1712261880000},"page":"703-721","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Herbrandized modified realizability"],"prefix":"10.1007","volume":"63","author":[{"given":"Gilda","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Paulo","family":"Firmino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"issue":"4","key":"917_CR1","doi-asserted-by":"publisher","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. Symbol. Log. 74(4), 1100\u20131120 (2009)","journal-title":"J. Symbol. Log."},{"key":"917_CR2","unstructured":"Borges, A.: On the herbrandized interpretation for nonstandard arithmetic. Master\u2019s thesis, Universidade de Lisboa (2016)"},{"key":"917_CR3","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1142\/9789811245220_0010","volume-title":"Mathematics for Computation (M4C)","author":"J Enes","year":"2023","unstructured":"Enes, J., Ferreira, F.: Chapter 10: a herbrandized interpretation of semi-intuitionistic second-order arithmetic with function variables. In: Bebini, M., Beyersdorff, O., Rathjen, M., Schuster, P. (eds.) Mathematics for Computation (M4C), pp. 251\u2013271. World Scientific, Hackensack (2023)"},{"issue":"9","key":"917_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2020.102843","volume":"171","author":"F Ferreira","year":"2020","unstructured":"Ferreira, F.: The FAN principle and weak K\u00f6nig\u2019s lemma in herbrandized second-order arithmetic. Ann. Pure Appl. Log. 171(9), 102843 (2020)","journal-title":"Ann. Pure Appl. Log."},{"issue":"3","key":"917_CR5","doi-asserted-by":"publisher","first-page":"399","DOI":"10.4171\/pm\/2056","volume":"77","author":"F Ferreira","year":"2020","unstructured":"Ferreira, F.: Weak K\u00f6nig\u2019s lemma in herbrandized classical second-order arithmetic. Port. Math. 77(3), 399\u2013408 (2020)","journal-title":"Port. Math."},{"key":"917_CR6","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/s00153-017-0555-6","volume":"56","author":"F Ferreira","year":"2017","unstructured":"Ferreira, F., Ferreira, G.: A herbrandized functional interpretation of classical first-order logic. Arch. Math. Log. 56, 523\u2013539 (2017)","journal-title":"Arch. Math. Log."},{"key":"917_CR7","doi-asserted-by":"publisher","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":"917_CR8","doi-asserted-by":"publisher","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."},{"issue":"1","key":"917_CR9","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1002\/malq.200810029","volume":"56","author":"G Ferreira","year":"2010","unstructured":"Ferreira, G., Oliva, P.: Confined modified realizability. Math. Log. Q. 56(1), 13\u201328 (2010)","journal-title":"Math. Log. Q."},{"key":"917_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"SC Kleene","year":"1945","unstructured":"Kleene, S.C.: On the interpretation of intuitionistic number theory. J. Symbol. Log. 10, 109\u2013124 (1945)","journal-title":"J. Symbol. Log."},{"key":"917_CR11","series-title":"European Logic Colloquium","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1093\/oso\/9780198538622.003.0010","volume-title":"Logic: From Foundations to applications","author":"U Kohlenbach","year":"1996","unstructured":"Kohlenbach, U.: Analysing proofs in analysis. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: From Foundations to applications. European Logic Colloquium, pp. 225\u2013260. Oxford University Press, Oxford (1996)"},{"key":"917_CR12","doi-asserted-by":"publisher","first-page":"139","DOI":"10.2307\/2964110","volume":"27","author":"G Kreisel","year":"1962","unstructured":"Kreisel, G.: On weak completeness of intuitionistic predicate logic. J. Symbol. Log. 27, 139\u2013158 (1962)","journal-title":"J. Symbol. Log."},{"key":"917_CR13","unstructured":"Pinto, P.: Proof mining with the bounded functional interpretation. Ph.D. thesis, Universidade de Lisboa (2019)"},{"key":"917_CR14","doi-asserted-by":"publisher","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. Symbol. Log. 32, 198\u2013212 (1967)","journal-title":"J. Symbol. Log."},{"key":"917_CR15","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973)","DOI":"10.1007\/BFb0066739"},{"key":"917_CR16","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":"917_CR17","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in mathematics. In: An Introduction (Volume II). Studies in Logic and the Foundations of Mathematics, vol. 123. Amsterdam (1988)"},{"issue":"12","key":"917_CR18","doi-asserted-by":"publisher","first-page":"1962","DOI":"10.1016\/j.apal.2012.07.003","volume":"163","author":"B van den Berg","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":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00917-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-024-00917-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-024-00917-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,27]],"date-time":"2024-06-27T05:03:18Z","timestamp":1719464598000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-024-00917-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,4]]},"references-count":18,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2024,7]]}},"alternative-id":["917"],"URL":"https:\/\/doi.org\/10.1007\/s00153-024-00917-6","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,4]]},"assertion":[{"value":"7 November 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}