Document Open Access Logo

Dependent Sums and Dependent Products in Bishop’s Set Theory

Author Iosif Petrakis

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.3.pdf
  • Filesize: 0.58 MB
  • 21 pages

Document Identifiers

Author Details

Iosif Petrakis
  • Ludwig-Maximilians-Universität Munich, Theresienstrasse 39, Germany

Acknowledgements

I want to thank the Hausdorff Research Institute for Mathematics (HIM) for providing me with ideal conditions of work as a temporary project fellow of the trimester program "Types, Sets and Constructions" (July-August 2018). It was during this stay of mine in Bonn that most of the research around this paper was carried out.

Cite AsGet BibTex

Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.3

Abstract

According to the standard, non type-theoretic accounts of Bishop’s constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman’s sense, semi-formalisation of Bishop’s set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • Bishop’s constructive mathematics
  • Martin-Löf’s type theory
  • dependent sums
  • dependent products
  • type-theoretic axiom of choice

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Peter Aczel and Michael Rathjen. Notes on Constructive Set Theory. Technical report, Institut Mittag-Leffler Preprint, 2000. Google Scholar
  2. Steven Awodey. Axiom of Choice and Excluded Middle in Categorical Logic. Bulletin of Symbolic Logic, 1:344, 1995. Google Scholar
  3. Michael J. Beeson. Formalizing constructive mathematics: Why and how? In Constructive Mathematics, pages 146-190. Springer Berlin Heidelberg, 1981. URL: https://doi.org/10.1007/bfb0090733.
  4. Michael J. Beeson. Foundations of Constructive Mathematics. Springer Berlin Heidelberg, 1985. URL: https://doi.org/10.1007/978-3-642-68952-9.
  5. Errett Bishop. Foundations of Constructive Analysis. Mcgraw-Hill, 1967. Google Scholar
  6. Errett Bishop. A General Lamguage. unpublished manuscript, 1968(9)? Google Scholar
  7. Errett Bishop. How to Compile Mathematics into Algol. unpublished manuscript, 1968(9)? Google Scholar
  8. Errett Bishop. Mathematics as a Numerical Language. In Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, pages 53-71. Elsevier, 1970. URL: https://doi.org/10.1016/s0049-237x(08)70740-7.
  9. Errett Bishop and Douglas S. Bridges. Constructive Analysis. Grundlehren der mathematischen Wissenschaften. Springer Berlin Heidelberg, 1985. Google Scholar
  10. Douglas S. Bridges and Fred Richman. Varieties of constructive mathematics. Cambridge University Press, 1987. Google Scholar
  11. Thierry Coquand, Peter Dybjer, Erik Palmgren, and Anton Setzer. Type-theoretic Foundations of Constructive Mathematics. book draft, 2005. Google Scholar
  12. Thierry Coquand and Henrik Persson. Integrated Development of Algebra in Type Theory. manuscript, 1998. Google Scholar
  13. Thierry Coquand and Arnaud Spiwack. Towards Constructive Homological Algebra in Type Theory. In Towards Mechanized Mathematical Assistants, pages 40-54. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73086-6_4.
  14. James Dugundji. Topology. Allyn and Bacon series in advanced mathematics. Allyn and Bacon, 1966. Google Scholar
  15. Robert Lee Constable et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986. Google Scholar
  16. Solomon Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, pages 87-139. Springer Berlin Heidelberg, 1975. URL: https://doi.org/10.1007/bfb0062852.
  17. Solomon Feferman. Constructive Theories of Functions and Classes. In Studies in Logic and the Foundations of Mathematics, pages 159-224. Elsevier, 1979. URL: https://doi.org/10.1016/s0049-237x(08)71625-2.
  18. Harvey Friedman. Set Theoretic Foundations for Constructive Analysis. The Annals of Mathematics, 105(1):1, January 1977. URL: https://doi.org/10.2307/1971023.
  19. Newcomb Greenleaf. Liberal constructive set theory. In Constructive Mathematics, pages 213-240. Springer Berlin Heidelberg, 1981. Google Scholar
  20. Hajime Ishihara and Erik Palmgren. Quotient topologies in constructive set theory and type theory. Annals of Pure and Applied Logic, 141(1-2):257-265, August 2006. URL: https://doi.org/10.1016/j.apal.2005.11.005.
  21. Maria Emilia Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, September 2009. URL: https://doi.org/10.1016/j.apal.2009.01.006.
  22. Per Martin-Löf. Notes on Constructive Mathematics. Almqvist and Wiksell, 1968. Google Scholar
  23. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium quotesingle73, Proceedings of the Logic Colloquium, pages 73-118. Elsevier, 1975. URL: https://doi.org/10.1016/s0049-237x(08)71945-1.
  24. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Google Scholar
  25. Ray Mines, Fred Richman, and Wim Ruitenburg. A course in constructive algebra. Springer-Verlag, 1988. Google Scholar
  26. John Myhill. Constructive set theory. Journal of Symbolic Logic, 40(3):347-382, September 1975. URL: https://doi.org/10.2307/2272159.
  27. Erik Palmgren. Bishop’s set theory. Slides from TYPES Summer School 2005, Gothenburg, 2005. Google Scholar
  28. Erik Palmgren. Lecture Notes on Type Theory. manuscript, 2014. Google Scholar
  29. Erik Palmgren and Olov Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science, Volume 10, Issue 3, 2014. URL: https://doi.org/10.2168/LMCS-10(3:25)2014.
  30. Iosif Petrakis. Constructive topology of Bishop spaces. PhD thesis, Ludwig-Maximilians-University, Munich, 2015. Google Scholar
  31. Iosif Petrakis. A constructive function-theoretic approach to topological compactness. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS quotesingle16. ACM Press, 2016. URL: https://doi.org/10.1145/2933575.2933582.
  32. Iosif Petrakis. The Urysohn Extension Theorem for Bishop Spaces. In Logical Foundations of Computer Science, pages 299-316. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-27683-0_21.
  33. Iosif Petrakis. Constructive uniformities of pseudometrics and Bishop topologies. Journal of Logic and Analysis, 11:FT2:1-44, 2019. Google Scholar
  34. Iosif Petrakis. Direct spectra of Bishop spaces and their limits. arXiv:1907.03273, 2019. Google Scholar
  35. Iosif Petrakis. Constructive Set and Function Theory. habilitation, Ludwig-Maximilians-University, Munich, in preparation, 2020. Google Scholar
  36. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, 2013. Google Scholar
  37. Giovanni Sambin. The Basic Picture: Structures for Constructive Topology. Oxford University Press, in press, 2019. Google Scholar
  38. Tilo Wiklund. Locally cartesian closed categories, coalgebras, and containers. Technical report, Uppsala Universitet, U.U.D.M Project Report, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact