HackerPapers

arXiv:1510.00641math.LO

On the Constructive Dedekind Reals

Robert Lubarsky, Michael Rathjen

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
Journal reference
Logic and Analysis, 1, No. 2 (2008), pp. 131-152
DOI
Subjects
math.LOLogic

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Aug 2025 to Aug 2025.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. What are the real numbers, really? (2024) 1 comment

    • Interestingly, constructive mathematics cannot prove that the Cauchy and Dedekind constructions are isomorphic: "As often happens in an intuitionistic setting, classically equivalent notions fork. Dedekind reals give rise to several demonstrably different collections of reals…

      hackandthinkView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.