{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T03:34:35Z","timestamp":1648870475249},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2013,10,25]],"date-time":"2013-10-25T00:00:00Z","timestamp":1382659200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2014,12]]},"abstract":"<jats:p>We introduce a realizability semantics based on interactive learning for full second-order Heyting arithmetic with excluded middle and Skolem axioms over \u03a3<jats:sub>1<\/jats:sub><jats:sup>0<\/jats:sup>-formulas. Realizers are written in a classical version of Girard's System<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000455_inline1\" \/><jats:tex-math>$\\mathsf{F}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>and can be viewed as programs that learn by interacting with the environment. We show that the realizers of any \u03a0<jats:sub>2<\/jats:sub><jats:sup>0<\/jats:sup>-formula represent terminating learning processes whose outcomes are numerical witnesses for the existential quantifier of the formula.<\/jats:p>","DOI":"10.1017\/s0960129513000455","type":"journal-article","created":{"date-parts":[[2013,10,25]],"date-time":"2013-10-25T13:26:38Z","timestamp":1382707598000},"source":"Crossref","is-referenced-by-count":1,"title":["Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1"],"prefix":"10.1017","volume":"24","author":[{"given":"FEDERICO","family":"ASCHIERI","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,10,25]]},"reference":[{"key":"S0960129513000455_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2275524"},{"key":"S0960129513000455_ref27","first-page":"207","article-title":"On Krivine Realizability Interpretation of Second-Order Classical Arithmetic.","volume":"84","author":"Oliva","year":"2008","journal-title":"Fundamenta Informaticae"},{"key":"S0960129513000455_ref22","first-page":"101","volume-title":"Constructivity in Mathematics","author":"Kreisel","year":"1959"},{"key":"S0960129513000455_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.12.004"},{"key":"S0960129513000455_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772068"},{"key":"S0960129513000455_ref28","volume-title":"Basic Proof Theory","author":"Schwichtenberg","year":"1996"},{"key":"S0960129513000455_ref20","volume-title":"Applied Proof Theory","author":"Kohlenbach","year":"2008"},{"key":"S0960129513000455_ref11","doi-asserted-by":"publisher","DOI":"10.2307\/2586854"},{"key":"S0960129513000455_ref1","unstructured":"Aschieri F. (2011a) Learning, Realizability and Games in Classical Arithmetic, Ph.D. Thesis, Queen Mary, University of London and University of Turin. (Available at http:\/\/arxiv.org\/abs\/1012.4992."},{"key":"S0960129513000455_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_17"},{"key":"S0960129513000455_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_15"},{"key":"S0960129513000455_ref2","first-page":"20","volume-title":"Computer Science Logic (CSL'11) \u2013 25th International Workshop\/20th Annual Conference of the EACSL","volume":"12","author":"Aschieri","year":"2011"},{"key":"S0960129513000455_ref13","unstructured":"Coquand T. (1991) A Semantics of Evidence for Classical Arithmetic. In: Informal Proceedings of the Second Workshop on Logical Frameworks 87\u201399."},{"key":"S0960129513000455_ref21","first-page":"241","article-title":"On the interpretation of non-finitist proofs, part I.","volume":"16","author":"Kreisel","year":"1951","journal-title":"Journal of Symbolic Logic"},{"key":"S0960129513000455_ref7","first-page":"57","volume-title":"Logic Colloquium '98","author":"Avigad","year":"2000"},{"key":"S0960129513000455_ref12","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:3)2005"},{"key":"S0960129513000455_ref18","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129513000455_ref8","doi-asserted-by":"publisher","DOI":"10.1002\/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6"},{"key":"S0960129513000455_ref32","volume-title":"Constructivism in Mathematics, vol. I","author":"Troelstra","year":"1988"},{"key":"S0960129513000455_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01273688"},{"key":"S0960129513000455_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2012.05.002"},{"key":"S0960129513000455_ref29","volume-title":"Lectures on the Curry\u2013Howard isomorphism","author":"Sorensen","year":"2006"},{"key":"S0960129513000455_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"S0960129513000455_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S0960129513000455_ref30","first-page":"1","volume-title":"Recursive Function Theory: Proceedings of Symposia in Pure Mathematics","author":"Spector","year":"1962"},{"key":"S0960129513000455_ref6","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1515\/9783110324921.11","volume-title":"Logic, Construction, Computation","author":"Aschieri","year":"2012"},{"key":"S0960129513000455_ref5","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:19)2010"},{"key":"S0960129513000455_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0960129513000455_ref23","first-page":"1","volume-title":"Lambda-calcul, types et mod\u00e8les","author":"Krivine","year":"1990"},{"key":"S0960129513000455_ref19","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0960129513000455_ref24","first-page":"197","volume-title":"Interactive models of computation and program behavior","author":"Krivine","year":"2009"},{"key":"S0960129513000455_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000455","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,10]],"date-time":"2022-03-10T15:15:48Z","timestamp":1646925348000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000455\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,25]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["S0960129513000455"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000455","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,10,25]]},"article-number":"e240601"}}