{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,12]],"date-time":"2022-06-12T08:25:16Z","timestamp":1655022316957},"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":5490,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1999,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We deal with ontological problems concerning basic systems of explicit mathematics, as formalized in J\u00e4ger's language of types and names. We prove a generalized inseparability lemma, which implies a form of Rice's theorem for types and a refutation of the strong power type axiom POW<jats:sup>+<\/jats:sup>. Next, we show that POW<jats:sup>+<\/jats:sup> can already be refuted on the basis of a weak uniform comprehension <jats:italic>without complementation<\/jats:italic>, and we present suitable optimal refinements of the remaining results within the weaker theory.<\/jats:p>","DOI":"10.2307\/2586767","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T14:02:25Z","timestamp":1146924145000},"page":"313-326","source":"Crossref","is-referenced-by-count":5,"title":["Uniform inseparability in explicit mathematics"],"prefix":"10.1017","volume":"64","author":[{"given":"Andrea","family":"Cantini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierluigi","family":"Minari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200014067_ref012","volume-title":"Theory of recursive functions and effective computability","author":"Rogers","year":"1967"},{"key":"S0022481200014067_ref007","first-page":"468\u2013489","volume":"61","author":"Glass","year":"1996","journal-title":"On power set in explicit mathematics"},{"key":"S0022481200014067_ref004","doi-asserted-by":"crossref","first-page":"87\u2013139","DOI":"10.1007\/BFb0062852","volume-title":"Algebra and logic","volume":"450","author":"Feferman","year":"1975"},{"key":"S0022481200014067_ref003","volume-title":"Logical frameworks for truth and abstraction","author":"Cantini","year":"1996"},{"key":"S0022481200014067_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0022481200014067_ref010","volume-title":"Studia Logica","author":"Minari"},{"key":"S0022481200014067_ref005","first-page":"159\u2013225","volume-title":"Logic colloquium '78","author":"Feferman","year":"1979"},{"key":"S0022481200014067_ref002","volume-title":"Studia Logica","author":"Cantini"},{"key":"S0022481200014067_ref009","first-page":"1142\u20131146","volume":"62","author":"J\u00e4ger","year":"1997","journal-title":"Power types in explicit mathematics"},{"key":"S0022481200014067_ref011","volume-title":"Classical recursion theory","author":"Odifreddi","year":"1989"},{"key":"S0022481200014067_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00058-B"},{"key":"S0022481200014067_ref008","first-page":"118\u2013128","volume-title":"CSL '87","volume":"329","author":"J\u00e4ger","year":"1987"},{"key":"S0022481200014067_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(89)90019-5"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200014067","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,10]],"date-time":"2019-05-10T15:06:45Z","timestamp":1557500805000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200014067\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["S0022481200014067"],"URL":"https:\/\/doi.org\/10.2307\/2586767","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}