The Dedekind cuts in an ordered set form a set in the sense of constructive
Zermelo—Fraenkel set theory. We deduce this statement from the principle of
refinement, which we distill before from the axiom of fullness. Together
with exponentiation, refinement is equivalent to fullness. None of the
defining properties of an ordering is needed, and only refinement for
two—element coverings is used.
¶
In particular, the Dedekind reals form a set; whence we have also refined an
earlier result by Aczel and Rathjen, who invoked the full form of fullness.
To further generalise this, we look at Richman's method to complete an
arbitrary metric space without sequences, which he designed to avoid
countable choice. The completion of a separable metric space turns out to be
a set even if the original space is a proper class; in particular, every
complete separable metric space automatically is a set.