{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T02:12:34Z","timestamp":1674871954448},"reference-count":13,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":13160,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1978,3]]},"abstract":"<jats:p>In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in \u00a71, we motivate and define our notion of realizability in \u00a72. In \u00a73 we prove a soundness theorem, and in \u00a74 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In \u00a75 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in \u00a76, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let \u03a3 be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let \u03a3<jats:sup>\u03c9<\/jats:sup> be the theory obtained from \u03a3 by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then \u03a3<jats:sup>\u03c9<\/jats:sup> is a conservative extension of \u03a3. An interesting example of this theorem is obtained by taking \u03a3 to be classical first-order arithmetic.<\/jats:p>","DOI":"10.2307\/2271946","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:46:34Z","timestamp":1146951994000},"page":"23-44","source":"Crossref","is-referenced-by-count":27,"title":["Relativized realizability in intuitionistic arithmetic of all finite types"],"prefix":"10.1017","volume":"43","author":[{"given":"Nicolas D.","family":"Goodman","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200049860_ref013","first-page":"177","volume-title":"Zapiski Nau\u010dnyk Seminarov Leningradskogo Otdelenija Matemati\u010deskogo Instituta im. V. A. Steklova Akademii Nauk SSSR","volume":"49","author":"Minc","year":"1975"},{"key":"S0022481200049860_ref006","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S0022481200049860_ref005","first-page":"109","volume":"10","author":"Kleene","year":"1945","journal-title":"On the interpretation of intuitionistic number theory"},{"key":"S0022481200049860_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066778"},{"key":"S0022481200049860_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S0022481200049860_ref008","unstructured":"Sasso L. P. Jr. , Degrees of unsolvability of partial functions, Dissertation, University of California at Berkeley, 1971."},{"key":"S0022481200049860_ref003","first-page":"574","volume":"41","author":"Goodman","year":"1976","journal-title":"The theory of the G\u00f6del functional"},{"key":"S0022481200049860_ref009","first-page":"130","volume":"40","author":"Sasso","year":"1975","journal-title":"A survey of partial degrees"},{"key":"S0022481200049860_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70854-1"},{"key":"S0022481200049860_ref001","first-page":"225","volume":"37","author":"Goodman","year":"1972","journal-title":"A simplification of combinatory logic"},{"key":"S0022481200049860_ref010","first-page":"1","volume-title":"Recursive function theory","author":"Spector","year":"1962"},{"key":"S0022481200049860_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073966"},{"key":"S0022481200049860_ref012","article-title":"Review of [13]","volume":"52","author":"Kuzi\u010dev","year":"1976","journal-title":"Mathematical Reviews"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200049860","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T20:19:15Z","timestamp":1558988355000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200049860\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1978,3]]}},"alternative-id":["S0022481200049860"],"URL":"https:\/\/doi.org\/10.2307\/2271946","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,3]]}}}