Abstract
What is the nature of mathematics? The different answers given to this perennial question can be gathered from the different theories which have been put forward as foundations of mathematics. In the common contemporary vision, the role of foundations is to provide safe grounds a posteriori for the activity of mathematicians, which on the whole is taken as a matter of fact. This is usually achieved by reducing all concepts of mathematics to that of set, and by postulating sets to form a fixed universe, which exists by itself and is unaffected by any human activity. Thus it is a static vision.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
More precisely—as explained to me by Milly Maietti—ML type theory deprived of the reduction rule inferring \(b=c\) from \(\lambda x.b=\lambda x.c\), and of universes.
- 2.
This is essentially Diaconescu theorem saying that that every topos satisfying AC is boolean (see (Bell, 1988) for a simple proof). Its version for type theory says more precisely that PSA, or more generally extensional quotients, are incompatible with AC, since the choice function does not respect extensionality (Maietti and Valentini, 1999; Maietti, 1999).
- 3.
More precisely, choice sequences can be defined as formal points over a suitable formal topology on the tree.
- 4.
This and the next equation are an immediate consequence of the fact that â—Š is left adjoint to rest, which means that the equivalence \(\Diamond D \subseteq U\) iff \(D\subseteq \textsf{rest} U\) holds for every D and U.
- 5.
It is still an open problem to prove, under the assumptions that \({\mathcal A},{\mathcal J}\) are presented by a basic pair and that \({\mathcal A} = {\mathcal A}_{I,C}\), that also \({\mathcal J} = {\mathcal J}_{I,C}\) holds.
Bibliography
Battilotti, G. and Sambin, G. (2006). Pretopologies and a uniform presentation of sup-lattices, quantales and frames. Annals of Pure and Applied Logic, 137:30–61.
Bell, J. L. (1988). Toposes and Local Set Theories: An introduction, volume 14 of Oxford Logic Guides. Clarendon, Oxford.
Bishop, E. (1967). Foundations of Constructive Analysis. McGraw-Hill, New York, NY.
Bishop, E. (1970). Mathematics as a numerical language. In Kino, A., Myhill, J., and Vesley, R., editors, Intuitionism and Proof Theory, pages 53–71. North-Holland, Amsterdam.
Bishop, E. and Bridges, D. (1985). Constructive Analysis. Springer, Berlin.
Ciraulo, F. (2007). Constructive Satisfiability. PhD thesis, Università di Palermo.
Coquand, T., Sambin, G., Smith, J., and Valentini, S. (2003). Inductively generated formal topologies. Annals of Pure and Applied Logic, 104:71–106.
Dummett, M. (1977). Elements of Intuitionism, volume 2 of Oxford Logic Guides. Clarendon, Oxford.
Hancock, P. and Hyvernat, P. (2006). Programming interfaces and basic topology. Annals of Pure and Applied Logic, 137:189–239.
Hyland, J. M. E. (1982). The effective topos. In Troesltra, A. S. and van Dalen, D., editors, The L.E.J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics, pages 165–216. North-Holland, Amsterdam.
Maietti, M. E. (1999). About effective quotients in constructive type theory. In Altenkirch, T., Naraschewski, W., and Reus, B., editors, Types for Proofs and Programs. TYPES ’98, volume 1657 of Lecture Notes in Computer Science, pages 164–178. Springer, Berlin.
Maietti, M. E. (2005). Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science, 15:1089–1149.
Maietti, M. E. (2009). A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160:319–354.
Maietti, M. E. and Sambin, G. (2005). Toward a minimalist foundation for constructive mathematics. In Crosilla, L. and Schuster, P., editors, From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, volume 48 of Oxford Logic Guides, pages 91–114. Clarendon, Oxford.
Maietti, M. E. and Sambin, G. (201x). Choice sequences in a minimalist foundation. In preparation.
Maietti, M. E. and Valentini, S. (1999). Can you add power-sets to Martin-Löf’s intuitionistic set theory? Mathematical Logic Quarterly, 45:521–532.
Martin-Löf, P. (1970). Notes on Constructive Mathematics. Almqvist & Wiksell, Stockholm.
Martin-Löf, P. (1984). Intuitionistic Type Theory: Notes by G. Sambin of a Series of Lectures Given in Padua, June 1980. Bibliopolis, Napoli.
Martin-Löf, P. (2006). 100 years of Zermelo’s axiom of choice: what was the problem with it? The Computer Journal, 49:10–37.
Martin-Löf, P. and Sambin, G. (in press). Generating positivity by coinduction. In The Basic Picture: Structures for Constructive Topology. Oxford University Press, Oxford, to appear.
Nordström, B. and Petersson, K. (1990). Programming in Martin-Löf’s Type Theory: An introduction. Oxford University Press, Oxford.
Sambin, G. (1987). Intuitionistic formal spaces—a first communication. In Skordev, D., editor, Mathematical Logic and Its Applications, pages 187–204. Plenum, New York, NY.
Sambin, G. (1995). Pretopologies and completeness proofs. Journal of Symbolic Logic, 60:861–878.
Sambin, G. (2002). Steps towards a dynamic constructivism. In Gärdenfors, P., Kijania-Placek, K., and Wolenski, J., editors, In the Scope of Logic: Methodology and Philosophy of Science, vol. 1, number 315 in Synthese Library, pages 263–286. Kluwer, Dordrecht.
Sambin, G. (2003). Some points in formal topology. Theoretical Computer Science, 305:347–408.
Sambin, G. (201x). The Basic Picture: Structures for Constructive Topology. Oxford University Press, Oxford. to appear.
Sambin, G. and Valentini, S. (1998). Building up a toolbox for Martin-Löf’s type theory: subset theory. In Sambin, G. and Smith, J., editors, Twenty-five Years of Constructive Type Theory, number 36 in Oxford Logic Guides, pages 221–244. Clarendon. Proceedings of a Congress held in Venice, October 1995.
Troelstra, A. and van Dalen, D. (1988). Constructivism in Mathematics: An Introduction, volume 2 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam.
Vickers, S. (2006). Compactness in locales and in formal topology. Annals of Pure and Applied Logic, 137:413–438.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Sambin, G. (2011). A Minimalist Foundation at Work. In: DeVidi, D., Hallett, M., Clarke, P. (eds) Logic, Mathematics, Philosophy, Vintage Enthusiasms. The Western Ontario Series in Philosophy of Science, vol 75. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0214-1_4
Download citation
DOI: https://doi.org/10.1007/978-94-007-0214-1_4
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-0213-4
Online ISBN: 978-94-007-0214-1
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)