arXiv · 1510.00641
On the Constructive 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.
Explore related subjects
Keep this discovery
Robert Lubarsky, Michael Rathjen. 2015-10-02. On the Constructive Dedekind Reals. https://arxiv.org/abs/1510.00641
Cite the original work for its findings. Save a collection to share your selection of sources.