Document Open Access Logo

De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory

Author Robert Passmann

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.33.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Robert Passmann
  • Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands

Funding

This research was partially supported by the Studienstiftung des deutschen Volkes (German Academic Scholarship Foundation).

Acknowledgements

I would like to thank Lorenzo Galeotti, Joel Hamkins, Rosalie Iemhoff, Dick de Jongh, Yurii Khomskii, and Benedikt Löwe for helpful and inspiring discussions.

Cite As Get BibTex

Robert Passmann. De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.33

Abstract

We prove that the propositional logic of intuitionistic set theory IZF is intuitionistic propositional logic IPC. More generally, we show that IZF has the de Jongh property with respect to every intermediate logic that is complete with respect to a class of finite trees. The same results follow for constructive set theory CZF.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Proof theory
Keywords
  • Intuitionistic Logic
  • Intuitionistic Set Theory
  • Constructive Set Theory

Metrics

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

Related Versions

References

  1. Peter Aczel. The type theoretic interpretation of constructive set theory. In Leszek Pacholski Angus Macintyre and Jeff Paris, editors, Proceedings of the Colloquium held in Wrocław, August 1-12, 1977), volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55-66. North-Holland Publishing Co., Amsterdam-New York, 1978. Google Scholar
  2. Peter 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. Proceedings of the Symposium held in Noordwijkerhout, June 8-13, 1981, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 1-40. North-Holland Publishing Co., Amsterdam-New York, 1982. Google Scholar
  3. Peter Aczel. The type theoretic interpretation of constructive set theory: inductive definitions. In Georg J. W. Dorn Ruth Barcan Marcus and Paul Weingartner, editors, Logic, methodology and philosophy of science. VII. Proceedings of the seventh international congress held at the University of Salzburg, Salzburg, July 11-16, 1983, volume 114 of Studies in Logic and the Foundations of Mathematics, pages 17-49. North-Holland Publishing Co., Amsterdam, 1986. Google Scholar
  4. Peter Aczel and Michael Rathjen. Notes on Constructive Set Theory. Draft, 2010. Google Scholar
  5. Mohammad Ardeshir and S. Mojtaba Mojtahedi. The de Jongh property for Basic Arithmetic. Archive for Mathematical Logic, 53(7-8):881-895, 2014. Google Scholar
  6. John L Bell. Set theory: Boolean-valued models and independence proofs, volume 47. Oxford University Press, 2011. Google Scholar
  7. Dick de Jongh. The maximality of the intuitionistic predicate calculus with respect to Heyting’s arithmetic. The Journal of Symbolic Logic, 35(4):606, 1970. Google Scholar
  8. Dick de Jongh and Craig Smoryński. Kripke models and the intuitionistic theory of species. Annals of Mathematical Logic, 9(1-2):157-186, 1976. Google Scholar
  9. Dick de Jongh, Rineke Verbrugge, and Albert Visser. Intermediate Logics and the de Jongh property. Archive for Mathematical Logic, 50(1):197-213, 2011. Google Scholar
  10. Rosalie Iemhoff. Kripke models for subtheories of CZF. Archive for Mathematical Logic, 49(2):147-167, 2010. Google Scholar
  11. Kenneth Kunen. Set theory: An introduction to independence proofs, volume 102 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam-New York, 1980. Google Scholar
  12. Benedikt Löwe, Robert Passmann, and Sourav Tarafder. Constructing illoyal algebra-valued models of set theory, 2018. ILLC Prepublication Series PP-2018-15. Google Scholar
  13. Robert S. Lubarsky. Independence results around constructive ZF. Annals of Pure and Applied Logic, 132(2-3):209-225, 2005. Google Scholar
  14. Robert S. Lubarsky. Separating the Fan Theorem and Its Weakenings II. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2018, Deerfield Beach, FL, USA, January 8-11, 2018, Proceedings, volume 10703 of Lecture Notes in Computer Science, pages 242-255. Springer, 2018. Google Scholar
  15. Robert S. Lubarsky and Hannes Diener. Separating the Fan Theorem and its weakenings. The Journal of Symbolic Logic, 79(3):792-813, 2014. Google Scholar
  16. Robert S. Lubarsky and Michael Rathjen. On the constructive Dedekind reals. Logic & Analysis, 1(2):131-152, 2008. Google Scholar
  17. David Charles McCarty. Incompleteness in intuitionistic metamathematics. Notre Dame Journal of Formal Logic, 32(3):323-358, 1991. Google Scholar
  18. John Myhill. Some properties of intuitionistic Zermelo-Fraenkel set theory. In A. R. D. Mathias and H. Rogers, editors, Cambridge Summer School in Mathematical Logic (held in Cambridge, England, August 1-21, 1971), volume 337 of Lecture Notes in Mathematics, pages 206-231. Springer-Verlag, Berlin-New York, 1973. Google Scholar
  19. Robert Passmann. Loyalty and Faithfulness of Model Constructions for Constructive Set Theory. Master’s thesis, ILLC, University of Amsterdam, 2018. Master of Logic Thesis (MoL) Series MoL-2018-03. Google Scholar
  20. Robert Passmann. The de Jongh property for bounded constructive Zermelo-Fraenkel set theory. ILLC Prepublication Series PP-2019-05, 2019. Google Scholar
  21. Michael Rathjen. The disjunction and related properties for constructive Zermelo-Fraenkel set theory. The Journal of Symbolic Logic, 70(4):1232-1254, 2005. Google Scholar
  22. Gene F. Rose. Propositional calculus and realizability. Transactions of the American Mathematical Society, 75:1-19, 1953. Google Scholar
  23. Craig Smoryński. Applications of Kripke models. In A. S. Troelstra, editor, Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Lecture Notes in Mathematics, pages 324-391. Springer, Berlin, 1973. Google Scholar
  24. Andrew Swan. CZF does not have the existence property. Annals of Pure and Applied Logic, 165(5):1115-1147, 2014. Google Scholar
  25. Anne Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. I, volume 121 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. Google Scholar
  26. Jaap van Oosten. A semantical proof of de Jongh’s theorem. Archive for Mathematical Logic, 31(2):105-114, 1991. Google Scholar
  27. Albert Visser. Rules and arithmetics. Notre Dame Journal of Formal Logic, 40(1):116-140, 1999. Google Scholar
  28. Freek Wiedijk. The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, 10(23):121-133, 2007. 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 About DROPS Imprint Privacy Contact