The disjunction and related properties for constructive Zermelo-Fraenkel set theory

Journal of Symbolic Logic 70 (4):1233-1254 (2005)

Michael Rathjen
University of Leeds
This paper proves that the disjunction property, the numerical existence property, Church’s rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,914
Through your library

References found in this work BETA

The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Formal Systems for Some Branches of Intuitionistic Analysis.G. Kreisel - 1970 - Annals of Pure and Applied Logic 1 (3):229.
Inaccessible Set Axioms May Have Little Consistency Strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.
Realizability and Recursive Set Theory.Charles McCarty - 1986 - Annals of Pure and Applied Logic 32 (2):153-183.

View all 6 references / Add more references

Citations of this work BETA

From the Weak to the Strong Existence Property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.
Kripke Models for Subtheories of CZF.Rosalie Iemhoff - 2010 - Archive for Mathematical Logic 49 (2):147-167.

View all 8 citations / Add more citations

Similar books and articles

A Note on Bar Induction in Constructive Set Theory.Michael Rathjen - 2006 - Mathematical Logic Quarterly 52 (3):253-258.
Constructive Notions of Set: Part I. Sets in Martin–Löf Type Theory.Laura Crosilla - 2005 - Annali Del Dipartimento di Filosofia 11:347-387.
On the Constructive Dedekind Reals.Robert S. Lubarsky & Michael Rathjen - 2008 - Logic and Analysis 1 (2):131-152.
Inaccessible Set Axioms May Have Little Consistency Strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.
Non-Deterministic Inductive Definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.
A Single Axiom for Set Theory.David Bennett - 2000 - Notre Dame Journal of Formal Logic 41 (2):152-170.


Added to PP index

Total views
13 ( #614,094 of 2,266,272 )

Recent downloads (6 months)
1 ( #850,735 of 2,266,272 )

How can I increase my downloads?


My notes

Sign in to use this feature