{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T21:41:06Z","timestamp":1697665266849},"reference-count":10,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T00:00:00Z","timestamp":1081296000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2004,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>It is well known that the extensional axiom of choice (AC<jats:sub>ext<\/jats:sub>) implies the law of excluded middle (EM). We here prove that the converse holds as well if we have the intensional (\u2018type\u2010theoretical\u2019) axiom of choice AC<jats:sub>int<\/jats:sub>, which is provable in Martin\u2010L\u00f6f's type theory, and a weak extensionality principle (Ext<jats:sub>\u2212<\/jats:sub>), which is provable in Martin\u2010L\u00f6f's extensional type theory. In particular, EM is equivalent to AC<jats:sub>ext<\/jats:sub> in extensional type theory. (\u00a9 2004 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200410100","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T15:02:29Z","timestamp":1081350149000},"page":"236-240","source":"Crossref","is-referenced-by-count":4,"title":["EM + Ext<sub>\u2212<\/sub> + AC<sub>int<\/sub> is equivalent to AC<sub>ext<\/sub>"],"prefix":"10.1002","volume":"50","author":[{"given":"Jesper","family":"Carlstr\u00f6m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2004,4,7]]},"reference":[{"key":"e_1_2_1_2_2","unstructured":"P.Aczel andN.Gambino Collection principles in dependent type theory. In: Types for Proofs and Programs InternationalWorkshop TYPES 2000 Durham UK December 8\u201012 2000 Selected Papers (P. Callaghan Z. Luo J. McKinna and R. Pollack eds.) Springer Lecture Notes in Computer Science2277 1\u201323 (2002)."},{"key":"e_1_2_1_3_2","unstructured":"E.Bishop Foundations of Constructive Analysis (McGraw\u2013Hill New York 1967)."},{"key":"e_1_2_1_4_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":"Proceedings of Amer. Math. Soc."},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19780242514"},{"key":"e_1_2_1_6_2","unstructured":"S.Lacas andB.Werner Which choices imply the Excluded Middle? Preprint 1999."},{"key":"e_1_2_1_7_2","unstructured":"M.Maietti About effective quotients in constructive type theory. In: Types for Proofs and Programs International Workshop TYPES '98 Kloster Irsee Germany March 27\u201031 1998 Selected Papers (T. Altenkirch W. Naraschewski and B. Reus eds.) Springer Lecture Notes in Computer Science1657 164\u2013178 (1999)."},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19990450410"},{"key":"e_1_2_1_9_2","unstructured":"P.Martin\u2010L\u00f6f Intuitionistic Type Theory (Bibliopolis Naples 1984)."},{"key":"e_1_2_1_10_2","unstructured":"B.Nordstr\u00f6m K.Petersson andJ.Smith Programming in Martin\u2010L\u00f6f's Type Theory (Oxford Univ. Press Oxford 1990). http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/book\/."},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.2307\/2274575"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200410100","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200410100","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T21:05:07Z","timestamp":1697663107000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200410100"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,7]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,5]]}},"alternative-id":["10.1002\/malq.200410100"],"URL":"https:\/\/doi.org\/10.1002\/malq.200410100","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,7]]}}}