Abstract
The continuum is here presented as a formal space by means of a finitary inductive definition. In this setting a constructive proof of the Heine-Borel covering theorem is given.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. An Introduction to Inductive Definitions, in Handbook of Mathematical Logic, J. Barwise ed., North-Holland (1977) 739–782.
L. E. J. Brouwer. Die intuitionistische Form des Heine-Borelschen Theorems, in L. E. J. Brouwer Collected Works, A. Heyting ed., North-Holland, Amsterdam (1975) vol. 1, 350–351, 1926C.
E. Bishop. “Foundations of Constructive Analysis”, Mc Graw Hill, 1967.
J. Cederquist. A machine assisted formalization of pointfree topology in type theory, Chalmers University of Technology and University of Göteborg, Sweden, Licentiate Thesis (1994).
J. Cederquist, T. Coquand, S. Negri Helly-Hahn-Banach in formal topology, forthcoming.
T. Coquand. An intuitionistic proof of Tychonoff 's theorem, The Journal of Symbolic Logic vol. 57, no. 1 (1992) 28–32.
T. Coquand. Constructive Topology and Combinatorics, proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613 (1992) 159–164.
M. P. Fourman, R.J. Grayson. Formal Spaces, in “The L. E. J. Brouwer Centenary Symposium”, A. S. Troelstra and D. van Dalen (eds), North-Holland, Amsterdam (1982) 107–122.
M. Franchella. “L. E. J. Brouwer pensatore eterodosso. L'intuizionismo tra matematica e filosofia”, Guerini Studio (1994).
A. Heyting. “Intuitionism, an introduction”, North-Holland (1971).
P. T. Johnstone. “Stone Spaces”, Cambridge University Press (1982).
L. Magnusson, “The Implementation of ALF — a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution”, Chalmers University of Technology and University of Göteborg, PhD thesis (1995).
P. Martin-Löf. “Notes on Constructive Mathematics”, Almqvist & Wiksell, Stockholm (1970).
P. Martin-Löf. “Intuitionistic type theory”, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Napoli (1984).
S. Negri. Stone bases, alias the constructive content of Stone representation, “Logic and Algebra”, A. Ursini and P. Aglianò eds., Dekker, New York (1996) 617–636.
S. Negri. “Dalla topologia formale all'analisi”, Ph.D. thesis, University of Padua (1996).
S. Negri, D. Soravia. The continuum as a formal space, Rapporto Interno n.4, 17-7-95, Dipartimento di Matematica Pura e Applicata, Universitá di Padova.
S. Negri, S. Valentini. Tychonoff 's theorem in the framework of formal topologies, The Journal of Symbolic Logic (in press).
B. Nordström, K. Peterson, J. Smith, “Programming in Martin-Löf's Type Theory”, Oxford University Press (1990).
G. Sambin. Intuitionistic formal spaces — a first communication, in Mathematical logic and its applications, D. Skordev ed., Plenum (1987) 187–204.
G. Sambin. Intuitionistic formal spaces and their neighbourhoods, in “Logic Colloquium 88”, R. Ferro et al. eds., North-Holland, Amsterdam (1989) 261–285.
G. Sambin, S. Valentini, P. Virgili. Constructive Domain Theory as a branch of Intuitionistic Pointfree Topology, Theoretical Computer Science (in press).
W. P. van Stigt. “Brouwer's Intuitionism”, Studies in the History and Philosophy of Mathematics, vol. 2, North-Holland (1990).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cederquist, J., Negri, S. (1996). A constructive proof of the Heine-Borel covering theorem for formal reals. In: Berardi, S., Coppo, M. (eds) Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science, vol 1158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61780-9_62
Download citation
DOI: https://doi.org/10.1007/3-540-61780-9_62
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61780-8
Online ISBN: 978-3-540-70722-6
eBook Packages: Springer Book Archive