Abstract

We introduce a new axiom scheme for constructive set theory, the Relation Reflection Scheme . Each instance of this scheme is a theorem of the classical set theory ZF. In the constructive set theory CZF–, when the axiom scheme is combined with the axiom of Dependent Choices , the result is equivalent to the scheme of Relative Dependent Choices . In contrast to RDC, the scheme RRS is preserved in Heyting-valued models of CZF– using set-generated frames. We give an application of the scheme to coinductive definitions of classes