{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:59:45Z","timestamp":1773097185273,"version":"3.50.1"},"reference-count":7,"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":8685,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>V. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a \u201cq-variant\u201d we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.<\/jats:p>","DOI":"10.2307\/2274666","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:35:29Z","timestamp":1146954929000},"page":"805-821","source":"Crossref","is-referenced-by-count":15,"title":["Lifschitz' realizability"],"prefix":"10.1017","volume":"55","author":[{"given":"Jaap","family":"van Oosten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200026165_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0022481200026165_ref004","volume-title":"The foundations of intuitionistic mathematics","author":"Kleene","year":"1965"},{"key":"S0022481200026165_ref001","volume-title":"Mathematical intuitionisnu introduction to proof theory","author":"Dragalin","year":"1979"},{"key":"S0022481200026165_ref007","volume-title":"Constructivism in mathematics","author":"Troelstra","year":"1988"},{"key":"S0022481200026165_ref002","first-page":"165","volume-title":"The L.E.J. Brouwer centenary symposium","author":"Hyland","year":"1982"},{"key":"S0022481200026165_ref003","volume-title":"Memoirs of the American Mathematical Society","author":"Kleene","year":"1969"},{"key":"S0022481200026165_ref005","first-page":"101","article-title":"CT0is stronger than CT0!","volume":"73","author":"Lifschitz","year":"1979","journal-title":"Proceedings of the American Mathematical Society"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200026165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T21:14:03Z","timestamp":1558214043000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200026165\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,6]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1990,6]]}},"alternative-id":["S0022481200026165"],"URL":"https:\/\/doi.org\/10.2307\/2274666","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,6]]}}}