On the existence of Stone-Čech compactification. (English) Zbl 1225.03089

Curi, Giovanni

J. Symb. Log. 75, No. 4, 1137-1146 (2010).

From the introduction: In [Ann. Pure Appl. Logic 146, No. 2–3, 103–123 (2007; Zbl 1139.03044)], I characterized the locales of which the Stone-Čech 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.
In this paper I show that this characterization continues to hold over the standard system CZF\(^+\), i.e., CZF plus REA, thus removing in particular any dependency from a choice principle. This will follow by a result of independent interest, namely the proof that the class of continuous mappings from a compact regular locale \(X\) to a regular and set-presented locale \(Y\) is a set in CZF (even without REA).
By exploiting the consistency of CZF+REA with a general form of Troelstra’s principle of uniformity [A. S. Troelstra and D. van Dalen, Constructivism in mathematics. An introduction. Volume I. Studies in Logic and the Foundations of Mathematics, 121. Amsterdam etc.: North-Holland (1988; Zbl 0653.03040)], I then prove that the existence of Stone-Čech compactification of a non-degenerate Boolean locale is independent of the axioms of CZF (+REA), so that the aforementioned characterization characterizes a proper subcollection of the collection of all locales. The same also holds for several, even impredicative, extensions of CZF+REA, as well as for CTT. This is in strong contrast with what happens in the context of higher-order Heyting arithmetic HHA – and thus in any topos-theoretic universe: within HHA the constructions by Banaschewski and Mulvey and by Johnstone of Stone-Čech compactification can be carried out for every locale.

MSC:

03F60	Constructive and recursive analysis
03F65	Other constructive mathematics
06D22	Frames, locales
54D35	Extensions of spaces (compactifications, supercompactifications, completions, etc.)

Keywords:

Stone-Čech compactification; constructive type theory; constructive set theory; CZF; regular extension axiom; principle of uniformity; non-degenerate Boolean locale

Citations:

Zbl 1139.03044; Zbl 0653.03040

References:

[1]	Logic Colloquium 2003 24 pp 282– (2006)
[2]	DOI: 10.1090/S0002-9947-1937-1501905-7 · JFM 63.1173.01 · doi:10.1090/S0002-9947-1937-1501905-7
[3]	DOI: 10.1007/BF01278464 · Zbl 0819.03047 · doi:10.1007/BF01278464
[4]	DOI: 10.1016/S0168-0072(03)00052-6 · Zbl 1070.03041 · doi:10.1016/S0168-0072(03)00052-6
[5]	DOI: 10.2307/1968839 · Zbl 0017.42803 · doi:10.2307/1968839
[6]	Theoretical Computer Science · Zbl 0867.68002
[7]	DOI: 10.1016/S0022-4049(03)00119-1 · Zbl 1036.54006 · doi:10.1016/S0022-4049(03)00119-1
[8]	DOI: 10.1016/0022-4049(84)90001-X · Zbl 0549.54017 · doi:10.1016/0022-4049(84)90001-X
[9]	Houston Journal of Mathematics 6 pp 301– (1980)
[10]	Notes on constructive set theory (2000)
[11]	DOI: 10.1016/j.apal.2009.03.005 · Zbl 1223.03050 · doi:10.1016/j.apal.2009.03.005
[12]	DOI: 10.1016/j.apal.2005.05.016 · Zbl 1077.03035 · doi:10.1016/j.apal.2005.05.016
[13]	Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland, August 14–20, 2003 24 pp 221– (2006)
[14]	Intuitionistic type theory (1984)
[15]	DOI: 10.1007/s11813-007-0005-6 · Zbl 1162.03034 · doi:10.1007/s11813-007-0005-6
[16]	DOI: 10.1016/j.apal.2005.07.002 · Zbl 1094.03038 · doi:10.1016/j.apal.2005.07.002
[17]	Sketches of an elephant: a topos theory compendium. II 44 (2002) · Zbl 1071.18001
[18]	Stone spaces (1982) · Zbl 0499.54001
[19]	DOI: 10.1007/BFb0061824 · doi:10.1007/BFb0061824
[20]	Mathematical Logic Quarterly
[21]	DOI: 10.1016/j.jpaa.2007.07.023 · Zbl 1141.06003 · doi:10.1016/j.jpaa.2007.07.023
[22]	DOI: 10.1016/j.apal.2006.12.004 · Zbl 1139.03044 · doi:10.1016/j.apal.2006.12.004
[23]	Constructivism in mathematics, an introduction 121 (1988)
[24]	Logic Colloquium 2002 27 pp 299– (2006)