On the Constructive Dedekind Reals
Logic
2015-10-05 v1
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.
Cite
@article{arxiv.1510.00641,
title = {On the Constructive Dedekind Reals},
author = {Robert Lubarsky and Michael Rathjen},
journal= {arXiv preprint arXiv:1510.00641},
year = {2015}
}