Why topology in the minimalist foundation must be pointfree
DOI:
https://doi.org/10.12775/LLP.2013.010Keywords
pointfree topology, real numbers, choice sequences’ Bar Induction, constructive type theory, axiom of unique choice, minimalist foundationAbstract
We give arguments explaining why, when adopting a minimalist approach to constructive mathematics as that formalized in our two-level minimalist foundation, the choice for a pointfree approach to topology is not just a matter of convenience or mathematical elegance, but becomes compulsory. The main reason is that in our foundation real numbers, either as Dedekind cuts or as Cauchy sequences, do not form a set.
References
Aczel, P., “The type theoretic interpretation of constructive set theory”, in Logic Colloquium ’77 (Proc. Conf., Wrocław, 1977), vol. 96 of Stud. Logic Foundations Math., North-Holland, Amsterdam – New York, 1978.
Aczel, P., “The type theoretic interpretation of constructive set theory: choice principles”, in D. van Dalen and A. Troelstra (ed.), The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), vol. 110 of “Stud. Logic Foundations Math.”, North-Holland, Amsterdam – New York, 1982.
Aczel, P., “The type theoretic interpretation of constructive set theory: inductive definitions”, in Logic, Methodology and Philosophy of Science, VII (Salzburg, 1983), vol. 114 of “Stud. Logic Foundations Math.”, North-Holland, Amsterdam – New York, 1986.
Allen, S.F., M. Bickford, R.L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran, “Innovations in Computational Type Theory using Nuprl”, Journal of Applied Logic, 4 (2006), 4: 428–469.
Asperti, A., W. Ricciotti, C. Sacerdoti Coen, and E. Tassi, “The Matita interactive theorem prover”, in Proceedings of the 23rd International Conference on Automated Deduction (CADE-2011), Wrocław, Poland, vol. 6803 of “LNCS”, 2011.
Barthes, G., V. Capretta, and O. Pons, “Setoids in type theory”, J. Funct. Programming, 13 (2003), 2: 261–293. Special issue on “Logical frameworks and metalanguages”.
Battilotti, G., and G. Sambin, “Pretopologies and a uniform presentation of sup-lattices, quantales and frames”, Annals of Pure and Applied Logic, 137 (2006): 30–61. Special issue: “Papers presented at the 2nd Workshop on Formal Topology (2WFTop 2002)”.
Beeson, M., Foundations of Constructive Mathematics, Springer-Verlag, Berlin, 1985.
Bell, J. L., Toposes and Local Set Theories: An introduction, Claredon Press, Oxford, 1988.
Bishop, E., Foundations of Constructive Analysis, McGraw-Hill Book Co., 1967.
Bishop, E., and D. S. Bridges, Constructive analysis, Springer, 1985.
Bove, A., P. Dybjer, and U. Norell, “A brief overview of Agda – a functional language with dependent types”, in S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, vol. 5674 of “Lecture Notes in Computer Science”, Springer, 2009, pp. 73–78.
Bridges, D., “A reverse look at Brouwer’s Fan Theorem”, in One Hundred Years of Intuitionism (1907–2007), Birkäuser, 2008, pp. 316–325.
Bridges, D., and F. Richman, Varieties of constructive mathematics, vol. 97 of “London Mathematical Society Lecture Note Series”, Cambridge University Press, 1987.
Ciraulo, F., M. E. Maietti, and G. Sambin, “Convergence in formal topology: An unifying presentation”, Logic and Analysis, 5 (2013), 2: 1–45.
Coq development team, The Coq Proof Assistant Reference Manual: Release 8.3, INRIA, Orsay, France, 2010.
Coquand, T., “Metamathematical investigation of a calculus of constructions”, in P. Odifreddi (ed.), Logic in Computer Science, Academic Press, 1990, pp. 91–122.
Coquand, T., G. Sambin, J. Smith, and S. Valentini, “Inductively generated formal topologies”, Annals of Pure and Applied Logic, 124 (2003), 1–3: 71–106.
Coquand, Th., and C. Paulin-Mohring, “Inductively defined types”, in P. Martin-Löf, and G. Mints (eds.), Proceedings of the International Conference on Computer Logic (Colog ’88), vol. 417 of “Lecture Notes in Computer Science”, Springer, Berlin, Germany, 1990, pp. 50–66.
Curi, G., “On some peculiar aspects of the constructive theory of pointfree spaces”, Mathematical Logic Quarterly, 56 ((2010)), 4: 375–387.
Feferman, S., “Constructive theories of functions and classes”, in Logic Colloquium ’78 (Mons, 1978), Stud. Logic Foundations Math., North-Holland, Amsterdam – New York, 1979, pp. 159–224.
Fourman, M., and R.J. Grayson, “Formal spaces”, in The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), vol. 110 of Stud. Logic Foundations Math., North-Holland, 1982, pp. 107–122.
Gambino, N., and P. Schuster, “Spatiality for formal topologies”, Math. Structures Comput. Sci., 17 (2007), 1: 65–80.
Hofmann, M., Extensional Constructs in Intensional Type Theory, Distinguished Dissertations, Springer, 1997.
Hyland, J.M.E., “The effective topos”, in The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), vol. 110 of “Stud. Logic Foundations Math.”, North-Holland, Amsterdam – New York„ 1982, pp. 165–216.
Hyland, J.M.E., P.T. Johnstone, and A.M. Pitts, “Tripos theory”, Bull. Austral. Math. Soc., 88 (1980): 205–232.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 182
Number of citations: 5
