Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-27T13:27:53.226Z Has data issue: false hasContentIssue false
  • English
  • Français

On the existence of Stone-Čech compactification

Published online by Cambridge University Press:  12 March 2014

Giovanni Curi
Giovanni Curi*
Affiliation:
Dipartimento di Informatica, Università di Verona, Strada le Grazie 15, 37134 Verona, Italy. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

Introduction. In 1937 E. Čech and M.H. Stone, independently, introduced the maximal compactification of a completely regular topological space, thereafter called Stone-Čech compactification [8, 23]. In the introduction of [8] the non-constructive character of this result is so described: “It must be emphasized that β(S) [the Stone-Čech compactification of S] may be defined only formally (not constructively) since it exists only in virtue of Zermelo's theorem”.

By replacing topological spaces with locales, Banaschewski and Mulvey [4, 5, 6], and Johnstone [14] obtained choice-free intuitionistic proofs of Stone-Čech compactification. Although valid in any topos, these localic constructions rely—essentially, as is to be demonstrated—on highly impredicative principles, and thus cannot be considered as constructive in the sense of the main systems for constructive mathematics, such as Martin-Löf's constructive type theory and Aczel's constructive set theory.

In [10] 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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 75 , Issue 4 , December 2010 , pp. 1137 - 1146
Copyright
Copyright © Association for Symbolic Logic 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Aczel, P., Aspects of general topology in constructive set theory, Annals of Pure and Applied Logic, vol. 137 (2006), no. 1–3, pp. 3–29.CrossRefGoogle Scholar
[2]Aczel, P. and Curi, G., On the T1 axiom and other separation properties in constructive topology, Annals of Pure and Applied Logic, vol. 161 (2010), pp. 560–569.CrossRefGoogle Scholar
[3]Aczel, P. and Rathjen, M., Notes on constructive set theory, Technical Report 40, Mittag-Leffler, 2000/2001.Google Scholar
[4]Banaschewski, B. and Mulvey, C. J., Stone-Čech compactification of locales. I, Houston Journal of Mathematics, vol. 6 (1980), pp. 301–312.Google Scholar
[5]Banaschewski, B. and Mulvey, C. J., Stone-Čech compactification of locales. II, Journal of Pure and Applied Algebra, vol. 33 (1984), pp. 107–122.CrossRefGoogle Scholar
[6]Banaschewski, B. and Mulvey, C. J., Stone-Čech compactification of locales. III, Journal of Pure and Applied Algebra, vol. 185 (2003), pp. 25–33.CrossRefGoogle Scholar
[7]van den Berg, B. and Moerdijk, I., Aspects of predicative algebraic set theory II: realizability, Theoretical Computer Science, To appear. Available from: http://arxiv.org/abs/0801.2305.Google Scholar
[8]Čech, E., On bicompact spaces, Annals of Mathematics, vol. 38 (1937), no. 2, pp. 823–844.CrossRefGoogle Scholar
[9]Coquand, T., Sambin, G., Smith, J., and Valentini, S., Inductively generated formal topologies, Annals of Pure and Applied Logic, vol. 124 (2003), no. 1–3, pp. 71–106.CrossRefGoogle Scholar
[10]Curi, G., Exact approximations to Stone-Čech compactification, Annals of Pure and Applied Logic, vol. 146 (2007), no. 2–3, pp. 103–123.CrossRefGoogle Scholar
[11]Curi, G., Remarks on the Stone-Čech and Alexandroff compactifications of locales, Journal of Pure and Applied Algebra, vol. 212 (2008), no. 5, pp. 1134–1144.CrossRefGoogle Scholar
[12]Curi, G., On some peculiar aspects of the constructive theory of point-free spaces, Mathematical Logic Quarterly, to appear.Google Scholar
[13]Fourman, M. P. and Scott, D. S., Sheaves and logic, Applications of sheaves (Fourman, M.et al., editors), Lecture Notes in Math., vol. 753, Springer, Berlin, 1979, pp. 302–401.CrossRefGoogle Scholar
[14]Johnstone, P. T., Stone spaces, Cambridge University Press, Cambridge, 1982.Google Scholar
[15]Johnstone, P. T., Sketches of an elephant: a topos theory compendium. II, Oxford Logic Guides, vol. 44, Clarendon Press, Oxford, 2002.Google Scholar
[16]Lubarsky, R. S., CZF and second order arithmetic, Annals of Pure and Applied Logic, vol. 141 (2006), no. 1–2, pp. 29–34.CrossRefGoogle Scholar
[17]Lubarsky, R. S. and Rathjen, M., On the constructive Dedekind reals, Logic and Analysis, vol. 1 (2008), no. 2, pp. 131–152.CrossRefGoogle Scholar
[18]Martin-Löf, Per, Intuitionistic type theory, Studies in Proof Theory, Bibliopolis, Napoli, 1984, Notes by G. Sambin.Google Scholar
[19]Palmgren, E., Predicativity problems in point-free topology, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland, August 14–20, 2003 (Stoltenberg-Hansen, V.et al., editors), Lecture Notes in Logic, vol. 24, Association for Symbolic Logic, AK Peters Ltd, 2006, pp. 221–231.Google Scholar
[20]Rathjen, M., The strength of some Martin-Löf type theories, Archive for Mathematical Logic, vol. 33 (1994), pp. 347–385.Google Scholar
[21]Rathjen, M., Choice principles in constructive and classical set theories, Logic Colloquium 2002 (Chatzidakis, Z., Koepke, P., and Pohlers, W., editors), Lecture Notes in Logic, vol. 27, A.K. Peters, 2006, pp. 299–326.Google Scholar
[22]Rathjen, M., Realizability for constructive Zermelo-Fraenkel set theory, Logic Colloquium 2003 (Väänänen, J. and Stoltenberg-Hansen, V., editors), Lecture Notes in Logic, vol. 24, A.K. Peters, 2006, pp. 282–314.Google Scholar
[23]Stone, M. H., Applications of the theory of Boolean rings to general topology, Transactions of the American Mathematical Society, vol. 41 (1937), pp. 375–481.CrossRefGoogle Scholar
[24]Streicher, T., Realizability models for CZF + ¬Pow, unpublished note.Google Scholar
[25]Troelstra, A. S. and van Dalen, D., Constructivism in mathematics, an introduction, Volume I. Studies in Logic and the Foundations of Mathematics, vol. 121, North-Holland Publishing Co., Amsterdam, 1988.Google Scholar