Skip to main content
SpringerLink
Log in
Book cover

New Computational Paradigms pp 287–312Cite as

Metamathematical Properties of Intuitionistic Set Theories with Choice Principles

  • Chapter

This paper is concerned with metamathematical properties of intuitionistic set theories with choice principles. It is proved that the disjunction property, the numerical existence property, Church’s rule, and several other metamathematical properties hold true for constructive Zermelo–Fraenkel Set Theory and full intuitionistic Zermelo–Fraenkel augmented by any combination of the principles of countable choice, dependent choices, and the presentation axiom. Also Markov’s principle may be added.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Aczel: The type theoretic interpretation of constructive set theory. In: MacIntyre, A. and Pacholski, L. and Paris, J., editor, Logic Colloquium ’77 (North Holland, Amsterdam 1978) 55-66.

    Chapter  Google Scholar 

  2. P. Aczel: The type theoretic interpretation of constructive set theory: Choice principles. In: A.S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium (North Holland, Amsterdam 1982) 1-40.

    Google Scholar 

  3. P. Aczel: The type theoretic interpretation of constructive set theory: Inductive definitions. In: R.B. Marcuset al., editors, Logic, Methodology and Philosophy of Science VII (North Holland, Amsterdam 1986) 17-49.

    Google Scholar 

  4. P. Aczel, M. Rathjen: Notes on constructive set theory, Technical Report 40, Institut Mittag-Leffler(The Royal Swedish Academy of Sciences,2001). http://www.ml.kva.se/preprints/archive2000-2001.php

  5. M. Beeson: Continuity in intuitionistic set theories. In: M Boffa, D. van Dalen, K. McAloon, editors, Logic Colloquium ’78 (North-Holland, Amsterdam 1979).

    Google Scholar 

  6. M. Beeson: Foundations of Constructive Mathematics. (Springer-Verlag, Berlin, Heidel-berg, New York, Tokyo 1985).

    MATH  Google Scholar 

  7. A. Blass: Injectivity, projectivity, and the axiom of choice. Transactions of the AMS 255 (1979) 31-59.

    Article  MATH  MathSciNet  Google Scholar 

  8. E. Bishop and D. Bridges: Constructive Analysis. (Springer-Verlag, Berlin, Heidelberg, New York, Tokyo 1985).

    MATH  Google Scholar 

  9. L. Crosilla, M. Rathjen: Inaccessible set axioms may have little consistency strength. Annals of Pure and Applied Logic 115 (2002) 33-70.

    Article  MATH  MathSciNet  Google Scholar 

  10. S. Feferman: A language and axioms for explicit mathematics. In: J.N. Crossley, editor, Algebra and Logic, Lecture Notes in Math. 450 (Springer, Berlin 1975) 87-139.

    Google Scholar 

  11. S. Feferman: Constructive theories of functions and classes. In: M. Boffa, D. van Dalen, K. McAloon, editors, Logic Colloquium ’78 (North-Holland, Amsterdam 1979) 159-224.

    Google Scholar 

  12. H. Friedman: Some applications of Kleene’s method for intuitionistic systems. In: A. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic, vol-ume 337 of Lectures Notes in Mathematics (Springer, Berlin, 1973) 113-170.

    Chapter  Google Scholar 

  13. H. Friedman: The disjunction property implies the numerical existence property. Pro-ceedings of the National Academy of Sciences of the United States of America 72 (1975) 2877-2878.

    Article  MATH  Google Scholar 

  14. H. Friedman: Set-theoretic foundations for constructive analysis. Annals of Mathematics 105 (1977) 868-870.

    Article  Google Scholar 

  15. H. Friedman, S. Š čedrov: Set existence property for intuitionistic theories with dependent choice. Annals of Pure and Applied Logic 25 (1983) 129-140.

    Article  MATH  MathSciNet  Google Scholar 

  16. H. Friedman, S. Š čedrov: The lack of definable witnesses and provably recursive func-tions in intuitionistic set theory. Advances in Mathematics 57 (1985) 1-13.

    Article  MATH  MathSciNet  Google Scholar 

  17. S.C. Kleene: On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic 10 (1945) 109-124.

    Article  MATH  MathSciNet  Google Scholar 

  18. S.C. Kleene: Disjunction and existence under implication in elementary intuitionistic formalisms. The Journal of Symbolic Logic 27 (1962) 11-18.

    Article  MathSciNet  Google Scholar 

  19. S.C. Kleene: An addendum. Journal of Symbolic Logic 28 (1963) 154-156.

    Article  MathSciNet  Google Scholar 

  20. S.C. Kleene: Formalized recursive functionals and formalized realizability. Memoirs of the AMS 89 (AMS, Providence 1969).

    Google Scholar 

  21. G. Kreisel, A.S. Troelstra: Formal systems for some branches of intuitionistic analysis. Annals of Mathematical Logic 1 (1970) 229-387.

    Article  MATH  MathSciNet  Google Scholar 

  22. J. Lipton: Realizability, set theory and term extraction. In: The Curry-Howard isomor-phism, Cahiers du Centre de Logique de l’Universite Catholique de Louvain, vol. 8 (1995) 257-364.

    MathSciNet  Google Scholar 

  23. D.C. McCarty: Realizability and recursive mathematics, PhD thesis, Oxford University (1984), 281 pages.

    Google Scholar 

  24. D.C. McCarty: Realizability and recursive set theory, Annals of Pure and Applied Logic 32 (1986) 153-183.

    Article  MATH  MathSciNet  Google Scholar 

  25. J.R. Moschovakis: Disjunction and existence in formalized intuitionistic analysis. In: J.N. Crossley, editor, Sets, models and recursion theory. (North-Holland, Amsterdam 1967)309-331.

    Chapter  Google Scholar 

  26. J. Myhill: Some properties of Intuitionistic Zermelo-Fraenkel set theory. In: A. Mathias and H. Rogers (eds.): Cambridge Summer School in Mathematical Logic, volume 337 of Lectures Notes in Mathematics (Springer, Berlin 1973) 206-231.

    Chapter  Google Scholar 

  27. J. Myhill: Constructive set theory. The Journal of Symbolic Logic 40 (1975) 347-382.

    Article  MATH  MathSciNet  Google Scholar 

  28. M. Rathjen: The anti-foundation axiom in constructive set theories. In: G. Mints, R. Muskens, editors, Games, Logic, and Constructive Sets. (CSLI Publications, Stanford 2003)87-108.

    Google Scholar 

  29. M. Rathjen: The disjunction and other properties for constructive Zermelo-Fraenkel set theory. The Journal of Symbolic Logic 70 (2005) 1233-1254.

    Article  MATH  MathSciNet  Google Scholar 

  30. M. Rathjen: Realizability for constructive Zermelo-Fraenkel set theory. In: J. Väänänen, V. Stoltenberg-Hansen, editors, Logic Colloquium ’03. Lecture Notes in Logic 24 (A.K. Peters, 2006) 282-314.

    Google Scholar 

  31. M. Rathjen: Choice principles in constructive and classical set theories. In: Z. Chatzidakis, P. Koepke, W. Pohlers, editors, Logic Colloquium ’02. Lecture Notes in Logic 27 (A.K. Peters 2006).

    Google Scholar 

  32. M. Rathjen, S. Tupailo: Characterizing the interpretation of set theory in Martin-Löf type theory. Annals of Pure and Applied Logic 141 (2006) 442-471.

    Article  MATH  MathSciNet  Google Scholar 

  33. L. Tharp: A quasi-intuitionistic set theory. Journal of Symbolic Logic 36 (1971) 456-460.

    Article  MATH  MathSciNet  Google Scholar 

  34. A.S. Troelstra: Realizability. In: S.R. Buss, editor, Handbook of Proof Theory (Elsevier, Amsterdam 1998) 407-473.

    Chapter  Google Scholar 

  35. A.S. Troelstra, D. van Dalen: Constructivism in Mathematics, Volumes I, II. (North Holland, Amsterdam 1988).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Pure Mathematics, University of Leeds, LS2 9JT, Leeds, UK

    Michael Rathjen

Authors
  1. Michael Rathjen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Leeds, LS2 9JT, Leeds, UK

    S. Barry Cooper

  2. University of Amsterdam, Plantage Muidergracht 24, 1018 TV, Amsterdam, Netherlands

    Benedikt Löwe

  3. Università di Siena, Pian dei Mantellini 44, 53100, Siena, Italy

    Andrea Sorbi

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer Science+Business Media, LLC

About this chapter

Cite this chapter

Rathjen, M. (2008). Metamathematical Properties of Intuitionistic Set Theories with Choice Principles. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds) New Computational Paradigms. Springer, New York, NY. https://doi.org/10.1007/978-0-387-68546-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-0-387-68546-5_13

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-0-387-36033-1

  • Online ISBN: 978-0-387-68546-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation