On the Constructive Dedekind Reals

TL;DR

This paper demonstrates that in constructive set theory, the collection of Cauchy reals can be a set using only exponentiation, but Dedekind reals cannot, shown via a specialized Kripke model.

Contribution

It provides a Kripke model showing that exponentiation alone suffices for Cauchy reals to form a set but not for Dedekind reals, clarifying their set-theoretic status.

Findings

Cauchy reals form a set in the model

Dedekind reals form a proper class in the model

Exponentiation alone is insufficient for Dedekind reals

Abstract

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.