Direct spectra of Bishop spaces and their limits. (English) Zbl 1473.03038
This paper is a very high quality work in which the author presented an abundance of material of interest to researchers of mathematics within the Bishop’s constructive framework. The central part of this report is Section 7 in which the concept of direct spectrums of Bishop spaces is introduced and analyzed. In sections 8–11, which follow this, some of the fundamental characteristics of this spectrum are analyzed. They determine and analyze the direct limit of a direct spectrum of Bishop spaces (Section 9), the inverse limit of a contravariant direct spectrum of Bishop spaces (Section 10) and prove the duality principle between the inverse and direct limits of Bishop spaces (Section 11).
Reviewer: Daniel Romano (Banja Luka)
Keywords:
Bishop set theory; Bishop spaces; direct spectrum of Bishop spaces; limits of Bishop spacesReferences:
| [1] | P. Aczel, M. Rathjen:Constructive Set Theory, book draft, 2010. |
| [2] | S. Awodey:Category Theory, Oxford University Press, 2010. · Zbl 1194.18001 |
| [3] | M. J. Beeson: Formalizing constructive mathematics: why and how, in [36], 1981, 146-190. · Zbl 0464.03050 |
| [4] | E. Bishop:Foundations of Constructive Analysis, McGraw-Hill, 1967. · Zbl 0183.01503 |
| [5] | E. Bishop: A General Language, unpublished manuscript, 1968(9)? |
| [6] | E. Bishop: Mathematics as a Numerical Language, in [16], 1970, 53-71. · Zbl 0205.01201 |
| [7] | E. Bishop and H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972. · Zbl 0239.02019 |
| [8] | E. Bishop and D. S. Bridges:Constructive Analysis, Grundlehren der math. Wissenschaften 279, SpringerVerlag, Heidelberg-Berlin-New York, 1985. · Zbl 0656.03042 |
| [9] | D. S. Bridges: Reflections on function spaces, Annals of Pure and Applied Logic 163, 2012, 101-110. · Zbl 1251.03093 |
| [10] | D. S. Bridges and F. Richman:Varieties of Constructive Mathematics, Cambridge University Press, 1987. · Zbl 0618.03032 |
| [11] | J. Dugundji:Topology, Allyn and Bacon, 1966. · Zbl 0144.21501 |
| [12] | S. Feferman: Constructive theories of functions and classes, in Boffa et. al. (Eds.)Logic Colloquium 78, North-Holland, 1979, 159-224. · Zbl 0441.03022 |
| [13] | H. Friedman: Set theoretic foundations for constructive analysis, Annals of Math. 105, 1977, 1-28. · Zbl 0353.02014 |
| [14] | N. Greenleaf: Liberal constructive set theory, in [36], 1981, 213-240. · Zbl 0519.03047 |
| [15] | H. Ishihara: Relating Bishop’s function spaces to neighborhood spaces, Annals of Pure and Applied Logic 164, 2013, 482-490. · Zbl 1275.03163 |
| [16] | A. Kino, J. Myhill and R. E. Vesley (Eds.):Intuitionism and Proof Theory, North-Holland, 1970. · Zbl 0195.01201 |
| [17] | P. Martin-L¨of: An intuitionistic theory of types, in G. Sambin, J. Smith (Eds.)Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1988, 127-172. · Zbl 0931.03070 |
| [18] | R. Mines, F. Richman, W. Ruitenburg:A course in constructive algebra, Springer Science+Business Media New York, 1988. · Zbl 0725.03044 |
| [19] | J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347-382. 4:50I. PetrakisVol. 17:2 · Zbl 0314.02045 |
| [20] | E. Palmgren:Bishop’s set theory, Slides from TYPES Summer School 2005, Gothenburg, in http://staff.math.su.se/palmgren/, 2005. |
| [21] | E. Palmgren:Bishop-style constructive mathematics in type theory - A tutorial, Slides, in http://staff.math.su.se/palmgren/, 2013. |
| [22] | E. Palmgren:Lecture Notes on Type Theory, 2014. |
| [23] | E. Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384-1399. · Zbl 1257.03095 |
| [24] | E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25. · Zbl 1341.03012 |
| [25] | I. Petrakis:Constructive Topology of Bishop Spaces, PhD Thesis, Ludwig-Maximilians-Universit¨at, M¨unchen, 2015. · Zbl 1335.54002 |
| [26] | I. Petrakis: Completely Regular Bishop Spaces, in A. Beckmann, V. Mitrana and M. Soskova (Eds.): Evolving Computability, CiE 2015, LNCS 9136, 2015, 302-312. · Zbl 1461.03058 |
| [27] | I. Petrakis: The Urysohn Extension Theorem for Bishop Spaces, in S. Artemov and A. Nerode (Eds.) Symposium on Logical Foundations of Computer Science 2016, LNCS 9537, Springer, 2016, 299-316. · Zbl 1477.03254 |
| [28] | I. Petrakis: A constructive function-theoretic approach to topological compactness, Proceedings of the 31st Annual ACM-IEEEE Symposium on Logic in Computer Science (LICS 2016), July 5-8, 2016, NYC, · Zbl 1394.03076 |
| [29] | I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies, Journal of Logic and Analysis, 11:FT2, 2019, 1-44. · Zbl 1436.03313 |
| [30] | I. Petrakis: Borel and Baire sets in Bishop spaces, in F. Manea et. al. (Eds): Computing with Foresight and Industry - 15th Conference on Computability in Europe, CiE 2019, LNCS 11558, Springer, 2019, · Zbl 1434.03142 |
| [31] | I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies, Journal of Logic and Analysis 11:FT2, 2019, 1-44. · Zbl 1436.03313 |
| [32] | I. Petrakis: Dependent sums and dependent products in Bishop’s set theory, in P. Dybjer et. al. (Eds) TYPES 2018, LIPIcs, Vol. 130, Article No. 3, 2019. · Zbl 1528.03241 |
| [33] | I. Petrakis:Embeddings of Bishop spaces, Journal of Logic and Computation, exaa015, 2020, https://doi.org/10.1093/logcom/exaa015. · Zbl 1515.03224 |
| [34] | I. Petrakis: Functions of Baire-class one over a Bishop topology, in M. Anselmo et. al. (Eds.)Beyond the Horizon of Computability, CiE 2020, Springer, LNCS 12098, 2020, 215-227. · Zbl 07633510 |
| [35] | I. Petrakis:Families of Sets in Bishop Set Theory, Habilitation Thesis, LMU, 2020 (available at http://www.mathematik.uni-muenchen.de/∼petrakis/content/Theses.php). · Zbl 1515.03224 |
| [36] | F. Richman:Constructive Mathematics, LNM 873, Springer-Verlag, 1981. · Zbl 0453.00009 |
| [37] | F. Richman: Constructive mathematics without choice, in [38], pp.199-205. · Zbl 1036.03052 |
| [38] | P. Schuster, U. Berger and H. Osswald (eds.):Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, Proc. 1999 Venice Symposium, Dordrecht: Kluwer, 2001. · Zbl 0982.00037 |
| [39] | H. Schwichtenberg, S. Wainer:Proofs and Computations, Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press, 2012. · Zbl 1294.03006 |
| [40] | A. S. Troelstra, D. van Dalen:Constructivism in Mathematics, An Introduction, Volume I, North-Holland, 1988. · Zbl 0653.03040 |
| [41] | The Univalent Foundations Program:Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013. · Zbl 1298.03002 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
