{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T10:40:26Z","timestamp":1648636826152},"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":6585,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1996,3]]},"abstract":"The purpose of this note is to clarify two points about the topos Lif, introduced in [13] as a generalization of Lifschitz' realizability ([9, 12]). Lif is a subtopos of Hyland's Effective topos ([1]). The points I want to make are:<\/jats:p>Remark 1.<\/jats:bold> Lif is the largest subtopos of satisfying the axiom (O):<\/jats:p><\/jats:disp-formula><\/jats:p>where denotes partial recursive application, and \u201c\u2208 Tot\u201d means that e<\/jats:italic> and f<\/jats:italic> range over codes for total recursive functions. One may read (O) as the statement \u201cThe union of two -sets is again a -set\u201d. That is, let be a subtopos of . Then (O) is true in for the standard interpretation (the variables range over the natural numbers object of , etc.) if and only if the inclusion \u21a3 factors through the inclusion Lif \u21a3 .<\/jats:p>Remark 2.<\/jats:bold> Like , Lif contains at least two weakly complete internal full subcategories, thus providing us with more models of polymorphism and other impredicative type theories.<\/jats:p>The principle (O) has some standing in the history of constructive mathematics:<\/jats:p>- H. Friedman has proved that (O) is equivalent to a formulation of intuitionistic completeness of the intuitionistic predicate calculus for Tarskian semantics; see [8]. This is not to imply that this result is of immediate relevance to Lif: Friedman works in a system of analysis, a theory of lawless sequences with an axiom of \u201copen data\u201d for arithmetical formulas, which at least for the domain of all functions from N<\/jats:italic> to N<\/jats:italic> fails in Lif. However, there might exist a \u201cnonstandard model\u201d of arithmetic and a corresponding system of analysis, in which we may be able to carry out his proof.<\/jats:p>- Moreover, Remark 2 entails that Lif should provide us with models of synthetic domain theory (for an exposition, see [3]), and one with the nice property that the dual of one of the axioms (axiom 7 in [3]) comes for free, by (O).<\/jats:p>","DOI":"10.2307\/2275598","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:57:36Z","timestamp":1146956256000},"page":"70-79","source":"Crossref","is-referenced-by-count":2,"title":["Two remarks on the Lifschitz realizability topos"],"prefix":"10.1017","volume":"61","author":[{"given":"Jaap Van","family":"Oosten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200017643_ref011","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054190000242"},{"key":"S0022481200017643_ref006","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-60.1.1"},{"key":"S0022481200017643_ref005","first-page":"333","volume-title":"Mathematical foundations of programming language semantics","author":"Hyland"},{"key":"S0022481200017643_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"S0022481200017643_ref012","first-page":"805","volume":"55","author":"van Oosten","year":"1990","journal-title":"Liftschitz' readability"},{"key":"S0022481200017643_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100068146"},{"key":"S0022481200017643_ref007","volume-title":"Topos theory","author":"Johnstone","year":"1976"},{"key":"S0022481200017643_ref009","first-page":"101","article-title":"CT0 is stronger than CT0!","volume":"73","author":"Lifschitz","year":"1979","journal-title":"Proceedings of the American Mathematical Society"},{"key":"S0022481200017643_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0022481200017643_ref001","first-page":"165","volume-title":"The L. E. J. Brower centenary symposium","author":"Hyland","year":"1982"},{"key":"S0022481200017643_ref013","first-page":"964","volume":"56","author":"van Oosten","year":"1991","journal-title":"Extension of Lifschitz' realizability to higher arithmetic, and a solution to a problem of F, Richman"},{"key":"S0022481200017643_ref003","first-page":"131","volume-title":"Cateogry theory, proceedings of the conference in Como 1990","author":"Hyland","year":"1991"},{"key":"S0022481200017643_ref008","volume-title":"Harvey Friedman's research on the foundations of mathematics","author":"Leivant","year":"1985"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200017643","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T19:07:37Z","timestamp":1557774457000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200017643\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["S0022481200017643"],"URL":"https:\/\/doi.org\/10.2307\/2275598","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}