%0 Journal Article
%T On the Constructive Dedekind Reals
%A Robert Lubarsky
%A Michael Rathjen
%J Mathematics
%D 2015
%I arXiv
%X In order to build the collection of Cauchy reals as a set in constructive set theory, the only Power Set-like principle needed is Exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that Exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, CZF with Subset Collection replaced by Exponentiation, in which the Cauchy reals form a set while the Dedekind reals constitute a proper class.
%U http://arxiv.org/abs/1510.00641v1