{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,29]],"date-time":"2023-10-29T04:29:46Z","timestamp":1698553786396},"reference-count":15,"publisher":"Wiley","issue":"4","license":[{"start":{"date-parts":[[2010,11,17]],"date-time":"2010-11-17T00:00:00Z","timestamp":1289952000000},"content-version":"vor","delay-in-days":4338,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[1999,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper we analyze an extension of Martin\u2010L\u00f6f s intensional set theory by means of a set contructor <jats:italic>P<\/jats:italic> such that the elements of <jats:italic>P<\/jats:italic>(<jats:italic>S<\/jats:italic>) are the subsets of the set <jats:italic>S.<\/jats:italic> Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is \u201c(<jats:italic>A V \u231d A<\/jats:italic>) <jats:italic>true<\/jats:italic> holds for any proposition <jats:italic>A.<\/jats:italic><\/jats:p>","DOI":"10.1002\/malq.19990450410","type":"journal-article","created":{"date-parts":[[2010,11,17]],"date-time":"2010-11-17T16:31:05Z","timestamp":1290011465000},"page":"521-532","source":"Crossref","is-referenced-by-count":18,"title":["Can You Add Power\u2010Sets to Martin\u2010Lof's Intuitionistic Set Theory?"],"prefix":"10.1002","volume":"45","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Valentini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,11,17]]},"reference":[{"key":"e_1_2_1_2_2","volume-title":"Toposes and Local Set Theory: An Introduction","author":"Bell J. L.","year":"1988"},{"key":"e_1_2_1_3_2","first-page":"589","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"De BRUUN N. G.","year":"1980"},{"key":"e_1_2_1_4_2","first-page":"91","volume-title":"Logic in Computer Science","author":"Coquand T.","year":"1990"},{"key":"e_1_2_1_5_2","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1090\/S0002-9939-1975-0373893-X","article-title":"Axiom of choice and complementation","volume":"51","author":"Diaconescu R.","year":"1975","journal-title":"Proc. Amer. Math. Soc."},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01278464"},{"key":"e_1_2_1_7_2","unstructured":"Hofmann M. Extensional concepts in intensional type theory. PhD Thesis University of Edinburgh 1995."},{"key":"e_1_2_1_8_2","first-page":"83","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Hofmann M.","year":"1995"},{"key":"e_1_2_1_9_2","first-page":"399","article-title":"The inconsistency of higher order extensions of Martin\u2010Lof's type theory","volume":"13","author":"Jacobs B.","year":"1989","journal-title":"J. Philos. Logic"},{"key":"e_1_2_1_10_2","volume-title":"An Introduction to Higher Order Categorical Logic","author":"Lambek J.","year":"1986"},{"key":"e_1_2_1_11_2","unstructured":"Luo Z. An extended calculus of constructions. PhD Thesis University of Edinburgh 1990."},{"key":"e_1_2_1_12_2","doi-asserted-by":"crossref","unstructured":"Martin\u2010L\u00d6F P. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: The Second Scandinavian Logic Symposium (J. E. FENSTAD ed.) North Holland Publ. Comp. Amsterdam1971.","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"e_1_2_1_13_2","unstructured":"Martin\u2010L\u00d6F P. Intuitionistic Type Theory. Notes by G. SAMBIN of a series of lectures given in Padua June 1980. Bibliopolis Naples1984."},{"key":"e_1_2_1_14_2","volume-title":"Programming in Martin\u2010Lof's Type Theory: An Introduction","author":"Nordstr\u00d6M B.","year":"1990"},{"key":"e_1_2_1_15_2","first-page":"221","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Sambin G.","year":"1995"},{"key":"e_1_2_1_16_2","first-page":"275","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Valentini S.","year":"1995"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.19990450410","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.19990450410","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.19990450410","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T21:17:08Z","timestamp":1698527828000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.19990450410"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":15,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["10.1002\/malq.19990450410"],"URL":"https:\/\/doi.org\/10.1002\/malq.19990450410","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}