{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T05:24:44Z","timestamp":1648790684096},"reference-count":4,"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":3571,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2004,6]]},"abstract":"<jats:p>A formalized version of Kleene realizability for intuitionistic first-order arithmetic <jats:bold>HA<\/jats:bold> was axiomatically characterized by Troelstra (see [2, 3.2]) as follows: for an arbitrary <jats:bold>HA<\/jats:bold>-sentence <jats:italic>\u03c6<\/jats:italic>, <jats:bold>HA<\/jats:bold> \u22a2 \u2203<jats:italic>x<\/jats:italic>(<jats:italic>x<\/jats:italic> realizes <jats:italic>\u03c6<\/jats:italic>) if and only if <jats:bold>HA<\/jats:bold> + ECT<jats:sub>0<\/jats:sub> \u22a2 <jats:italic>\u03c6<\/jats:italic>.<\/jats:p><jats:p>Many notions of realizability have been characterized in this fashion: see [2] or [3] for details. For some notions, for example extensional realizability, it is necessary to pass to an extension of <jats:bold>HA<\/jats:bold>: realizability in <jats:bold>HA<\/jats:bold> is characterized by deducibility from certain axioms in an extension of <jats:bold>HA<\/jats:bold>.<\/jats:p><jats:p>The present note is concerned with <jats:italic>modified realizability<\/jats:italic>, seen as interpretation for <jats:bold>HA<\/jats:bold>. From semantical considerations (see [4]) it follows that this interpretation can be constructed as a combination of three ingredients:<\/jats:p><jats:p>i) Kleene realizability;<\/jats:p><jats:p>ii) Kripke forcing over a 2-element linear order <jats:italic>P<\/jats:italic>;<\/jats:p><jats:p>iii) The Friedman translation [1].<\/jats:p><jats:p>This will be shown in section 2. The Friedman translation (in the way we use it) introduces a new propositional constant <jats:italic>V<\/jats:italic>; hence we move to an extension <jats:bold>HA<\/jats:bold>(<jats:italic>V<\/jats:italic>) of <jats:bold>HA<\/jats:bold>. We must then define Kleene realizability and forcing for the extended language. Now let (<jats:italic>\u03c6<\/jats:italic>)<jats:italic>v<\/jats:italic> be the result of the Friedman translation applied to <jats:italic>\u03c6<\/jats:italic>. We obtain, in <jats:bold>HA<\/jats:bold>, that the sentence saying that <jats:italic>\u03c6<\/jats:italic> is modified-realizable, is equivalent to the sentence which says that the statement \u201c(<jats:italic>\u03c6<\/jats:italic>)<jats:italic>v<\/jats:italic> is Kleene-realizable\u201d is forced in <jats:italic>P<\/jats:italic> (see section 2).<\/jats:p>","DOI":"10.2178\/jsl\/1082418535","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:35:23Z","timestamp":1109799323000},"page":"421-429","source":"Crossref","is-referenced-by-count":0,"title":["A partial analysis of modified realizability"],"prefix":"10.1017","volume":"69","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":"S0022481200007829_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"S0022481200007829_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0022481200007829_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(97)00101-1"},{"key":"S0022481200007829_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200007829","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T21:02:41Z","timestamp":1557176561000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200007829\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,6]]},"references-count":4,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,6]]}},"alternative-id":["S0022481200007829"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1082418535","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,6]]}}}