Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Rathjen, M (2005)
Publisher: Graz University of Technology, Institut für Informationssysteme und Computer Medien
Languages: English
Types: Article
The paper furnishes realizability models of constructive Zermelo-Fraenkel set theory, CZF, which also validate Brouwerian principles such as the axiom of continuous choice (CC), the fan theorem (FT), and monotone bar induction (BIM), and thereby determines the proof-theoretic strength of CZF augmented by these principles. The upshot is that CZF+CC+FT possesses the same strength as CZF, or more precisely, that CZF+CC+FTis conservative over CZF for 02 statements of arithmetic, whereas the addition of a restricted version of bar induction to CZF (called decidable bar induction, BID) leads to greater proof-theoretic strength in that CZF+BID proves the consistency of CZF.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. 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.
    • 2. P. Aczel: The type theoretic interpretation of constructive set theory: Inductive de nitions. In: R.B. et al. Marcus, editor, Logic, Methodology and Philosophy of Science VII (North Holland, Amsterdam 1986) 17{49.
    • 3. P. Aczel, M. Rathjen: Notes on constructive set theory, Technical Report 40, Institut Mittag-Le er (The Royal Swedish Academy of Sciences, 2001). http://www.ml.kva.se/preprints/archive2000-2001.php
    • 4. J. Barwise: Admissible Sets and Structures (Springer-Verlag, Berlin, Heidelberg, New York, 1975).
    • 5. M. Beeson: Foundations of Constructive Mathematics. (Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985).
    • 6. E. Bishop and D. Bridges: Constructive Analysis. (Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985).
    • 7. D. Bridges, F. Richman: Varieties of constructive mathematics. LMS Lecture Notes Series 97 (Cambridge University Press,Cambridge,1987).
    • 8. L.E.J. Brouwer: Weten, willen, spreken (Dutch). Euclides 9 (1933) 177-193.
    • 9. L. Crosilla and M. Rathjen: Inaccessible set axioms may have little consistency strength Annals of Pure and Applied Logic 115 (2002) 33{70.
    • 10. M. Dummett: Elements of intuitionism. Second edition (Clarendon Press,Oxford,2000)
    • 11. S. Feferman: A language and axioms for explicit mathematics. In: J.N. Crossley (ed.): Algebra and Logic, Lecture Notes in Math. 450 (Springer, Berlin 1975) 87{139.
    • 12. S. Feferman: Constructive theories of functions and classes in: Bo a, M., van Dalen, D., McAloon, K. (eds.), Logic Colloquium '78 (North-Holland, Amsterdam 1979) 159{224.
    • 13. N. Gambino: Types and sets: a study on the jump to full impredicativity, Laurea Dissertation, Department of Pure and Applied Mathematics, University of Padua (1999).
  • No related research data.
  • Discovered through pilot similarity algorithms. Send us your feedback.

Share - Bookmark

Funded by projects

Cite this article