{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T23:56:57Z","timestamp":1676678217733},"reference-count":12,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13250,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1977,12]]},"abstract":"Abstract<\/jats:title>Every recursively enumerable extension of arithmetic which obeys the disjunction property obeys the numerical existence property [Fr, 1]. The requirement of recursive enumerability is essential. For extensions of intuitionistic second order arithmetic by means of sentences (in its language) with no existential set quantifiers, the numerical existence property implies the set existence property. The restriction on existential set quantifiers is essential. The numerical existence property cannot be eliminated, but in the case of finite extensions of HAS, can be replaced by a weaker form of it. As a consequence, the set existence property for intuitionistic second order arithmetic can be proved within itself.<\/jats:p>","DOI":"10.2307\/2271871","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:45:39Z","timestamp":1146951939000},"page":"506-514","source":"Crossref","is-referenced-by-count":3,"title":["On the derivability of instantiation properties"],"prefix":"10.1017","volume":"42","author":[{"given":"Harvey","family":"Friedman","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S002248120005012X_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90001-X"},{"key":"S002248120005012X_ref007","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1973-0432406-2"},{"key":"S002248120005012X_ref001","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.72.8.2877"},{"key":"S002248120005012X_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066744"},{"key":"S002248120005012X_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"S002248120005012X_ref005","first-page":"11","volume":"27","author":"Kleene","year":"1962","journal-title":"Disjunction and existence under implication in elementary intuitionistic formalisms"},{"key":"S002248120005012X_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066773"},{"key":"S002248120005012X_ref003","unstructured":"de Jongh D. H. J. and Smorynski C. , Kripke models and the theory of species, University of Amsterdam, Report 74\u201303, 1974."},{"key":"S002248120005012X_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066774"},{"key":"S002248120005012X_ref004","first-page":"109","volume":"10","author":"Kleene","year":"1945","journal-title":"On the interpretation of intuitionistic number theory"},{"key":"S002248120005012X_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70854-1"},{"key":"S002248120005012X_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066742"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S002248120005012X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T20:46:37Z","timestamp":1558989997000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S002248120005012X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1977,12]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1977,12]]}},"alternative-id":["S002248120005012X"],"URL":"https:\/\/doi.org\/10.2307\/2271871","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1977,12]]}}}