{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T06:14:42Z","timestamp":1711347282519},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1380,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2010,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functional of finite type. As an application, we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.<\/jats:p>","DOI":"10.2178\/jsl\/1268917503","type":"journal-article","created":{"date-parts":[[2010,3,18]],"date-time":"2010-03-18T13:05:57Z","timestamp":1268917557000},"page":"759-773","source":"Crossref","is-referenced-by-count":2,"title":["The bounded functional interpretation of the double negation shift"],"prefix":"10.1017","volume":"75","author":[{"given":"Engr\u00e1cia","family":"Patr\u00edcia","sequence":"first","affiliation":[]},{"given":"Fernando","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200002760_ref014","first-page":"1","volume-title":"Recursive function theory","author":"Spector","year":"1962"},{"key":"S0022481200002760_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_44"},{"key":"S0022481200002760_ref012","volume-title":"Applied proof theory: Proof interpretations and their use in mathematics","author":"Kohlenbach","year":"2008"},{"key":"S0022481200002760_ref011","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1093\/oso\/9780198538622.003.0010","volume-title":"Logic: from foundations to applications","author":"Kohlenbach","year":"1996"},{"key":"S0022481200002760_ref008","volume-title":"Collected works, vol. II","author":"G\u00f6del","year":"1990"},{"key":"S0022481200002760_ref003","first-page":"205","volume-title":"dialectica","volume":"62","author":"Ferreira","year":"2008"},{"key":"S0022481200002760_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"S0022481200002760_ref004","first-page":"122","volume-title":"Annals of Pure and Applied Logic","volume":"157","author":"Ferreira","year":"2009"},{"key":"S0022481200002760_ref002","first-page":"652","volume":"50","author":"Bezem","year":"1985","journal-title":"Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals"},{"key":"S0022481200002760_ref009","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard","year":"1968","journal-title":"Compositio Mathematica"},{"key":"S0022481200002760_ref006","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-2008-027"},{"key":"S0022481200002760_ref010","first-page":"454","volume-title":"Metamathematical investigation of intuitionistic Arithmetic and Analysis","volume":"344","author":"Howard","year":"1973"},{"key":"S0022481200002760_ref007","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0022481200002760_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.11.001"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200002760","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T05:45:05Z","timestamp":1711345505000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200002760\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["S0022481200002760"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1268917503","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6]]}}}