On the constructive Dedekind reals (Q1000868)

In classical set theory, the concepts of Cauchy reals and Dedekind reals lead to isomorphic structures. Constructive Zermelo-Fraenkel set theory at least proves that both classes form a set. But how are they related to each other? To prove that the Cauchy reals are a set, the axiom of subset collection is not needed to its full extent but may be replaced by exponentiation. This paper defines a Kripke model of Zermelo-Fraenkel set theory with subset collection replaced by exponentiation. In this model, the Dedekind reals constitute a proper class. This is a strong independence result. Readers from various fields of mathematics, like proof theory, constructive mathematics, set theory, model theory and foundations of real analysis will be interested in reading this paper.