Abstract
We analyze the concepts of finite set and finite subset from the perspective of a minimalist foundational theory which has recently been introduced by Maria Emilia Maietti and the second author. The main feature of that theory and, as a consequence, of our approach is compatibility with other foundational theories such as Zermelo-Fraenkel set theory, Martin-Löf’s intuitionistic Type Theory, topos theory, Aczel’s CZF, Coquand’s Calculus of Constructions. This compatibility forces our arguments to be constructive in a strong sense: no use is made of powerful principles such as the axiom of choice, the power-set axiom, the law of the excluded middle.
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
Preview
Unable to display preview. Download preview PDF.
References
Ciraulo, F., Sambin, G.: Finitary Formal Topologies and Stone’s Representation Theorem. Theoretical Computer Science (to appear)
Coquand, T.: An Intuitionistic Proof of Tychonoff Theorem. Journal of Symbolic Logic 57(1), 28–32 (1992)
van Dalen, D. (ed.): Brouwer’s Cambridge Lectures on Intuitionism. Cambridge University Press, Cambridge (1981)
Maietty, M.E.: Quotients over Minimal Type Theory. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol. 4497, Springer, Heidelberg (2007)
Maietti, M.E., Sambin, G.: Toward a Minimalist Foundation for Constructive Mathematics. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, Oxford UP. Oxford Logic Guides, vol. 48 (2005)
Martin-Löf, P.: Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples (1984)
Negri, S., Valentini, S.: Tychonoff’s Theorem in the Framework of Formal Topologies. Journal of Symbolic Logic 62(4), 1315–1332 (1997)
Nordström, B., Peterson, K., Smith, J.: Programming in Martin-Löf’s Type Theory. Clarendon Press, Oxford (1990)
Sambin, G., Valentini, S.: Building up a Toolbox for Martin-Löf Type Theory: Subset Theory. In: Sambin, G., Smith, J. (eds.) Twenty-Five Years of Constructive Type Theory. Proceedings of a Congress Held in Venice, October 1995, pp. 221–240. Oxford University Press, Oxford (1998)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol. 1. NorthHolland, Amsterdam (1988)
Veldman, W.: Some Intuitionistic Variations on the Notion of a Finite Set of Natural Numbers. In: de Swart, H.C.M., Bergman, L.J.M. (eds.) Perspectives on negation. Essays in honour of Johan J. de Iongh on his 80th birthday, pp. 177–202. Tilburg Univ. Press, Tilburg (1995)
Vickers, S.J.: Compactness in Locales and in Formal Topology. In: Banaschewski, B., Coquand, T., Sambin, G. (eds.) Papers presented at the 2nd Workshop on Formal Topology (2WFTop 2002), Venice, Italy, April 04-06, 2002. Annals of Pure and Applied Logic, vol. 137, pp. 413–438 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciraulo, F., Sambin, G. (2008). Finiteness in a Minimalist Foundation. In: Miculan, M., Scagnetto, I., Honsell, F. (eds) Types for Proofs and Programs. TYPES 2007. Lecture Notes in Computer Science, vol 4941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68103-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-68103-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68084-0
Online ISBN: 978-3-540-68103-8
eBook Packages: Computer ScienceComputer Science (R0)