{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:03:00Z","timestamp":1760346180474},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1197,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2010,12]]},"abstract":"<jats:p><jats:bold>Introduction.<\/jats:bold> In 1937 E. \u010cech and M.H. Stone, independently, introduced the maximal compactification of a completely regular topological space, thereafter called Stone-\u010cech compactification [8, 23]. In the introduction of [8] the non-constructive character of this result is so described: \u201cIt must be emphasized that \u03b2(<jats:italic>S<\/jats:italic>) [the Stone-\u010cech compactification of <jats:italic>S<\/jats:italic>] may be defined only formally (not constructively) since it exists only in virtue of Zermelo's theorem\u201d.<\/jats:p><jats:p>By replacing topological spaces with locales, Banaschewski and Mulvey [4, 5, 6], and Johnstone [14] obtained choice-free intuitionistic proofs of Stone-\u010cech compactification. Although valid in any topos, these localic constructions rely\u2014essentially, as is to be demonstrated\u2014on highly impredicative principles, and thus cannot be considered as constructive in the sense of the main systems for constructive mathematics, such as Martin-L\u00f6f's constructive type theory and Aczel's constructive set theory.<\/jats:p><jats:p>In [10] I characterized the locales of which the Stone-\u010cech compactification can be defined in constructive type theory CTT, and in the formal system CZF+uREA+DC, a natural extension of Aczel's system for constructive set theory CZF by a strengthening of the Regular Extension Axiom REA and the principle of Dependent Choice.<\/jats:p>","DOI":"10.2178\/jsl\/1286198140","type":"journal-article","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T13:16:13Z","timestamp":1286198173000},"page":"1137-1146","source":"Crossref","is-referenced-by-count":4,"title":["On the existence of Stone-\u010cech compactification"],"prefix":"10.1017","volume":"75","author":[{"given":"Giovanni","family":"Curi","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200002176_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/s11813-007-0005-6"},{"key":"S0022481200002176_ref021","first-page":"299","volume-title":"Logic Colloquium 2002","volume":"27","author":"Rathjen","year":"2006"},{"key":"S0022481200002176_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(84)90001-X"},{"key":"S0022481200002176_ref022","first-page":"282","volume-title":"Logic Colloquium 2003","volume":"24","author":"Rathjen","year":"2006"},{"key":"S0022481200002176_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.07.002"},{"key":"S0022481200002176_ref020","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF01278464","article-title":"The strength of some Martin-L\u00f6f type theories","volume":"33","author":"Rathjen","year":"1994","journal-title":"Archive for Mathematical Logic"},{"key":"S0022481200002176_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.12.004"},{"key":"S0022481200002176_ref014","volume-title":"Stone spaces","author":"Johnstone","year":"1982"},{"key":"S0022481200002176_ref012","volume-title":"Mathematical Logic Quarterly","author":"Curi"},{"key":"S0022481200002176_ref019","first-page":"221","volume-title":"Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland, August 14\u201320, 2003","volume":"24","author":"Palmgren","year":"2006"},{"key":"S0022481200002176_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.03.005"},{"key":"S0022481200002176_ref018","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0022481200002176_ref003","volume-title":"Notes on constructive set theory","author":"Aczel","year":"2000"},{"key":"S0022481200002176_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(03)00119-1"},{"key":"S0022481200002176_ref008","doi-asserted-by":"publisher","DOI":"10.2307\/1968839"},{"key":"S0022481200002176_ref023","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1937-1501905-7"},{"key":"S0022481200002176_ref024","unstructured":"Streicher T. , Realizability models for CZF + \u00acPow, unpublished note."},{"key":"S0022481200002176_ref004","first-page":"301","article-title":"Stone-\u010cech compactification of locales. I","volume":"6","author":"Banaschewski","year":"1980","journal-title":"Houston Journal of Mathematics"},{"key":"S0022481200002176_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.016"},{"key":"S0022481200002176_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0022481200002176_ref015","volume-title":"Sketches of an elephant: a topos theory compendium. II","volume":"44","author":"Johnstone","year":"2002"},{"key":"S0022481200002176_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2007.07.023"},{"key":"S0022481200002176_ref007","volume-title":"Theoretical Computer Science","author":"van den Berg"},{"key":"S0022481200002176_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061824"},{"key":"S0022481200002176_ref025","volume-title":"Constructivism in mathematics, an introduction","volume":"121","author":"Troelstra","year":"1988"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200002176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:36:57Z","timestamp":1556397417000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200002176\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["S0022481200002176"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1286198140","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12]]}}}